Should `grind` use `simp` lemmas?

Stream: new members

[Asei Inoue]

I think you want “grind +simp” option?

[Asei Inoue]

I want such a option too.
I think “@[simp]” tag and “@[grind =]” tag tend to appear simultaneously…

[Henrik Böving]

grind is not a better simp. Please refer to the reference manual sections for simp and grind. They operate on fundamentally different ideas with simp aiming to be a confluent-as-possible rewriting system while grind works by combining equivalence classes of terms. While a lot of simp theorems are sensible grind theorems not all of them are.

[Jakub Nowak]

@Henrik Böving I completely agree that they're different. But why do you think that not all simp lemmas are a sensible grind theorems? As far as I understand how grind works adding more lemmas to it won't stop it from being able to prove something it could before, the only downside being performance. I can agree that not all simp lemmas are needed for grind, or rather we can have better version of them. Current adoption of grind in mathlib is not anywhere near complete. Adding something like grind +simp sounds like a quick option to be able to start exploring using grind with mathlib. Once grind adoption is complete we can discourage using grind +simp.

[Alex Meiburg]

While a lot of simp theorems are sensible grind theorems not all of them are.

I've heard this a few times and I think I would really benefit from some examples. (Also, having those examples in the documentation.) Cause I haven't been able to think of a case myself, probably because I don't fully grok grind myself.

[Marcus Rossel]

@Alex Meiburg here's a (not so good) example. Though I'm not even sure if grind is expected to fail.

import Mathlib

variable [CommRing R] [LieRing L] [LieAlgebra R L] (t : R) (x y : L)

example : ⁅x, t • y⁆ = t • ⁅x, y⁆ := by
  simp only [LieAlgebra.lie_smul]

example : ⁅x, t • y⁆ = t • ⁅x, y⁆ := by
  grind only [LieAlgebra.lie_smul] -- invalid `grind` theorem, failed to find an usable pattern using different modifiers

[Jakub Nowak]

Marcus Rossel said:

Alex Meiburg here's a (not so good) example. Though I'm not even sure if grind is expected to fail.

import Mathlib

variable [CommRing R] [LieRing L] [LieAlgebra R L] (t : R) (x y : L)

example : ⁅x, t • y⁆ = t • ⁅x, y⁆ := by
  simp only [LieAlgebra.lie_smul]

example : ⁅x, t • y⁆ = t • ⁅x, y⁆ := by
  grind only [LieAlgebra.lie_smul] -- invalid `grind` theorem, failed to find an usable pattern using different modifiers

But that's only an example of a theorem that cannot be used with grind. It's not an example of a theorem that's good for simp and bad for grind.
That only means that grind +simp would probably not use all simp theorems. And that's assuming this would work by just adding simp theorems as grind theorems (which isn't very helpful, this could be automated with some script).

[Notification Bot]

7 messages were moved here from #new members > Why `grind` isn't using `simp` lemmas? by Jakub Nowak.

[Jovan Gerbscheid]

LieAlgebra.lie_smul is just a bad lemma because of lean#9727, which needs to be fixed.

[Kim Morrison]

It's a good question, with a few angles on the answer.

0. Yes, @[simp] implies @[grind =] is a good zero-th approximation for adding annotations.
1. It might lead to grind annotations that are not as good as they might be (with or without the use of +simp), and going slightly slower (i.e. encouraging, by requiring, users to think about the annotations for their libraries) may reach a better endpoint.
2. It's not entirely trivial to implement: stuff is happening (i.e. patterns are being identified and indexed) at the time we write @[grind] or grind_pattern, and this would have to be hooked into @[simp] to also run then: you can't just, at tactic run time, decide to throw in all simp lemmas.
3. It's pretty common to write @[grind =] on lemmas with an if on the right hand side (taking advantage of grinds case bashing power), but we tend not to want to do this for @[simp]. Conflating, even partially, @[grind =] and @[simp] might lead to deterioration in @[simp] sets (by people adding @[simp] in order to enable it in grind, and not realising that it causes a problem in simp.

That all said, it's not crazy to try it out. We do need to make grind easier to use in situations where the library hasn't been annotated at all. As of a recent nightly we now have grind +suggestions which uses a (configurable) premise selection engine to add many theorems into the grind set at tactic invocation time. This will hopefully get a lot more powerful in coming releases, as we tune the premise selection engines, and enable using external neural engines.

[Damiano Testa]

Is there some programmatic way of detecting some goals that definitely should have the grind attribute and link that to a linter?

[Kim Morrison]

Not particularly that I can think of.

[Jakub Nowak]

I was thinking that we could use simp lemmas in grind differently than other grind lemmas. When the algorithm picks an expression A, applies some grind lemmas to it, which results in some expression B, we could then apply simp algorithm to the expression B. And then we could either add both to the e-graph, or completely forget about B. But always applying simp algorithm and forgetting about B can lead to failure in proofs grind would have been successful otherwise.

[Bhavik Mehta]

Yes, @[simp] implies @[grind =] is a good zero-th approximation for adding annotations.

Focusing on this point (since I don't have a strong opinion on the other things discussed here), are there concrete examples where @[simp] is good where @[grind =]isn't? And while reading the manual is of course the correct thing to do, what's the first-order correction needed for this approximation?

[Jovan Gerbscheid]

Wasn't it recommended to not tag lemma with grind if they are about algebra, such as add_zero, because matching on such patterns is messy (and redundant) due to the sattelite solvers of grind?

[Bhavik Mehta]

Oh yeah, good point!

[Bhavik Mehta]

So the first-order approximation might be "if it's simp, make it grind =, unless it's ringy"

[František Silváši 🦉]

Sounds about right for the time being, but doesn't appear to scale... we are one step away from 'unless one of the satellite solvers doesn't like that', and then you need this bag of trivia to not step on an arbitrary landmine that evolves over time.

[Jovan Gerbscheid]

I haven't looked closely at the way grind indexes patterns, but it uses something else than the DiscrTree used by simp. So that may also play a role in determining what is or isn't a good grind annotation.