Zulip Chat Archive

Stream: general

Topic: LFTCM2020 category theory

Sebastien Gouezel (Oct 14 2022 at 12:17):

I had fixed LFTCM2020 yesterday, but it is again broken today :-( But this is because of category theory, where a nonterminal simp is not doing anything anymore, in

def functor.preadditive.preserves_biproducts (F : C  D) (P : F.preadditive) (X Y : C) :
  F.obj (X  Y)  F.obj X  F.obj Y :=
-- sorry
{ hom := biprod.lift (F.map biprod.fst) (F.map biprod.snd),
  inv := biprod.desc (F.map biprod.inl) (F.map biprod.inr),
  hom_inv_id' := begin simp, simp_rw [F.map_comp, P.map_add'], simp, end,
  inv_hom_id' := begin ext; simp; simp_rw [F.map_comp]; simp [P.map_zero'], end, }
-- This proof is not yet "mathlib-ready", because it uses "nonterminal" `simp`s.
-- Can you fix it?
-- sorry

(the first simp in hom_inv_id' does not simplify). @Scott Morrison , could you have a look?

Jireh Loreaux (Oct 14 2022 at 14:15):

I think this is just evidence that non-terminal simps are so evil they can't even be discussed in teaching materials. :rofl:

Sebastien Gouezel (Oct 14 2022 at 14:19):

And my answer to the question can you fix it? is clearly no, I can't :grinning_face_with_smiling_eyes:

Scott Morrison (Oct 16 2022 at 06:29):

Sorry, I can't reproduce. In lftcm2020, that proof was sorried out in master, and when I restore the proof given above it compiles fine.

Scott Morrison (Oct 16 2022 at 06:29):

I guess I can do the simps anyway.

Scott Morrison (Oct 16 2022 at 06:35):

I restored the proof with the non-terminal simps expanded.

Sebastien Gouezel (Oct 16 2022 at 08:13):

Thanks. I guess you didn't reproduce because you didn't try to update mathlib: the proof used to build fine with mathlib from two days ago, but not with yesterday's.

Sebastien Gouezel (Oct 16 2022 at 08:29):

But with the explicit lemmas you provided and the amazing https://mathlib-changelog.org/, I was able to fix it myself.

Last updated: Aug 03 2023 at 10:10 UTC