Multiply delayed assignments?

Stream: lean4 dev

[Rish Vaishnav]

Hi, I've gotten sucked into the MetavarContext.lean file (I know it's "ancient" at this point haha, just really want to get a handle on something relating to metavariables before I move on to frontend stuff) and I understand most of the motivation behind the code there at this point. One thing that has puzzled me a bit however, is this part of elimMVar:

/- If `mvarId` is the lhs of a delayed assignment `?m #[x_1, ... x_n] := ?mvarPending`,
   then `nestedFVars` is `#[x_1, ..., x_n]`.
   In this case, `newMVarId` is also `syntheticOpaque` and we add the delayed assignment delayed assignment
   ```
   ?newMVar #[y_1, ..., y_m, x_1, ... x_n] := ?m
   ```
   where `#[y_1, ..., y_m]` is `toRevert` after `collectForwardDeps`.
-/
let (mvarIdPending, nestedFVars) ← match (← getDelayedMVarAssignment? mvarId) with
  | none => pure (mvarId, #[])
  | some { fvars, mvarIdPending } => pure (mvarIdPending, fvars)
assignDelayedMVar newMVarId (toRevert ++ nestedFVars) mvarIdPending

Like, I understand exactly what we're doing here -- we're just extending the free variables that come from the original delayed assignment with toRevert from this one, and then associating it with the same underlying original metavariable. And I know how this case can arise in terms of how the function is called, if we call it first on a syntheticOpaque metavar with some free variables xs in the context, and then call it later on the resulting delayed assigned metavariable with a set of free variables ys that includes some free variables not in xs. I'm just trying to wrap my head around when exactly this would arise. Are there any MWEs you know of that fall into this case? Also having some concrete examples to walk through would really help me out with my understanding of this file hahaha. Thanks!

[Rish Vaishnav]

(also lmk if this topic is better suited for the general Lean 4 stream, not sure if this is the right place for newbie questions relating to things not being actively developed atm)

[Leonardo de Moura]

@Rish Vaishnav Happy to do a walkthrough of the MetavarContext.lean in our next front-end meeting. It may also be a good opportunity to document the file better and simplify the implementation.
Not sure I fully understood the question, but I will try to give some pointers.

• Metavariables are holes/goals. They have a local context and a type. When we assign a value e to a metavariable ?m with local context ctx, all free variables in e must be in ctx.
• Synthetic opaque metavariables ?m are synthesized using procedures (e.g., by executing a tactic). These procedures may be on a to-do list, and are responsible for performing the assignment ?m := v
• When we create a (dependent) arrow or a lambda abstraction, we convert free variables into bound variables.
• Suppose we want to create a lambda abstraction using the term Nat.add x ?m by abstracting the free variable x. That is, we want to create fun x => Nat.add x ?m. Note that, the x in the body of the lambda is the bound variable Exp.bvar 0. Now, suppose that x is in the local context of ?m. Now, suppose later we assign ?m := x. We need to make sure that the free variable x also becomes Expr.bvar 0. Let's focus on the case ?m is a synthetic opaque metavariable. Then, we create a new metavariable ?n that does not contain the free variable x in its local context, and we add the delayed assignment ?n #[x] := ?m. We can view this delay assignment as follows: when ?m is assigned, abstract x and assign the result to ?n. Then, our resulting lambda is fun x => Nat.add x ?n.
• Now, suppose we want to construct fun y => fun x => Nat.add x ?n, and y is in the local context of ?n. This scenario will trigger the code in your message.

To trigger the scenario, we need

• An opaque synthetic metavariable, we can create one using tactics.
• Abstract a term containing the metavariable, and then abstract the term again.

[Leonardo de Moura]

Here is an artificial example to reach the branch

  | some { fvars, mvarIdPending } => pure (mvarIdPending, fvars)

Example:

example (x : True) : True :=
  have h : True → True := fun _ => by constructor
  h x

[Rish Vaishnav]

Thank you! Yes, a walkthough would be great, but no pressure at all if there's another topic more directly related to frontend that you wanted to talk about instead. I was just looking for a concrete example that would trigger it, so you've exactly answered my question :)

I'll have to think about that a bit more, but I'm guessing that the by constructor tactic is what introduces the synthetic opaque metavar here?

[Leonardo de Moura]

If we put an assert! false in the branch above. That is,

  | some { fvars, mvarIdPending } => assert! false; pure (mvarIdPending, fvars)

and then execute the example in the debugger with LEAN_ABORT_ON_PANIC set,

~/projects/lean4/build/release (master) $ LEAN_ABORT_ON_PANIC=1 gdb stage1/bin/lean
...
(gdb) run  mvarEx.lean

Where mvarEx.lean contains the example above, we get a stack trace

Starting program: /home/leodemoura/projects/lean4/build/release/stage1/bin/lean mvarEx.lean
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
PANIC at _private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elimMVar Lean.MetavarContext:1075:45: assertion violation: false
backtrace:
/home/leodemoura/projects/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0xa3)[0x7ffff7b21a33]
/home/leodemoura/projects/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimMVar___spec__6+0x19)[0x7ffff78a59f9]
...
/home/leodemoura/projects/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_mkLambdaFVars+0x400)[0x7ffff69049f0]
...
/home/leodemoura/projects/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabMutualDef_go___lambda__3+0x3
...

That is, we got the assertion when trying to abstract the (x : True) here
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/MutualDef.lean#L248

[Leonardo de Moura]

I'll have to think about that a bit more, but I'm guessing that the by constructor tactic is what introduces the synthetic opaque metavar here?

Correct.

[Leonardo de Moura]

The first abstraction occurs at fun _ => by constructor, and the second when abstracting (x : True).

[Rish Vaishnav]

Thank you very much! I'm going to give this another pass tomorrow, and try out that gdb run for myself.

[Rish Vaishnav]

Leonardo de Moura said:

Here is an artificial example to reach the branch

  | some { fvars, mvarIdPending } => pure (mvarIdPending, fvars)

Example:

example (x : True) : True :=
  have h : True → True := fun _ => by constructor
  h x

Is there some code/documentation I can read into to better understand the process/rationale of creating an opaque synthetic metavariable here?

[Leonardo de Moura]

@Rish Vaishnav I am not exactly sure what the question is. We can start the next frontend meeting (on Tuesday) discussing that. I think this is an important topic, and we would all benefit from additional documentation.

[Rish Vaishnav]

No worries! Yes that sounds like a great plan for Tuesday.

[Rish Vaishnav]

I suppose I could rephrase my question as: which file is the logic that makes a synthetic opaque metavar for the by constructor tactic in the example above defined in? Is that part of the logic for the constructor tactic itself, or the more general tactic framework?

[Rish Vaishnav]

(go-to-definition on constructor didn't work for me)

[Leonardo de Moura]

The constructor tactic is a small wrapper around apply https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Constructor.lean#L25
The apply tactic is creating the opaque metavariables here: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Apply.lean#L140

[Rish Vaishnav]

Ah, thank you! I'll investigate those files.