Lint error with `Simp says`

Stream: mathlib4

[Xavier Roblot]

CI is failing on some PRs and the problem is due to some call to simp says not producing the expected result, see for example here. I am not sure what the correct fix is but I have been trying to collect these errors and replace the calls to simp says by simp only in a PR: #28775

[Kevin Buzzard]

See Kim's comment 2 here #nightly-testing > Mathlib status updates @ 💬

[Bryan Gin-ge Chen]

These should hopefully go away if you merge master, which includes #28764 covering some of the same fixes. The one in LucasLehmer looks new though...

[Bryan Gin-ge Chen]

Thanks for putting together this PR by the way; if there are any fixes that remain after merging master, I'll be happy to merge it quickly whenever you think it's ready!

[Xavier Roblot]

I see that the solution you used was to fix the simp says and not replace it by a simp only. Is that what I should do with the other (possible) errors?

[Bryan Gin-ge Chen]

Good question. Let's try and fix them for now.

We may end up removing all the says at some point, but in that case we'll still need the correct simp only there, I think.

[Xavier Roblot]

The simp call in LucasLehmer can just be deleted so that's an easy fix :wink:

[Bryan Gin-ge Chen]

I would check that the proof isn't getting much slower though -- there's a chance that the simp was helping Lean avoid some unfolding.

[Xavier Roblot]

I have checked that there is no significant timing difference with or without the simp call.

#28775 is ready for review.

[Sébastien Gouëzel]

If a simp says breaks, I think we should replace it by the fixed simp says and not by simp only: the point of simp says is to emphasize which lemmas are important, and which lemmas are just coming from the simpset. This is valuable information, which is lost in the simp only.

[Kim Morrison]

Yes, simp? says is complicated: it preserved useful information for humans, which is great, but comes at a pretty annoying maintenance cost (in particular, failures that you can't see until CI, and quite often these failures fall on the people looking after nightly-testing).

[Michael Stoll]

I'm seeing a bunch of simp? says errors in #26766 (after merging master).
More specifically (see here),

  Error: error: Mathlib/Algebra/Order/CauSeq/Basic.lean:440:2: Tactic `simp? [not_forall]
     at nk` produced `simp only [gt_iff_lt, ge_iff_le, not_exists, not_and, not_forall, Classical.not_imp, not_le] at nk`,
  but was expecting it to produce `simp only [gt_iff_lt, ge_iff_le, not_exists, not_and, not_forall, not_le] at nk`!

  Error: error: Mathlib/CategoryTheory/Limits/Fubini.lean:108:18: Tactic `simp?  at this` produced `simp only [Category.id_comp, map_id, NatTrans.id_app] at this`,
  but was expecting it to produce `simp only [Category.id_comp, Functor.map_id, NatTrans.id_app] at this`!

  Error: error: Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean:131:6: Tactic `simp? [w'', α,
    β]` produced `simp only [Functor.comp_obj, vComp'_app, Iso.trans_inv, Functor.isoWhiskerLeft_inv, Iso.symm_inv, assoc,
      NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app, Functor.whiskerLeft_app, Functor.associator_inv_app,
      comp_id, id_comp, vComp_app, Functor.map_comp, Equivalence.inv_fun_map, CatCommSq.vInv_iso_hom_app, Iso.trans_hom,
      Functor.isoWhiskerLeft_hom, Iso.symm_hom, Functor.associator_hom_app, Functor.rightUnitor_hom_app,
      Iso.hom_inv_id_app_assoc, w'', α, β]`,
  but was expecting it to produce `simp only [Functor.comp_obj, vComp'_app, Iso.trans_inv, Functor.isoWhiskerLeft_inv, Iso.symm_inv, assoc,
      NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app, Functor.whiskerLeft_app, Functor.associator_inv_app,
      comp_id, id_comp, vComp_app, Functor.map_comp, Equivalence.inv_fun_map, CatCommSq.vInv_iso_hom_app, Iso.trans_hom,
      Functor.isoWhiskerLeft_hom, Iso.symm_hom, Functor.associator_hom_app, Functor.rightUnitor_hom_app,
      Iso.hom_inv_id_app_assoc, w'', this, α, β]`!

  Error: error: Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean:83:4: Tactic `simp? [colimit_eq_iff]
     at
      h` produced `simp only [comp_obj, colim_obj, ι_colimitLimitToLimitColimit_π_apply, colimit_eq_iff, curry_obj_obj_obj,
      curry_obj_obj_map] at h`,
  but was expecting it to produce `simp only [Functor.comp_obj, colim_obj, ι_colimitLimitToLimitColimit_π_apply, colimit_eq_iff, curry_obj_obj_obj,
      curry_obj_obj_map] at h`!

What should I do about this?

[Michael Rothgang]

Can you make a separate PR just fixing these? (You probably need to make an artificial change to each of these files to force a proper build, and hopefully then you can fix them.) If this path works, it seems the nicest.

[Michael Rothgang]

If it doesn't, we have a much bigger problem...

[Bryan Gin-ge Chen]

I think if you put set_option says.verify true at the top of the file these warnings should pop up. I wish there was an easier way to fix these all at once. In #28764 I made a change to Mathlib.Init to try to force the warnings in the rest of mathlib to show up, but it didn't work... maybe I just need to do a rebuild from scratch locally with CI=true.

edit: I've started a build while I go for lunch. Hopefully I can have a PR ready later.

[Michael Stoll]

I'm confused: To create the PR, I did git switch master; git pull; git switch -c <new branch>, but I then cannot find the first simp? says that gave an error in the relevant file (Mathlib/Algebra/Order/CauSeq/Basic.lean, line 440).

My suspicion is that I might have done something wrong when I tried to merge master previously (what I did was git merge upstream/master and then git push); IIRC it looked like the CI run after that produced the same errors as the one before, which I think is suspicious.

[Michael Stoll]

I guess I should have pulled before mergeing...

[Michael Stoll]

So I merged master again, and now it seems to be OK:
Sorry for the noise!