Moving to grind

Stream: Analysis I

[Dan Abramov]

I've noticed anecdotally that grind seems to work better than aesop (or simp_all) but it only seems activated for lemmas specifically tagged for grind.

Should we tag existing simp lemmas as also being grind lemmas? Is the best practice to leave both or to fully move over to grind? Not sure what makes sense for the book content.

Overall I wish grind could be used in more places because it feels faster. Though maybe it's because there aren't as many grind lemmas yet.

[Dan Abramov]

One downside of grind is it seems less obvious how to check what lemmas it used. I'm sure there's some way to do that? With aesop I just write aesop? and it tells me.

[Shreyas Srinivas]

Grind is different from simp. This is explained in the lean reference manual

[Dan Abramov]

I’m aware that it is not literally the same thing. My point is that aesop and grind seem to solve similar goals (or maybe that’s wrong?) but aesop seems slower and less powerful so I’d like to replace more of its usage by grind. But unlike aesop, which seems to be aware of simp lemmas, grind isn’t. So the question is whether we should go over already marked lemmas and mark then for grind too.

If there’s a bigger point you disagree with, I’d appreciate you being more explicit. “RTFM” is rarely a helpful response.

[Li Xuanji]

I'm still getting a feel for how best to use grind, but here's what I've found helpful so far:

1. You can use grind [myTheorem1, myTheorem2] to try out specific theorems without "committing" to having them marked with the grind attributes
2. grind the tactic is also available in grind? and grind only [...] variants that can give you more visibility into the lemmas used. I don't think there is a way for it to tell you about lemmas that can be removed, it seems like the grind architecture is not designed for this.
3. The grind "tags" are more complicated than simp tags, it teaches grind how to "instantiate" theorems, and you can use variants like @[grind =] (documented here) to get finer control over the instantiation. I'm still trying to fully grok this, but playing around with the examples on that page was pretty useful.
4. On simp vs grind, my mental model (others please correct if I'm wrong) is that there are some proofs that have "rewrite this expression into a more complicated form" as an intermediate step, and grind is designed to be able to find them, but simp is not, and this is why it's harder to annotate grind lemmas (you don't want grind to do a lot of useless simpler -> more complicated rewriting). An example of such a proof might be, rewrite 1 with 10^0 so that at the next step, you can use some lemma like a^x b^x = (ab)^x. Also, if I have a proof step that looks like "do the obvious simplifications" (no clever rewriting), stylistically I prefer to use simp even when grind works, but that is just a personal preference.

[Lawrence Wu (llllvvuu)]

One downside of grind is it seems less obvious how to check what lemmas it used. I'm sure there's some way to do that? With aesop I just write aesop? and it tells me.

grind also has grind? (EDIT: saw this mentioned). Or you can do set_option trace.grind.ematch true, which shows why a lemma was instantiated.

[Rado Kirov]

I haven't used grind at all in this project so far, but also curious to start using it more. My mental model is there is a partial ordering:
1) rw < simp
2) simp < domain specific tactics - tauto, omega, positivitiy, norm_cast, linarith (all of those are not comparable with each other)
3) simp < aesop
4) domain specific tactics < aesop
Is this correct? Good style mandates one uses the least powerful tactic that closes the goal, but one needs a clear picture of the power of the tactic to apply that.

I haven't read much about aesop, but also rarely use it because it is at the top of the tactics power order, so it is the last tactic to try (I noticed it shines when one needs to introduce by case analysis). AFAIU, grind is plays in the same spaces a aesop (not domain specific, and more powerful than simp). Is that true? If so I will start swapping aesop with it.

[Shreyas Srinivas]

simp and domain specific tactics have no ordering.

[Shreyas Srinivas]

They are meant to construct proofs differently under the presence of different kinds of hypothesis