feat(tactic/lint): check that left-hand side of all simp lemmas is in simp-normal form

[gebner]

Motivation: suppose you write a simp lemma 0 ≤ of_nat n. You then try it out only to find out that it doesn't work. What happened? There is another simp lemma rewriting of_nat n to ↑n, and your nice lemma never has a chance to apply.

What was wrong with the lemma? The term of_nat n was not in simp-normal form, it is simplified to ↑n.

This PR introduces a linter to detect such simp lemmas, concretely it checks that all arguments of the left-hand side of the simp lemma are in simp-normal form. It also fixes a large number of these issues across mathlib.

The error message from the linter is hopefully enlightening enough:

-- ring_theory/algebra.lean
#print algebra.map_sub /- Argument #5 of left-hand side (algebra_map A (r - s)) reduces from
  r - s
to
  r + -s
using 
  [sub_eq_add_neg] -/

There is maybe an argument to be made that some of the simp-normal forms should be chosen differently. I tried to keep the existing simp-normal forms as far as possible, and only remove/fix lemmas that could never apply. If you want to change the simp NFs, I'd prefer to do this in follow-up PRs.

• Subtraction is the single largest source of issues. The lemma sub_eq_add_neg rewrites a - b to a + -b. Hence no lemma with a - on the left-hand side ever worked as a simp lemma.
• Multisets use 0 and + instead of ∅ and ∪. Therefore you can't use the built-in set notation on the lhs of simp lemmas.
• Finsets have their special finset.singleton, so you can't have {a} on the lhs of a simp lemma.
• I'm getting really annoyed by coercions as type classes. As you probably know, we have two different coercions from ℕ to ℤ. And of course half of the lemmas used the wrong coercion on the lhs. To make it even worse, the error message you get from the linter is ↑n reduces to ↑n. 😠
• You can't use ⋃ x ∈ A ∪ B, ... on the lhs of a simp lemma, because x ∈ A ∪ B simplifies to x ∈ A ∨ x ∈ B.
• You can't use ∃ x ∈ A, ... either. By now you can probably guess why.

I have a few more linters for simp lemmas in the works: no local constants as head symbols, simp lemmas that can be proven by simp, and local confluence.

[digama0]

This is a really great linter. I want to remark specifically about the case of subtraction though that I want to kill sub_eq_add_neg with fire. If we change core to un-simp this, will it be difficult to find the now mangled simp lemmas and fix them to use subtraction on the lhs?

[sgouezel]

Is there a way to create a new attribute @[standard_form_simp] or whatever name you like, that would create a new lemma in which the left hand side would be replaced by its simp normal form, and add it to the simpset? I think all these lemmas for which you removed the simp attribute would benefit from such an attribute.

[gebner]

to kill sub_eq_add_neg with fire.

Then please submit a PR to our glorious Lean fork! We can also finally get rid of add_comm as a simp lemma (I'm just waiting for our current CI troubles to clear up before merging Ed's PR).

If we change core to un-simp this, will it be difficult to find the now mangled simp lemmas and fix them to use subtraction on the lhs?

Practical answer: you revert the "remove simp lemmas for sub" commit from this PR.

Interesting answer: if the local confluence checker (#4 in the series) actually works (read: is fast enough and doesn't produce too many false positives), then you probably only need to add this lemma and fix all the subsequent linter issues:

@[simp] lemma add_neg_eq_sub : a + -b = a - b := sorry

[gebner]

I think all these lemmas for which you removed the simp attribute would benefit from such an attribute.

Only very few of the lemmas I changed would be fixed by such an attribute. E.g. all of the *_sub lemmas would just result in redundant simp lemmas (which will be rejected by simp linter #3).

Some of the changed lemmas are OK at the point where they are defined. They are only broken by later simp lemmas. A standard_form_simp attribute wouldn't help here either.

For the few lemmas where it would work, I believe it is clearer and more reliable to just write the correct left-hand side by hand. Furthermore, synthesizing the left-hand side automatically is fragile for the same reasons that non-terminal simp is fragile: 1) the simplifier is not fully deterministic (due to some bugs); 2) new simp lemmas may change the lhs, and even introduce non-termination.

[gebner]

Should we just ignore sub_eq_add_neg for now? @digama0 If you submit a PR removing the simp attribute for sub_eq_add_neg, then I'll manually remove sub_eq_add_neg from the simp set used in the linter and we don't need to change all the lemmas back the next time we upgrade Lean.

[urkud]

BTW, why do we use a special finset.singleton?

[digama0]

it doesn't require a decidable instance, unlike the regular singleton, since that is defined in terms of finset.insert which does require the decidable instance.

[robertylewis]

What's the status here? This PR works for both 3.5.1 and a future Lean including leanprover-community/lean#117 ? I think we should merge it fast before conflicts come up! @fpvandoorn @digama0 any thoughts?

[robertylewis]

@gebner Could you add this to the list of default linters at the top of lint.lean and in command.md?

[gebner]

What's the status here? This PR works for both 3.5.1 and a future Lean including leanprover-community/lean#117 ?

Yes, there's nothing that changes, really. At the moment I'm just manually removing sub_eq_add_neg from the simp set. This will be a no-op in Lean 3.6.

Could you add this to the list of default linters at the top of lint.lean and in command.md?

Done.

[urkud]

Was it deleted for a reason?

[gebner]

Yes, because it is exactly the same as mk0_val, but with a ⁻¹ around (the coercion is inserted inside the inverse). It's not used anywhere, so I removed it.

[robertylewis]

There are merge conflicts already. @digama0 @fpvandoorn last chance to comment, I suggest we merge today!

[gebner]

And the linter has caught three new broken simp lemmas (I've just fixed them):

 -- analysis/normed_space/multilinear.lean
#print continuous_multilinear_map.uncurry0_curry0 /- Argument #8 of left-hand side (continuous_multilinear_map.curry0 𝕜 G
  (continuous_multilinear_map.uncurry0 f)) reduces from
  continuous_multilinear_map.uncurry0 f
to
  ⇑f 0
using 
  [continuous_multilinear_map.uncurry0_apply] -/
#print continuous_multilinear_map.curry0_norm /- Argument #2 of left-hand side (∥continuous_multilinear_map.uncurry0 f∥) reduces from
  continuous_multilinear_map.uncurry0 f
to
  ⇑f 0
using 
  [continuous_multilinear_map.uncurry0_apply] -/

-- algebraic_geometry/prime_spectrum.lean
#print prime_spectrum.zero_locus_bot /- Argument #2 of left-hand side (prime_spectrum.zero_locus ↑⊥) reduces from
  ↑⊥
to
  {0}
using 
  [submodule.bot_coe] -/

[fpvandoorn]

This looks really useful! It seems good to merge this quickly indeed.

Two questions:

• The linter tries to simplify all arguments of the lhs of the expression, correct? So if I have a lemma
  with LHS a + (b + of_nat n) I will get the feedback that b + of_nat n reduces to b + ↑n, right?
• It doesn't ensure that the lhs as a whole is in simp-normal-form (ignoring the lemma under consideration?), right? So if I have two hypothetical simp-lemmas a + (b + c) = (a + b) + c and a + (b + 0) = a + b (and no others), will it complain about the second one (since the LHS is not in simp-normal form)? Or do we want to allow those? Is this related to the local confluence linter?

[gebner]

I will get the feedback that b + of_nat n reduces to b + ↑n, right?

Yes, indeed. You also get the list of simp lemmas causing this reduction.

It doesn't ensure that the lhs as a whole is in simp-normal-form (ignoring the lemma under consideration?), right?

You've got this right. I wanted the (first version of the) linter to only point out objectively broken simp lemmas. If one of the arguments is not in simp-normal form, then the simp lemma can never rewrite. You always need to fix the lemma indicated by the linter.

Checking for reducibility of the whole left-hand side is also interesting and what I'm going to do real soon now. However such a check also subsumes a redundancy lint (i.e. it will complain whenever you have a simp lemma that can be proven by simp). I didn't know at first if it would be feasible remove all redundant simp lemmas or if there are performance issues when simplifying all left-hand sides. And there were performance issues: that's how I found the looping lemmas in #2026.

But I think that linting and removing redundant simp lemmas is feasible now, there's not that many: https://gist.github.com/gebner/32577f90fafecde4db92b2efd4b49666 I'll probably merge the linter for redundant lemmas and the normal form linter.

Practically speaking, it's easier to first fix the really broken lemmas and then fix the less broken lemmas in a second PR.