Zulip Chat Archive

Stream: PR reviews

Topic: !4#2808 CategoryTheory.Monoidal.Free.Basic

Scott Morrison (Apr 06 2023 at 10:14):

This PR, which has been stalled for a while, has some interesting problems. If anyone would like to jump in on this one, it could use some help!

  1. There is a PANIC in _private.Lean.Meta.Match.MatchEqs.0.Lean.Meta.Match.SimpH.substRHS, which is quite likely a Lean 4 bug. It would be great to minimize this, which is going to be some nontrivial work, but doable. Just start copying stuff into a new file, inlining imports and removing material that is incidental to generating the panic...

  2. In the construction of project at the end of the file, the fields map_comp and μ_natural used to by proved by tidy in mathlib3, but aesop_cat can't yet cope. (It's not brave enough about doing induction on hypotheses, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Aesop.20and.20cases).
    Even so, when I try to prove these by hand, I have to write induction' f using Quotient.recOn, and I don't understand why just induction isn't enough.

  3. Again in the construction of project, in μ_natural, Lean doesn't seem to process the proof; it says there are unfinished goals but doesn't produce goal states during the final steps. Not sure what is happening here.

Scott Morrison (Apr 06 2023 at 10:43):

(And thanks Moritz for the work on this one already. It was not a smooth ride. :-)

Joël Riou (May 03 2023 at 11:22):

I could fix !4#2808 by using dsimp instead of simp for the definition which strangely triggered a PANIC. I have also ported CategoryTheory.Monoidal.Free.Coherence !4#3769, which is mostly done, except for another PANIC "invalid LCNF substitution of free variable with expression CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.{u}" at https://github.com/leanprover-community/mathlib4/pull/3769/files#diff-c2efee64cb592a9da8340f823962d63d41ab3cf932cc32b0e1375f0f24d6e968R117-R136

Matthew Ballard (May 17 2023 at 01:23):

Adding dsimp [normalizeObj] avoids the panics though I am not sure why

Joël Riou (May 18 2023 at 07:30):

Thanks! Now, it compiles.

Matthew Ballard (May 18 2023 at 12:44):

Hmm. Does just dsimpwork to avoid the panic?

Last updated: Dec 20 2023 at 11:08 UTC