Qq context in run_tac

Stream: metaprogramming / tactics

[Mirek Olšák]

I thought it could be qute, if the run_tac script directly obtained context from the proof state in the form of expressions, or even better quoted expressions. I could get bare expressions working. I thought I could also get quoted expressions by replacing q(Expr) with q(Quoted $t) but that just breaks everything. Am I missing something simple, or is there a deeper difficulty?

import Lean
import Qq

open Lean Meta Elab Tactic Qq

elab "run_taq" e:doSeq : tactic => do
    let lctx ← getLCtx
    let mut metaCtx := LocalContext.empty
    let mut fs : Array Expr := #[]
    for decl in lctx do
      if decl.kind != default then continue
      let fid : FVarId := decl.fvarId -- reuse the same fvarId, hopefully ok
      let f : Expr := (Expr.fvar fid)
      let t : Expr := decl.type
      let metaDecl := LocalDecl.ldecl
        metaCtx.size fid decl.userName
        q(Expr) q($f)
        true default
      metaCtx := metaCtx.addDecl metaDecl
      fs := fs.push f
    let typeExpr := (mkApp (Lean.mkConst ``TacticM) (Lean.mkConst ``Unit))
    let tacExpr : Expr ← withLCtx metaCtx #[] do
      let body ← Term.elabTerm (← `(discard do $e)) typeExpr
      mkLetFVars fs body
    let tac ← unsafe evalExpr (TacticM Unit) typeExpr tacExpr
    tac

example (a b : Nat) (h : a = b) : True := by
  run_taq
    have a : Q(Nat) := a
    logInfo "a"
    have b : Q(Nat) := b
    have h : Q($a = $b) := h
    have p : Q(Prop) := q($a = $b)
    let t ← inferType h
    logInfo t
    logInfo a
    logInfo h
    logInfo p
    logInfo <| toString p
    logInfo <| toString <| ← isDefEq p t
  trivial

[Mirek Olšák]

Ok, I was a bit too naive -- Qq builds references to external variables differently than just by quoting an Expr. Now I am thinking of using Qq.Impl.quoteExpr with carefully setting the exprBackSubst, I will let know when I get it working.

[Eric Wieser]

To check I understand, you want run_tacq to create a meta-time context with quoted copies of each variable?

[Eric Wieser]

I think you need to insert a have rather than a let

[Eric Wieser]

Ultimately though I think this is a great idea, though probably this makes more sense as a by_elabQ in MetaM Q(expected_type)

[Mirek Olšák]

Eric Wieser said:

I think you need to insert a have rather than a let

That might turn out to be necessary, I was experimenting with cdecl instead of ldecl too. The have analogue to mkLetFVars, is just mkLambdaFVars & mkAppN?

[Mirek Olšák]

But first, I need to quote the expression correctly.

[Mirek Olšák]

Eric Wieser said:

Ultimately though I think this is a great idea, though probably this makes more sense as a by_elabQ in MetaM Q(expected_type)

Sure, by_elab could have this feature too, so it makes sense to write a code generally to support both cases. Originally, I just wanted it for more convenient experiments in TacticM.

[Eric Wieser]

Here's a cdecl version:

elab "run_taq" e:doSeq : tactic => do
    let lctx ← getLCtx
    let mut metaCtx := LocalContext.empty
    let mut fs : Array Expr := #[]
    let mut vals : Array Expr := #[]
    for decl in lctx do
      if decl.kind != default then continue
      let fid : FVarId ← mkFreshFVarId
      let f : Expr := (Expr.fvar fid)
      let t : Expr := decl.type
      let metaDecl := LocalDecl.cdecl
        metaCtx.size fid decl.userName
        q(Expr)
        default default
      metaCtx := metaCtx.addDecl metaDecl
      fs := fs.push f
      vals := vals.push (.fvar decl.fvarId)
    let tacExpr : Expr ← withLCtx metaCtx #[] do
      let body ← Term.elabTerm (← `(discard do $e)) q(TacticM Unit)
      mkLambdaFVars fs body
    let tacExpr := mkLambda `fvars default q(Array Expr) <|
      let arg : Q(Array Expr) := Expr.bvar 0
      mkAppN tacExpr (fs.mapIdx fun (i : Nat) _ => q($arg[$i]!))
    Lean.logInfo tacExpr
    let tac ← unsafe evalExpr (Array Expr → TacticM Unit) q(Array Expr → TacticM Unit) tacExpr
    tac vals

[Eric Wieser]

Note that you'll want to translate lets in the goal state into ldecls, but you certainly want to go through the Qq internals to get there

[Eric Wieser]

(edit: fixed above)

[Eric Wieser]

Certainly to make Quoted $t work you need to back-substitute t with the variables you've created so far

[Robin Arnez]

Also, use mkLocalDecl instead of addDecl

[Robin Arnez]

Here is my implementation of by_elabq:

import Lean
import Qq

open Lean Meta Elab Tactic Qq

elab "by_elabq" e:doSeq : tactic => withMainContext do
  let lctx ← getLCtx
  let mut metaCtx := LocalContext.empty
  let mut assignments : Array Expr := ∅
  let mut levelSubst : Std.HashMap Level Expr := ∅
  for nm in (← Term.getLevelNames) do
    let fid ← mkFreshFVarId
    let metaDecl := LocalDecl.cdecl
      metaCtx.size fid nm
      q(Level) .default .default
    metaCtx := metaCtx.addDecl metaDecl
    levelSubst := levelSubst.insert (.param nm) (.fvar fid)
    assignments := assignments.push (toExpr (Level.param nm))
  let mut exprSubst : Std.HashMap Expr Qq.Impl.ExprBackSubstResult := ∅
  for decl in lctx do
    if decl.kind != .default then continue
    let fid ← mkFreshFVarId
    let type ← instantiateMVars decl.type
    let quotedType ← (Qq.Impl.quoteExpr type).run {
      exprBackSubst := exprSubst,
      levelBackSubst := levelSubst
      mayPostpone := false
    }
    metaCtx := metaCtx.mkLocalDecl fid decl.userName
      (mkApp (mkConst ``Quoted) quotedType) decl.binderInfo
    assignments := assignments.push (toExpr (Expr.fvar decl.fvarId))
    if decl.isLet then
      let eqFid ← mkFreshFVarId
      let level ← getLevel type
      let quotedLevel ← (Qq.Impl.quoteLevel (← instantiateLevelMVars level)).run {
        exprBackSubst := exprSubst,
        levelBackSubst := levelSubst
        mayPostpone := false
      }
      let quotedValue ← (Qq.Impl.quoteExpr (← instantiateMVars decl.value)).run {
        exprBackSubst := exprSubst,
        levelBackSubst := levelSubst
        mayPostpone := false
      }
      metaCtx := metaCtx.mkLocalDecl eqFid (← mkFreshUserName `eq)
        (mkApp4 (mkConst ``QuotedDefEq) quotedLevel quotedType (.fvar fid) quotedValue)
      assignments := assignments.push
        (mkApp4 (mkConst ``QuotedDefEq.unsafeIntro) quotedLevel quotedType (.fvar fid) quotedValue)
    exprSubst := exprSubst.insert (.fvar decl.fvarId) (.quoted (.fvar fid))
  let goalType ← instantiateMVars (← (← getMainGoal).getType)
  let quotedGoal ← (Qq.Impl.quoteExpr goalType).run {
    exprBackSubst := exprSubst,
    levelBackSubst := levelSubst
    mayPostpone := false
  }
  let quotedGoalType := mkApp (mkConst ``TacticM) (mkApp (mkConst ``Quoted) quotedGoal)
  let tacExpr : Expr ← withLCtx metaCtx #[] do
    let body ← Term.elabTermAndSynthesize (← `(do $e)) quotedGoalType
    let res ← metaCtx.foldrM (init := (assignments, body)) fun decl (assignments, body) => do
      let value := assignments.back!
      let result := .letE decl.userName decl.type value (body.abstract #[.fvar decl.fvarId]) false
      return (assignments.pop, result)
    return res.2
  unless tacExpr.hasMVar do
    let typeExpr := (mkApp (Lean.mkConst ``TacticM) (Lean.mkConst ``Expr))
    let tac ← unsafe evalExpr (TacticM Expr) typeExpr tacExpr
    let val ← tac
    (← getMainGoal).assign val

example (a b : Nat) (h : a = b) : True := by
  by_elabq
    return q(trivial)

[Robin Arnez]

When you look at the expected type you get something like

u : Level
α : Q(Type u)
a b : Q(«$α»)
h : Q(«$a» = «$b»)
⊢ TacticM Q(True)

[Robin Arnez]

for

example {α : Type u} (a b : α) (h : a = b) : True := by
  by_elabq
    return q(trivial)

[Eric Wieser]

This is really excellent Robin!

[Eric Wieser]

I think probably this makes sense to Pr to Qq, since it relies on implementation details of Qq itself?

[Eric Wieser]

As a nit, things like (mkApp (Lean.mkConst ``TacticM) (Lean.mkConst ``Expr)) can be golfed to q(TacticM Expr)

[Aaron Liu]

That's great, but what about non-finishing tactics?

[Eric Wieser]

I think probably the signature of those should be

u : Level
α : Q(Type u)
a b : Q(«$α»)
h : Q(«$a» = «$b»)
⊢ Q(True) -> TacticM Unit

(where the Q(True) is the goal metavariable to be assigned)

[Eric Wieser]

by_elabq should probably live in TermElabM or even MetaM. I think there's probably some inspiration to be had from docs#Lean.Elab.Tactic.liftMetaFinishingTactic and docs#Lean.Elab.Tactic.liftMetaTactic for what the API should look like

[Eric Wieser]

Really what we're doing is providing a Qq-ified version of those

[Robin Arnez]

Hmm so then the idea is to use it like this?

example {α : Type u} (a b : α) (h : a = b) : True := by
  by_elabq fun goal => do
    let _ ← assertDefEqQ goal q(trivial)
    return []

[Robin Arnez]

Oh wow no there is a bug with this (the fact that it doesn't throw an error)

[Robin Arnez]

Screenshot 2025-06-27 161210.png
It doesn't assign the meta-variable but pretends to have done so

[Robin Arnez]

oh wait no proof irrelevance

[Robin Arnez]

weird stuff

[Notification Bot]

Mirek Olšák has marked this topic as resolved.

[Mirek Olšák]

Thanks! I agree with Eric that if this gets into Qq, it will be great. My understanding is that there should be two elaborators -- by_elabq, and run_tacq. The first runs in TermElabM allowing something like

def f (x : Bool) : Rat :=
  by_elabq return q(if $x then 2 else 3)

and the second would run in TacticM and ignores its return value, like run_tac allowing something like

example (a b : Nat) (h : a = b) : True := by
  by_elabq
    let p := q($a = $b)
    let t ← inferType h
    logInfo <| toString (← isDefEq t p)
    logInfo <| toString (← isDefEq h.ty p)
  trivial

I think with your example, I would manage to write it, but I am happy to leave it for you.

[Aaron Liu]

Robin Arnez said:

Screenshot 2025-06-27 161210.png
It doesn't assign the meta-variable but pretends to have done so

assertDefEqQ won't assign synthetic opaque metavariables

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

One difference with run_tac is that run_tacq only runs on the first goal

[Aaron Liu]

Maybe just pass the goal list?

[Eric Wieser]

But the hypotheses only exist in a single goal

[Eric Wieser]

I think perhaps we don't need new "context-switching" elaborators at all, and should instead have a with_contextQ% => and with_contextQ% goal => elaborators that can be used inside by_elab and run_tac?

[Robin Arnez]

There is no goal state context though when elaborating the body of run_tac or by_elab

[Mirek Olšák]

I feel that making run_tac to choose the goal for its context is a bit over-complicated. When I want another goal, I can run case', or rotate_left. Even the Q-annotated goal is not a must-have feature, but I understand its beauty.

[Mirek Olšák]

I made the PR
https://github.com/leanprover-community/quote4/pull/88

[Eric Wieser]

I was unclear; the goal above was intended to be the variable name introduced to hold the goal state, not as a selector to choose the goal

[Aaron Liu]

Eric Wieser said:

I was unclear; the goal above was intended to be the variable name introduced to hold the goal state, not as a selector to choose the goal

oh I thought it was a selector to choose the goal

[Eric Wieser]

Either way, easier to comment on the PR with what I actually meant

[Eric Wieser]

This is now available in mathlib master; thanks @Mirek Olšák and @Robin Arnez!

[Eric Wieser]

https://github.com/leanprover-community/quote4/pull/90 has a small follow-up, since I couldn't remember the name of this API during review