grind with expressions

Stream: lean4

[Marcus Rossel]

AFAIK, currently grind can only take constants as parameters. That is, the following won't work:

example (a : Nat) (h : ∀ x : Nat, x = x) : a = a := by
  grind [h a]
        --^^
/- unexpected identifier; expected ']' -/

However, in the definition of docs#Lean.Meta.Grind.EMatchTheorem:

structure EMatchTheorem where
  /--
  It stores universe parameter names for universe polymorphic proofs.
  Recall that it is non-empty only when we elaborate an expression provided by the user.
  When `proof` is just a constant, we can use the universe parameter names stored in the declaration.
  -/
  levelParams : Array Name
  ...

... the comment on the field levelParams suggests that support for general expressions might be planned in the future? Is that so, or am I interpreting this comment incorrectly?

[Théophile]

I encountered the same limitation, but have relied on the following workaround which worked well in my use cases:

example (a : Nat) (h : ∀ x : Nat, x = x) : a = a := by
  have := h a
  grind

(in this case grind will work without the have, but it works in more complex examples)

[Kim Morrison]

We're planning to add support for this soon, but it's not ready yet. For now have is the workaround.

[Marcus Rossel]

This has now landed in the latest nightly :) https://github.com/leanprover/lean4-nightly/commit/47228b94fdc9a2c008ec83987f78221053ee258c