finding `simps` lemmas

Stream: mathlib4

[Jireh Loreaux]

In mathlib 3 I could do @[simps?] to see the lemmas that simps was generating. What can I do in Lean 4?

[Reid Barton]

autocompletion I guess?

[Gabriel Ebner]

There's also whatsnew in @[simps] def foo := ... (which works for all commands).

[Floris van Doorn]

Did you try @[simps?] in Lean 4?

[Jireh Loreaux]

Yes, and that gave me nothing. Actually, whatsnew complains too, because of the syntax (it wants to see the def immediately, not the @[attrs...])

[Jireh Loreaux]

So I still don't have a solution to this.

[Floris van Doorn]

Jireh Loreaux said:

Yes, and that gave me nothing.

#mwe?

The code

import Mathlib.Tactic.Simps.Basic

@[simps?]
def foo : Nat × Nat := (1, 2)

gives

[simps.verbose] [simps] > generating projection information for structure Prod.

[simps.verbose] [simps] > generated projections for Prod:
            > Projection fst: fun α β x => x.fst
            > Projection snd: fun α β x => x.snd

[simps.verbose] [simps] > adding projection foo_fst:
            > foo.fst = 1

[simps.verbose] [simps] > adding projection foo_snd:
            > foo.snd = 2

It's a linter trace message. Did you turn anything like that off?

[Jireh Loreaux]

I confirm that your mwe works for me. However, if you want to see where it was failing for me, pull !4#1949 and have a look at the first @[simps apply] (line 143). There are lots of errors in the file, but they all occur after that declaration. I didn't turn off any linting (at least not consciously). I would troubleshoot, but I need to go teach.

[Kevin Buzzard]

whatsnew in works for me, and says that

whatsnew in
/-- `finsupp.map_range` as an equiv. -/
@[simps apply]
def mapRange.equiv (f : M ≃ N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) : (α →₀ M) ≃ (α →₀ N)
    where
  toFun := (mapRange f hf : (α →₀ M) → α →₀ N)
...

produces Finsupp.mapRange.equiv, Finsupp.mapRange.equiv.proof_1 and Finsupp.mapRange.equiv.proof_2. One appealing conclusion consistent with everything is that @[simps apply] creates 0 lemmas. I've never understood @[simps] properly. What's it supposed to produce?

[Jireh Loreaux]

oops, I apologize, whatsnew does work for me on that declaration. It didn't work later in the file, but that may have been because of various errors that showed up earlier.

[Jireh Loreaux]

simps? doesn't though.

[Kevin Buzzard]

What I'm saying is that according to whatsnew, simps is creating 0 new lemmas, and this is consistent with simps? printing out nothing.

[Kevin Buzzard]

And what I'm asking is what lemmas you're expecting it to produce, because I don't understand simps.

[Jireh Loreaux]

oh, sorry, I understand. Normally simps produces the definitional lemmas associated to data-carrying structure projections (although in mathlib 3 at least it can sometimes do other things too, but sometimes this causes it to timeout). In this case, I think I would be expecting it to make a slightly different lemma:

lemma mapRange.equiv_apply (f : M ≃ N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) (g : α →₀ M) : mapRange.equiv f hf hf' g = mapRange f hf g := rfl

I think it is supposed to make this lemma because of an initialize_simps_projection (since it's not exactly just the structure projection), but I could be wrong.

[Floris van Doorn]

This is caused by noncomputable section on line 48. It seems to disable all attributes (including @[simp] or @[simps]) with applicationTime := .afterCompilation. This is a bug in core.
Note: @[simps?] always prints something, even if there are 0 lemmas generated.

[Floris van Doorn]

@Gabriel Ebner shall I open an issue in the lean4 repo?

[Gabriel Ebner]

Yes please. If you know, can you also please explain why simps should be afterCompilation (i.e., why it can't be afterTypeChecking).

[Floris van Doorn]

This is left-over from Lean 3 behavior. simps had to be run after to_additive, to_additive had to be run after simp and simp is afterCompilation. I think this is all unnecessary since !4#1314. I'll try to remove these application times and see if everything is ok.

[Floris van Doorn]

lean4#2077

[Jireh Loreaux]

Thanks @Floris van Doorn!