How to see what `grind` is doing?

Stream: new members

[Bbbbbbbbba]

I have a grind proof but I want to learn why grind works in this case and not others, and whether it might be worthwhile to convert this into an explicit proof. Neither show_term nor trace.grind yields anything useful.

import Mathlib


set_option trace.grind true


example (N x : ℝ) (hx : x ^ 3 = N) : x ^ 9 = N * (N * N) := by
  show_term grind

[Ilmārs Cīrulis]

Explicit proof seems to be short, so, probably yes, you can use it instead of grind.

import Mathlib

example (N x : ℝ) (hx : x ^ 3 = N) : x ^ 9 = N * (N * N) := by
  rw [← hx]; ring

[Yan Yablonovskiy 🇺🇦]

After the rewrite, you can run show_term on ring, but fair warning it is very horrible to look at. Tactics like this typically look rough.

[Ilmārs Cīrulis]

In this specific case the following proof that avoids ring works too, but in more complex situations automation offered by ring is probably the best option.

import Mathlib

example (N x : ℝ) (hx : x ^ 3 = N) : x ^ 9 = N * (N * N) := by
  rw [← hx, ← pow_add, ← pow_add]

[Eric Paul]

You can see the proof that grind generated as follows, although it is fairly large:

import Mathlib

example (N x : ℝ) (hx : x ^ 3 = N) : x ^ 9 = N * (N * N) := by?
  grind -abstractProof

[Yoh Tanimoto]

Eric Paul said:

You can see the proof that grind generated as follows, although it is fairly large:

When I click [apply], it gives errors...

[Vlad Tsyrklevich]

It's because the delaborator is not including all of the necessary type information. If you instead click apply on this even more awful term, it will succeed.

import Mathlib

set_option pp.all true
example (N x : ℝ) (hx : x ^ 3 = N) : x ^ 9 = N * (N * N) := by?
  grind -abstractProof

[Bbbbbbbbba]

Thanks a lot! All your answers helped in different ways.

[Nick Adfor]

Well, I want grind to have something like grind? and generate rw… or simp…

[Nick Adfor]

But the grind -abstractProof can only show large abstractProof without mathematical meaning :(

[Henrik Böving]

The best you will get is the grind? grind mode output which in your case becomes:

example (N x : ℝ) (hx : x ^ 3 = N) : x ^ 9 = N * (N * N) := by?
  grind => ring

For non trivial coals grind would produce a more verbose proof. Emitting rw or simp style proofs would not be efficient for grind. It operates based on very different data structures internally and enforces a lot of assumptions about the shape that the goal it is working on is in. You don't just get these assumptions in general tactic mode.