fix: unsqueeze simp, re Yaël's comments on #11259#11455
fix: unsqueeze simp, re Yaël's comments on #11259#11455
Conversation
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
| theorem head_ofSeq (s : Seq α) : head (ofSeq s) = Computation.pure s.head := by | ||
| simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map] | ||
| cases Seq.head s <;> rfl | ||
| simp [head]; cases Seq.head s <;> rfl |
There was a problem hiding this comment.
@YaelDillies Why do you want to bring back a non-terminal simp here? If you don't like simp only, then we can use simp? says simp only ...
There was a problem hiding this comment.
Here is my comment for context: #11259 (comment)
My arguments for the squeezed simp being a worse proof are that
- It mentions more lemmas
- Those lemmas are part of the very basic API of their corresponding defs and could change if the defs change defeq
- The non-terminal simp was just unfolding the definitions anyway (importantly, in a way that doesn't depend on the exact defeqs)
|
This PR has been on the queue for a long time now, we should make a decision. Yael: I gather you're against the |
|
I agree that reintroducing the nonterminal simp isn't right here. If any change is wanted here,
sounds good to me. |
|
Sure, we can try. I'm not yet convinced it's better than having |
| theorem head_ofSeq (s : Seq α) : head (ofSeq s) = Computation.pure s.head := by | ||
| simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map] | ||
| cases Seq.head s <;> rfl | ||
| simp [head]; cases Seq.head s <;> rfl |
There was a problem hiding this comment.
| simp [head]; cases Seq.head s <;> rfl | |
| suffices Computation.pure (Option.map (Prod.fst ∘ (·, s.tail)) s.head) | |
| = Computation.pure (s.head) by simpa [head] | |
| cases Seq.head s <;> rfl |
|
Coming here from triaging stale PRs: is this PR still relevant? If not, feel free to close it. |
This PR reverts/simplifies some of the "squeeze
simp" changes in #11259.See #11259 for context.