fix: replace bad simp lemmas for Id #8388
Conversation
This is free at runtime, since both `Id.run` and `pure` are inlined.
sgraf812
requested review from
TwoFX,
david-christiansen,
digama0,
kim-em,
mhuisi,
Kha,
leodemoura and
zwarich
as code owners
|
This is a rebase of #7352. (CC @eric-wieser). In #8066 (comment) Eric writes
I'm content to leave the "think about which lemmas should be about Id.run" for someone else. I'm not sure about back compat. What concrete steps does thinking about that entail? Also is there a way to at least acknowledge you as co-author (if not as main author)? |
github-actions
bot
added
the
toolchain-available
|
Thanks!
If you merge the PR normally, the individual commits with my name should show up. If you squash merge, then optimistically github will add a Co-authored-by line automatically, or else you can add it yourself. |
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
the
breaks-mathlib
|
The other thing you could do is directly push to #7352, since maintainers are allowed to write to that branch. |
| @[simp] theorem forIn'_yield_eq_foldl | ||
| {xs : Array α} (f : (a : α) → a ∈ xs → β → β) (init : β) : | ||
| forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) = | ||
| xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by | ||
| rcases xs with ⟨xs⟩ | ||
| simp [List.foldl_map] | ||
| {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : | ||
| (forIn' xs init (fun a m b => .yield <$> f a m b)).run = | ||
| xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := | ||
| forIn'_pure_yield_eq_foldl _ _ |
There was a problem hiding this comment.
To elaborate on my comment elsewhere; I think:
- The old lemma should be kept and deprecated
- The new lemma should be called
idRun_forIn'_yield_eq_foldlandsimp
This applies to pretty much every statement modified in this PR.
There was a problem hiding this comment.
Some existing lemmas follow the naming scheme id_run_* (Array.id_run_foldlM); others follow the naming scheme *_id:
@[simp]
theorem findM?_id (p : α → Id Bool) (as : List α) :
(findM? p as).run = as.find? (p · |>.run) :=
findM?_pure _ _
Should I change these as well? To which naming scheme? The former is more "post-order traversal", the latter is more "in-order traversal". As a user, I think I would have an easier time finding the latter, but of course it depends on whether I have Id.run * or *.run, so YMMV.
There was a problem hiding this comment.
That lemma is not an "existing lemma", the .run was added in this PR. So I'm pretty convinced we should be adding "run" to these names.
I think the id_run name (vs idRun) is a pretty weird reading of the naming convention, but since the concern is cosmetic I'll let someone else at the fro decide.
of course it depends on whether I have Id.run * or *.run, so YMMV.
My guess would be that the former tends to be less confusing, and so in a separate PR it would make sense to tell the delaborator not to use dot notation
There was a problem hiding this comment.
In conversation with Markus, Paul and Kim, we decided on adopting the idRun_* naming convention 👍
I pushed to #7352 for Kim to take over and will close this PR. Sorry about the chaos 😅
| @@ -2541,18 +2541,18 @@ theorem flatten_reverse {L : List (List α)} : | |||
| induction l generalizing b <;> simp [*] | |||
|
|
|||
| theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} : | |||
There was a problem hiding this comment.
| theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} : | |
| theorem foldl_eq_idRun_foldlM {f : β → α → β} {b : β} {l : List α} : |
etc, keeping the old lemma as deprecated and proving it with the new one.
|
I pushed to #7352 for Kim to take over and closed this PR. Sorry about the chaos 😅 |
|
Thanks for championing it! |
This PR reworks the simp set around the Id monad.
In particular, it stops encoding the "defeq abuse" of Id X = X in the statements of theorems, instead using Id.run and pure to pass back and forth between these two spellings.
This fixes the problem with the current simp set where Id.run (pure x) is simplified to Id.run x, instead of the desirable x.
This is particularly bad because the x is sometimes inferred with type Id X instead of X, which prevents other simp lemmas about X from firing.
Making Id reducible instead is not an option, as then the Monad instances would have nothing to key on.