Grind

Stream: lean4

[Bas Spitters]

What is the best source to learn more about Grind? I've found this one helpful:
https://pr-451--lean-reference-manual-review.netlify.app/The--grind--tactic

Given the name, perhaps it is inspired by Grind in PVS? https://pvs.csl.sri.com/doc/pvs-prover-guide.pdf

It also seems similar to https://gitlab.inria.fr/fbesson/itauto in Rocq.
And I guess Isabelle may have something similar.

I would expect Lean's grind to use the most modern algorithms, and I would be curious what they are.

[Henrik Böving]

If you care about the actual implementation of grind the easiest way to figure out what's going on is probably to read https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%3Aleodemoura+is%3Aclosed+, there is obviously inspirations from existing literature, for example the linear integer stuff is based on https://leodemoura.github.io/files/cutsat.pdf but it also has custom modifications to avoid having to do case splits that are not published anywhere.

I don't know whether grind is related to PVS though based on the fact that Leo used to work at SRI maybe there is at least a spiritual connection.

I would also reason that grind is quite obviously more capable than itauto given the fact that it can prove the provided example on which itauto fails:

Goal forall {A: Type} (x y z: A) (p: Prop), x = y -> y = z -> (x = z -> p) -> p.
Proof.
intros.
Fail intuition congruence.
Abort.

example  {A: Type} (x y z: A) (p: Prop) : x = y -> y = z -> (x = z -> p) -> p := by grind -- works

I don't know if Isabelle has an all-in-one tool that can keep up with grind, grind has the ability to perform case analysis, congruence closure and e matching and linear integer stuff which I'm somewhat confident sledgehammer can probably do. But on top of that it also supports reasoning in arbitrary (commutative) (semi)rings, fields and linear arithmetic. I'm not sure whether sledgehammer can do that? Maybe an Isabelle expert here can chime in on that.

[Bas Spitters]

Thanks @Henrik Böving

About itauto, you read that example a bit too quickly. itauto was in fact designed to solve that example.
itauto also combines with other tactics. So, e.g.

itauto ring

would do something similar in Rocq, although I suspect Grind to be more efficient.

[Henrik Böving]

How does a ring solver come into play here? A is an arbitrary type without any additional assumptions isn't it?

[Bas Spitters]

Those were two separate remarks.

1. itauto solves that goal.
2. itauto ring supports reasoning in arbitrary (commutative) (semi)rings.

[metakuntyyy]

Does there also exist grind? that produces a term?

[Henrik Böving]

There does exist a grind? that produces something akin to simp? but nothing that directly produces a term no. Internally grind does obviously generate a term but there is little point in putting it int othe proof script

[Mario Carneiro]

you can use show_term grind to get the proof term (as with any tactic)

[metakuntyyy]

Ah ok, I see. show_term should suffice.

[Kim Morrison]

Please don't. :-)

[metakuntyyy]

Now I wonder even more how big those terms can get. I guess for context since @Mario Carneiro knows that I come from metamath and the big feature is complete traceability. I consider every tactic as a black box and I want to learn what it does, sometimes just so that I can port the proof.

I guess this translates why I like #explode, conv and the simple tactics that much.

[metakuntyyy]

I guess we all have different use cases.

[Kim Morrison]

I didn't mean that what you get from show_term grind would be terrible: it actually produces decent proof terms quite often. Just that it's missing the point of grind-style automation to care what it did. :-)

[Kim Morrison]

(As long as it's working...!)

[metakuntyyy]

Ah I didn't mean to replace grind with the show term, I just wanted to see if there is something that can be inspected. I guess this is a question of perspective. A proof author, given a step can use grind to solve it. But for a proof reader this step is a black box. It would be easy for example to see, ah grind does a case split on n from 120 to 800 or something like that and solves each goal individually.

Also is it designed to be extended. Let's say I have a decision procedure that has to look at finite amount of cases. Can I extend grind to solve goals of a specific form?

[Henrik Böving]

It would be easy for example to see, ah grind does a case split on n from 120 to 800 or something like that and solves each goal individually.

I don't think this is easy to see at all for non trivial proofs by inspecting the proof term

[metakuntyyy]

I've tried it out

theorem expr (k:ℕ) (h:k < 8): k^2 ≤ 100 := by
  interval_cases k
  repeat norm_num

works, but

import Mathlib

theorem expr (k:ℕ) (h:k < 8): k^2 ≤ 100 := by
  grind

fails. Maybe I'm misusing it.

[Kim Morrison]

It's not intended that grind can solve that problem (yet). When it does, it will not be by case-bashing, and it will equally well prove (k < 2^1000) → (k^2 < 2^3000).

[Mario Carneiro]

that sounds optimistic TBH, lean really likes to compute big numbers

[Mario Carneiro]

well, 2^1000 isn't too big to represent so maybe that's possible, but if the number was even bigger I would expect it to have issues

[Kenny Lau]

@metakuntyyy the proof is "obviously"

import Mathlib.Data.Nat.Basic

theorem expr (k : ℕ) (h : k < 8) : k^2 ≤ 100 := by
  decide +revert

:slight_smile:

[metakuntyyy]

Can someone tell me where the entry point of the grind tactic is in the code.

syntax (name := grind)
  "grind" optConfig (&" only")?
  (" [" withoutPosition(grindParam,*) "]")?
  (&" on_failure " term)? : tactic

This code is bespoke. Am I supposed to look for a def called grind? If so, where is it defined.

[Henrik Böving]

https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Grind.lean#L263

[metakuntyyy]

Ah I see, what is the purpose of the code in Init? I couldn't understand how this is connected and what it's doing.

[Henrik Böving]

It declares the syntax for people to use, the other file declares how the syntax is elaborated, this is the approach for all meta programs in Lean (though some macros allow to do both things at once)

[metakuntyyy]

Ah, so Init = Syntax and Elab is where the juice is made.

If I wanted to add a logging line to grind, kinda like a hello world every time I call grind. Would it work to just change the code to add a println?

[Henrik Böving]

If you compile your own Lean from source with an IO.println line added you would see it in the info view yes, the more idiomatic way would be to use the trace framework that you see being used in grind (and other elaborators) all over the place. Given that you seem to have basically zero experience with meta programming though I would suggest to maybe take a look through the meta programming book before trying to do things in grind.

[metakuntyyy]

The questions I ask are independent of grind. I am indeed trying to understand how to do metaprogramming. I thought adding a newline and seeing how the sauce is made would help me more. My preferred approach is top-down. I want to understand the architecture and building step first.