How `intro` works with mvars

Stream: metaprogramming / tactics

[Chase Norman]

The tactic intro x makes it seem like we assigned the main goal to fun x => ?M for some new metavariable ?M which contains x in the local context. This metavariable is the goal state after the tactic. However, it appears this is not possible, as x would need to be a bvar for ?M, not an fvar. Here's an experiment I ran with mkLetFVars, which is used in the implementation of intro:

import Lean
open Lean Meta Expr

#eval (do
  let goal ← mkFreshExprMVar (mkConst ``Nat)
  withLetDecl `test (mkConst ``Nat) (← mkFreshExprMVar (mkConst ``Nat)) fun fvar => do
    let inner ← mkFreshExprMVar (mkConst ``Nat)
    dbg_trace inner
    -- ?_uniq.22524
    goal.mvarId!.assign (← mkLambdaFVars #[fvar] (usedLetOnly := false) inner)
    dbg_trace (← instantiateMVars goal)
    -- let test : Nat := ?_uniq.22522; ?_uniq.22525
    inner.mvarId!.assign fvar
    dbg_trace (← instantiateMVars goal)
    -- let test : Nat := ?_uniq.22522; ?_uniq.22525
)

Rather than assigning goal to a let definition with body inner, it creates a new metavariable that does not respond to updates in inner. This is sensible, but it implies that the tactics after intro have to be evaluated first, before the mkLambdaFVars is applied. This is surprising to me, as I thought tactics were run in order.

My main question is: is it possible to create a function that assigns a metavariable to a let definition of other metavariables, where the latter has an extended local context, and where assignments of those metavariables would be propagated?

[Aaron Liu]

this is the delayed assignment thing

[Aaron Liu]

tactics are run in order I'm pretty sure

[Aaron Liu]

it's just delayed assigned mvars are weird

[Aaron Liu]

Chase Norman said:

My main question is: is it possible to create a function that assigns a metavariable to a let definition of other metavariables, where the latter has an extended local context, and where assignments of those metavariables would be propagated?

can you give some pseudocode of what you want to assign

[Chase Norman]

import Lean
open Lean Meta Expr

def assignLet (mvar : MVarId) (name : Name) (type : Expr) : MetaM (MVarId × MVarId) := do
  let value ← mkFreshExprMVar type
  withLetDecl name type value fun fvar => do
    let body ← mkFreshExprMVar (← mvar.getType)
    mvar.assign (← mkLambdaFVars #[fvar] (usedLetOnly := false) value)
    return (body.mvarId!, value.mvarId!)

[Chase Norman]

I want this but something that would actually work

[Chase Norman]

Just edited it to return the new mvars

[Chase Norman]

The idea would be that then you could present these mvars to a user, and they would be assigned later

[Aaron Liu]

ok now I'm confused this mvar is weird

[Aaron Liu]

the mvar structure has some questionable design choices

[Aaron Liu]

I think you assigned an mvar that was already assigned and that's why it wasn't updating

[Aaron Liu]

specifically, the mkLambdaFVars in your first example assigned inner

[Aaron Liu]

so when you assigned it again it broke the thing

[Chase Norman]

That appears to be true. I want inner to be just like what intro does, unassigned and presentable to a user for assignment.

[Aaron Liu]

look it's already assigned

import Lean
open Lean Meta Expr

#eval (do
  let goal ← mkFreshExprMVar (mkConst ``Nat)
  withLetDecl `test (mkConst ``Nat) (← mkFreshExprMVar (mkConst ``Nat)) fun fvar => do
    let inner ← mkFreshExprMVar (mkConst ``Nat)
    dbg_trace inner
    -- ?_uniq.22524
    goal.mvarId!.assign (← mkLambdaFVars #[fvar] (usedLetOnly := false) inner)
    dbg_trace (← instantiateMVars goal)
    -- let test : Nat := ?_uniq.22522; ?_uniq.22525
    dbg_trace ← inner.mvarId!.isAssigned
    -- true
)

[Aaron Liu]

if you want it to not be assigned then maybe making it synthetic opaque will do something

[Aaron Liu]

since that's what tactics work on

[Aaron Liu]

docs#Lean.MetavarKind.syntheticOpaque

[Chase Norman]

This is progress:

let test : Nat := ?_uniq.2026; ?_uniq.2029 test
let test : Nat := ?_uniq.2026; test

[Chase Norman]

I guess you can't expect the top to read just ?inner because that breaks the Expr invariant

[Aaron Liu]

wait what's the expr invariant

[Chase Norman]

That test should be bound in the body

[Chase Norman]

Meaning any mvar that uses it has to be passed it as an argument

[Chase Norman]

Is there a way to instantiateMVars that also greedily instantiates delayed mvars? It would be nice to be able to show the partial assignment, even though there are still mvars around

[Aaron Liu]

nope can't find anything

[Aaron Liu]

there is a pp option pp.mvars.delayed

[Aaron Liu]

it seems to be doing something

[Chase Norman]

I see no effect