simpNF error behind `simps`

Stream: mathlib4

[Arien Malec]

In !4#1995 this definition causes a simpNF error

-- The additive version of `Finsupp.toTinsupp`. Note that this is `noncomputable` because
`Finsupp.hasAdd` is noncomputable. -/
@[simps (config := { fullyApplied := false })]
def finsuppLequivDfinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M] : (ι →₀ M) ≃ₗ[R] Π₀ _i : ι, M :=
  { finsuppEquivDfinsupp with
    toFun := Finsupp.toDfinsupp
    invFun := Dfinsupp.toFinsupp
    map_smul' := Finsupp.toDfinsupp_smul
    map_add' := Finsupp.toDfinsupp_add }

the error is

#check @finsuppLequivDfinsupp_apply_apply /- Left-hand side simplifies from
  ↑(finsuppLequivDfinsupp R).toLinearMap
to
  ↑(finsuppLequivDfinsupp R)
using
  simp only [@LinearEquiv.coe_coe]

but I have no access to the definition that's failing... (I only know this is the definition that fails by using the hack of moving #lint up the file until it doesn't fail...

[Arien Malec]

I tried to nolint here, but it doesn't help

[Arien Malec]

and if I remove the config section from simps the lint issue goes away....

[Jireh Loreaux]

simps? will tell you the declarations that simps is generating.

[Arien Malec]

Ah, yes, I see the declaration... What's the fix here?

[Arien Malec]

I see in another file that the fix was to add the lemmas manually...

[Arien Malec]

And the generated code doesn't typecheck?

[Jireh Loreaux]

The fact that the code from the pretty printer doesn't type check isn't too surprising, you may need to massage it a bit.

The problem is that the LHS isn't simplified (i.e., there is some other lemma that simplifies the LHS), which means that sometimes this lemma wouldn't get applied when you want it to (because it will get "skipped over" due to the other simp lemma).

In this case, I personally think it makes sense to replace the LHS of the generated lemma with the one provided by simpNF (and so you should manually add the simp lemma).

[Arien Malec]

Thanks. Yep, on it as soon as I figure out the types.

[Arien Malec]

As an example, simps? generates (this is one of the ones that simpNF didn't complain about):

finsuppLequivDfinsupp_apply_apply:
            > ∀ {ι : Type u_1} (R : Type u_2) {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R]
      [inst_2 : AddCommMonoid M] [inst_3 : (m : M) → Decidable (m ≠ 0)] [inst_4 : Module R M],
      ↑(finsuppLequivDfinsupp R).toLinearMap = Finsupp.toDfinsupp

which I've translated as:

@[simp]
theorem finsuppLequivDfinsupp_apply_toAddHom_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M]:
    ↑(finsuppLequivDfinsupp R).toLinearMap.toAddHom = Finsupp.toDfinsupp := sorry

but we get type errors

type mismatch
  (finsuppLequivDfinsupp R).toLinearMap.toAddHom
has type
  AddHom (?m.64898 →₀ ?m.64899) (Dfinsupp fun _i => ?m.64899) : Type (max ?u.64895 ?u.64897)
but is expected to have type
  (?m.64785 →₀ ?m.64786) → Dfinsupp fun _i => ?m.64786 : Type (max ?u.64783 ?u.64784)

(note that it doesn't matter if I take the simps output more verbatim -- same issues with the below (which is the same thing modulo prettier formatting and previous variable declarations).

theorem finsuppLequivDfinsupp_apply_toAddHom_apply:
        ∀ {ι : Type u_1} (R : Type u_2) {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R]
      [inst_2 : AddCommMonoid M] [inst_3 : (m : M) → Decidable (m ≠ 0)] [inst_4 : Module R M],
      ↑(finsuppLequivDfinsupp R).toLinearMap.toAddHom = Finsupp.toDfinsupp := sorry

[Floris van Doorn]

simps is configured wrong for linearEquiv, it shouldn't even generate these lemmas, and didn't do this in Lean 3. I will PR a fix, going through all simps configurations.

There is still one thing I don't understand, maybe @Gabriel Ebner knows what's going on.
If, after the definition of finsuppLequivDfinsupp in !4#1995, I write the following, then simp can simplify the LHS of both lemmas, but the linter complains only about 1 of them. Is that expected? Should the linter also complain about lemma2?

@[simp]
lemma lemma1 [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
    (↑(finsuppLequivDfinsupp (M := M) R).toLinearMap : (ι →₀ M) → _) =
    Finsupp.toDfinsupp := by
  simp -- simplifies LHS to `↑(finsuppLequivDfinsupp R)`
  rfl

@[simp]
lemma lemma2 [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M] (f : ι →₀ M) :
    (finsuppLequivDfinsupp (M := M) R).toLinearMap f =
    Finsupp.toDfinsupp f := by
  simp -- simplifies LHS to `↑(finsuppLequivDfinsupp R) f`
  rfl

#lint -- simpNF complains only about lemma1, not about lemma2

[Gabriel Ebner]

The only difference between lemma1 and lemma2 is that lemma1's lhs is foo and lemma2's lhs is foo x, right? Then it should be clear why only lemma2 is redundant: lemma1 applies to lemma2 but not vice versa.

[Floris van Doorn]

Yes, that is exactly the difference.
In this case lemma2 is redundant, because of lemma1, but I am confused why the simpNF linter doesn't complain about it (lemma2), even though the LHS is not in simp-normal form.

[Gabriel Ebner]

I guess lemma2 is simplified using itself, so it doesn't look like it's redundant.

[Floris van Doorn]

In Lean 4 subexpressions are not simplified first? Is this allowed for the same reason that in Lean 3 we could have simp lemmas that specialize earlier simp-lemmas?

[Gabriel Ebner]

I think it's more "partial applications are not simplified first", but I'd need to check.

[Floris van Doorn]

ok, thanks