Conversation
4994bfe to
609a770
Compare
Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
|
@jcommelin, thanks! Once I am home, I will undo these squeezing and I will add these proof to the unlinted ones. My impression is that the category theory ones need some new idea. The others, almost make me wish that |
There was a problem hiding this comment.
@adomani do you want to resolve all merge conflicts once more? Then I think we could see that we get this merged quickly.
(and maybe do a bench! once you've done that, just for good measure)
| induction' s using WSeq.recOn with a s s <;> | ||
| simp only [nil_append, cons_append, destruct_cons, destruct_pure, liftRelAux_inl_inl, | ||
| LiftRelO, true_and, think_append, destruct_think, Computation.destruct_think, | ||
| liftRelAux_inr_inr] | ||
| · induction' S using WSeq.recOn with s S S <;> | ||
| simp only [nil_append, join_nil, cons_append, join_cons, destruct_think, | ||
| Computation.destruct_think, think_append, append_assoc, liftRelAux_inr_inr, join_think] | ||
| · induction' SS using WSeq.recOn with S SS SS <;> | ||
| simp only [join_nil, destruct_nil, destruct_pure, map_nil, liftRelAux_inl_inl, LiftRelO, | ||
| join_cons, join_think, destruct_think, Computation.destruct_think, map_cons] |
There was a problem hiding this comment.
Is this one of the instances where avoiding non-terminal simp obfuscates the proof unreasonably?
PR summary 8d36235876Import changesNo significant changes to the import graph Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
|
@adomani : I feel like this PR has been lying around for too long. The squeezes here either already have been fixed or should be addressed by your "flexible linter". I think it's probably easier to close this PR and redo the things again on a fresh master branch if still relevant. Please reopen the PR if you disagree. |
|
I'm happy with closing this. As you probably know, I am no longer sure that squeezing |
Another batch of squeezed
simps, converted mostly tosimp only, but alsosimpa,tauto,aesopandsimp? says.Ref: #11246