Traversing the goal and local context

Stream: lean4

[Jason Rute]

I'm interested in traversing the goal (for the purpose of machine learning), including all the goal expressions and their local context expressions (at the level of Expr). I am very familiar with how to do this in Lean 3, but I'd like to know how to get started in Lean 4. Is there a good resource or example? Maybe the metaprogramming book? Or is the interface very similar to Lean 3, in which case I just need to map from my old code to the new API. Also, ideally, I'd like to take advantage of pointer-based optimizations, which I think Lean 4 has, to avoid traversing the same subexpression (if it uses the same pointer).

[Jason Rute]

To be more clear, I want to work in MetaM and write code to extract information from the current goal.

[Jason Rute]

Here is some old code I once used to gather this sort of data in Lean 3 (and serialize it to JSON).

[Jason Rute]

Maybe to make it more concrete:

1. How do I use MetaM to access the list of current goals (was tactic.get_goals in Lean 3)?
2. For each goal, how do I access their expressions and their local contexts?
3. Are there any data structures I should be aware of to accurately capture the goal state?
4. How do I traverse these structures with pointer optimization?

[Shreyas Srinivas]

see the examples in hitchhikers guide 2023 version

[Jason Rute]

Oh, actually the Tactics FAQ in the metaprogramming book seems to have exactly the answers to at least questions (1) and (2). Nice!

[Jason Rute]

Ok, those two books seem like a good start! I can't find stuff about pointer-based optimization in either, but that is probably premature optimization anyway.

[Kyle Miller]

Something you might be interested in is being able to completely extract the main goal's state as a single expression (including eliminating metavariables as additional function arguments).

import Lean

open Lean Meta

def captureGoal (g : MVarId) : MetaM Expr := g.withContext do
  let fvars ← (← g.getDecl).lctx.getFVars.filterM fun fvar => do
    return !(← fvar.fvarId!.getDecl).isImplementationDetail
  let ty ← mkForallFVars fvars (← g.getType)
  let res ← abstractMVars ty
  let ty := res.expr
  if true then
    logInfo m!"Universe level metavariables: {res.paramNames}\n{
      ""}Number of abstracted metavariables: {res.numMVars}\n{
      ""}Captured goal:{indentD ty}"
  return ty

elab "goal" : tactic => do
  let g ← Elab.Tactic.getMainGoal
  discard <| captureGoal g

example {α : Type _} (x y : Nat) (h : x = y) : let z := x + y; z = y + x := by
  intro z
  /-
  α : Type ?u.4868
  x y : Nat
  h : x = y
  z : Nat := x + y
  ⊢ z = y + x
  -/
  goal
  /-
  Universe level metavariables: [_abstMVar.0]
  Number of abstracted metavariables: 0
  Captured goal:
    ∀ {α : Type _abstMVar.0} (x y : Nat),
      x = y →
        let z := x + y;
        z = y + x
  -/

[Kyle Miller]

Here's an example of a complicated metavariable situation that it can handle, so you don't have to wade through all the MetaM state yourself.

example {α : Type _} : True := by
  have : (x : α) → ?_ := ?_
  /-
  α : Type ?u.4954
  this : (x : α) → ?m.4966 x
  ⊢ True
  -/
  set_option pp.funBinderTypes true in goal
  /-
  Universe level metavariables: [_abstMVar.0, _abstMVar.1]
  Number of abstracted metavariables: 1
  Captured goal:
    fun (x_0 : {α : Type _abstMVar.0} → α → Sort _abstMVar.1) ↦
      ∀ {α : Type _abstMVar.0}, ((x : α) → x_0 x) → True
  -/

[Kyle Miller]

Re traversing with optimizations, many core operations use a cache, and the Expr equality operation tries pointer equality first I believe (equality checking even uses a cache).