Explicit and grind-free suggestions from the grind tool

Stream: lean4

[Plamen Dimitrov]

I would be great if we could make grind output the working proof path and not just the initial e-matched theorems. In many cases users (me included) would prefer not to have grind as a proof of each and every theorem they define (assuming best outcomes from the tool) but self-documenting steps of theorems that were applied and how the proof was achieved. The aesop? for instance can easily suggest a proof path that one can still verify manually and/or refine for compactness and customization. It would be great if grind? could expand similarly or at least provide grind-free replacement of its output that described the found proof.

What are your thoughts about this? Has something in this direction already been developed and/or worked on?

[Kim Morrison]

No, an entirely grind free proof would not be possible: there do not exist the primitives required to concisely express a grind proof! (Beyond, of course, the proof term, which in principle you can get with show_term grind.)

[Plamen Dimitrov]

But IIUC as the proofs grind finds are all in essence mathematical proofs still fully utilizing dependent type theory, CoC, etc. it could indicate where it found a contradiction in the proof-by-contradiction search it does? While it would expand the whiteboard with collected theorems it should be possible to trace back how a given contradiction was reached, i.e. to describe the proof "trace" that was reached and not how the entire search process. Or do you mean something more fundamental with "no primitives to express a grind proof"?

[Henrik Böving]

The closest to that explanation you can get is the fully expanded grind-mode proof that grind? gives you.

[Snir Broshi]

Kim Morrison said:

(Beyond, of course, the proof term, which in principle you can get with show_term grind.)

Or show_term grind -abstractProof to avoid the foo._proof_1_1 stuff