Collect used external fvars in tactics block

Stream: metaprogramming / tactics

[Yiming Fu]

Hi everyone,
I want to collect which external FVars (from before a tactic block) are actually used inside the block.

import Lean
open Lean Elab Tactic

elab "trace_fvars" "{" seq:tacticSeq "}" : tactic => do
  let goalbefore ← getMainGoal
  evalTactic seq
  let goalafter ← getMainGoal
  let UsedExternalFvars : Array FVarId := sorry
  for fvars in UsedExternalFvars do
    logInfo m!"{← fvars.getUserName}"
  sorry

example (n : Nat) (unused : 1 = 1) : ∃ f : Nat → Nat, f (n + (1) ^ 2) = n + 1 := by
  let g : Nat → Nat := fun x => x
  have hg : ∀ x, g x = x := by
    intro x
    rfl
  have : 1 ^ 2 = 1 := by rfl
  -- tactic block begins -- use `trace_fvars {}` here
  let f := fun (x : Nat) => x
  refine ⟨f, ?_⟩
  rewrite [this]
  /-
  n : Nat
  unused : 1 = 1
  g : Nat → Nat := fun x => x
  hg : ∀ (x : Nat), g x = x
  this : 1 ^ 2 = 1
  f : Nat → Nat := fun x => x -/
  -- end
  rfl

Here, the external FVars (n, unused, g, hg, this) exist before the block, but in this block n, this are actually used. I want to get usedExternalFVars : Array FVarIdthat contains exactly the external FVars used in the block. Specifically, I have two questions:

1. How to get the "external FVars" (those in the context before the block).
2. How to get the FVars actually used in a tactic block.

[Jovan Gerbscheid]

It is a bit tricky. The way to do it is to take the initial goal, and then instantiate metavariables in it after executing the tactic sequence. Then we can look in the proof term to see what free variables are there.

Due to delayed assigned metavariables, instantiateMVars may not do anything where we want it. As a workaround, we can instantiate the remaining goals with default.

import Lean
open Lean Elab Tactic

elab "trace_fvars" "{" seq:tacticSeq "}" : tactic => withMainContext do
  let goalsBefore ← getGoals
  evalTactic seq
  let goalsAfter ← getGoals
  Meta.withoutModifyingMCtx do
  for goal in goalsAfter do
    goal.assign default
  let mut fvarsState : CollectFVars.State := {}
  for goal in goalsBefore do
    logInfo m!"{goal}"
    fvarsState := collectFVars fvarsState (← instantiateMVars (.mvar goal))
  let UsedExternalFvars := fvarsState.fvarIds
  logInfo m!"{UsedExternalFvars.map (Expr.fvar ·)}"


example (n : Nat) (unused : 1 = 1) : ∃ f : Nat → Nat, f (n + (1) ^ 2) = n + 1 := by
  let g : Nat → Nat := fun x => x
  have hg : ∀ x, g x = x := by
    intro x
    rfl
  have : 1 ^ 2 = 1 := by rfl
  -- tactic block begins -- use `trace_fvars {}` here
  trace_fvars {
  let f := fun (x : Nat) => x
  refine ⟨f, ?_⟩
  rewrite [this]
  }
  rfl

[Yiming Fu]

Great! I didn’t even think about the delayed metavariable issue. Thanks!