Force instantiate delay assigned metavariable

Stream: lean4

[Leni Aniva]

Is there a way to force all delay assigned metavariables to be instantiated?

For example, if I have an expression ?m.1 ?m.2, where

• ?m.2 is not instantiated
• ?m.1 is delay assigned to fun x => x + ?m.3
• ?m.3 is not instantiated
  Is there a way to convert the expression ?m.1 ?m.2 to ?m.2 + ?m.3 or (fun x => x + ?m.3) ?m.2? i.e. I want all metavariables to be "as instantiated as possible".

[Mario Carneiro]

does instantiateMVars not do that?

[Leni Aniva]

Mario Carneiro said:

does instantiateMVars not do that?

No. It seems like it only instantiates delay assigned metavariables that don't refer to other metavariables

[Jannis Limperg]

That's right. The transformation you suggest, where delayed-assigned mvars are replaced with an abstraction, might also be sound, but afaik it's not implemented anywhere.

[Joachim Breitner]

I was under the impression that delayed meta variables are always just substitutions of other meta variables, not terms like x + ?m. Am I wrong?

[Leni Aniva]

Joachim Breitner said:

I was under the impression that delayed meta variables are always just substitutions of other meta variables, not terms like x + ?m. Am I wrong?

In this case its fun x => x + ?m

[Joachim Breitner]

Then my understanding of delayed meta variables is still wanting :-)

[Leni Aniva]

Jannis Limperg said:

That's right. The transformation you suggest, where delayed-assigned mvars are replaced with an abstraction, might also be sound, but afaik it's not implemented anywhere.

so delay assigned metavariables can only be instantiated if they are fully resolved?

[Jannis Limperg]

That's my understanding, yes.

[Jannis Limperg]

That's my understanding, yes.

[Leni Aniva]

Is there a way to determine what metavariables must be resolved before a delay assigned metavariable can be instantiated?

[Leni Aniva]

For example if ?m := fun x => x + ?m.3 is delay assigned, then ?m depends on ?m.3

[Leni Aniva]

Jannis Limperg said:

That's right. The transformation you suggest, where delayed-assigned mvars are replaced with an abstraction, might also be sound, but afaik it's not implemented anywhere.

Would it be possible to write this transformation using the expression transform functions?

[Kyle Miller]

Yeah, you can force delayed assignment metavariables to make progress if they're partially assigned. There's nothing built-in, but it's not so hard to write the transformation.

import Lean

open Lean Meta

/--
Instantiate metavariables, including partially assigned delayed assignment metavariables.
-/
def semiInstantiateMVars (e : Expr) : MetaM Expr := do
  Meta.transform (← instantiateMVars e)
    (pre := fun e => e.withApp fun f args => do
      if let .mvar mvarId := f then
        if let some decl ← getDelayedMVarAssignment? mvarId then
          if args.size ≥ decl.fvars.size then
            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
            if !pending.isMVar then
              return .visit <| (← mkLambdaFVars decl.fvars pending).beta args
      return .continue)

elab "check " t:term : tactic => Elab.Tactic.withMainContext do
  let mut e ← Elab.Tactic.elabTerm t none
  if e.isFVar then
    if let some val ← e.fvarId!.getValue? then
      e := val
  logInfo m!"{e}"

elab "check' " t:term : tactic => Elab.Tactic.withMainContext do
  let mut e ← Elab.Tactic.elabTerm t none
  if e.isFVar then
    if let some val ← e.fvarId!.getValue? then
      e := val
  let e' ← semiInstantiateMVars e
  logInfo m!"{e'}"

example : True := by
  let h : ∀ x y : Nat, 1 + x = 1 + y := fun x y => ?foo
  case' foo => refine congrArg _ ?_
  rotate_left
  check h   -- fun x y ↦ ?m.4924 x y
  check' h  -- fun x y ↦ congrArg (HAdd.hAdd 1) (?m.4955 x y)
  trivial

[Kyle Miller]

I've only tested this with this one example, so there might be bugs.

[Leni Aniva]

Kyle Miller said:

Yeah, you can force delayed assignment metavariables to make progress if they're partially assigned. There's nothing built-in, but it's not so hard to write the transformation.

import Lean

open Lean Meta

/--
Instantiate metavariables, including partially assigned delayed assignment metavariables.
-/
def semiInstantiateMVars (e : Expr) : MetaM Expr := do
  Meta.transform (← instantiateMVars e)
    (pre := fun e => e.withApp fun f args => do
      if let .mvar mvarId := f then
        if let some decl ← getDelayedMVarAssignment? mvarId then
          if args.size ≥ decl.fvars.size then
            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
            if !pending.isMVar then
              return .visit <| (← mkLambdaFVars decl.fvars pending).beta args
      return .continue)

elab "check " t:term : tactic => Elab.Tactic.withMainContext do
  let mut e ← Elab.Tactic.elabTerm t none
  if e.isFVar then
    if let some val ← e.fvarId!.getValue? then
      e := val
  logInfo m!"{e}"

elab "check' " t:term : tactic => Elab.Tactic.withMainContext do
  let mut e ← Elab.Tactic.elabTerm t none
  if e.isFVar then
    if let some val ← e.fvarId!.getValue? then
      e := val
  let e' ← semiInstantiateMVars e
  logInfo m!"{e'}"

example : True := by
  let h : ∀ x y : Nat, 1 + x = 1 + y := fun x y => ?foo
  case' foo => refine congrArg _ ?_
  rotate_left
  check h   -- fun x y ↦ ?m.4924 x y
  check' h  -- fun x y ↦ congrArg (HAdd.hAdd 1) (?m.4955 x y)
  trivial

I tried this but sometimes it gives

PANIC at Lean.LocalContext.get! Lean.LocalContext:227:14: unknown free variable
backtrace:
.lake/build/bin/test(lean_panic_fn+0xa3)[0x61d100e1d643]
.lake/build/bin/test(l_Lean_MetavarContext_MkBinding_mkBinding___lambda__2+0x171)[0x61d0ffee65a1]
.lake/build/bin/test(lean_apply_1+0x260)[0x61d100e270c0]
.lake/build/bin/test(l_EStateM_bind___rarg+0x16)[0x61d100d9db66]
.lake/build/bin/test(lean_apply_1+0x15d)[0x61d100e26fbd]
.lake/build/bin/test(lean_apply_2+0xd36)[0x61d100e287d6]
.lake/build/bin/test(l_Lean_MetavarContext_mkBinding+0x1a2)[0x61d0ffee8e12]
.lake/build/bin/test(l_Lean_Meta_mkLambdaFVars+0x3a8)[0x61d0fefe8098]
.lake/build/bin/test(l_Lean_Expr_withAppAux___at_Pantograph_instantiatePartialDelayedMVars___spec__1+0x629)[0x61d0fd87a349]
.lake/build/bin/test(l_Pantograph_instantiatePartialDelayedMVars___lambda__1+0xc9)[0x61d0fd87a8c9]
.lake/build/bin/test(lean_apply_5+0x363)[0x61d100e2a9c3]
.lake/build/bin/test(lean_apply_6+0xb65)[0x61d100e2be45]
.lake/build/bin/test(l_ReaderT_bind___at_Lean_Meta_zetaReduce___spec__14___rarg+0xb7)[0x61d0ffd9cc37]
.lake/build/bin/test(lean_apply_6+0x3a5)[0x61d100e2b685]
.lake/build/bin/test(l_Lean_Meta_withIncRecDepth___at_Lean_Meta_zetaReduce___spec__15+0x45b)[0x61d0ffd9d5eb]
.lake/build/bin/test(l_Lean_Meta_transform_visit___at_Lean_Meta_zetaReduce___spec__2+0x859)[0x61d0ffd926c9]
.lake/build/bin/test(l_Array_mapMUnsafe_map___at_Lean_Meta_zetaReduce___spec__10+0x1ec)[0x61d0ffd98fcc]
.lake/build/bin/test(l_Lean_Expr_withAppAux___at_Lean_Meta_zetaReduce___spec__13+0xa6f)[0x61d0ffd9b94f]
.lake/build/bin/test(l_Lean_Meta_transform_visit___at_Lean_Meta_zetaReduce___spec__2___lambda__1+0x7e1)[0x61d0ffd9ee11]
.lake/build/bin/test(lean_apply_7+0x4e1)[0x61d100e2c3f1]
.lake/build/bin/test(l_ReaderT_bind___at_Lean_Meta_zetaReduce___spec__14___rarg+0x264)[0x61d0ffd9cde4]
.lake/build/bin/test(lean_apply_6+0x3a5)[0x61d100e2b685]
.lake/build/bin/test(l_Lean_Meta_withIncRecDepth___at_Lean_Meta_zetaReduce___spec__15+0x45b)[0x61d0ffd9d5eb]
.lake/build/bin/test(l_Lean_Meta_transform_visit___at_Lean_Meta_zetaReduce___spec__2+0x859)[0x61d0ffd926c9]
.lake/build/bin/test(l_Lean_Meta_transform___at_Lean_Meta_zetaReduce___spec__1+0xf6)[0x61d0ffda0246]

[Leni Aniva]

Is it always true that the free variables in the mvarIdPending mvar of a delay assigned mvar are either in the fvars list or in the local context of the caller context? If there is only a simple substitution involved here maybe I could use a function that replace the occurrence of mvars instead of Expr.beta?

[Leni Aniva]

In this case I found an example where the lctx has _uniq.63, and the fvars list of a delay assigned mvar has _uniq.80, but the pending mvar is assigned to Eq.{?_uniq.83} ?_uniq.87 ?_uniq.88 ?_uniq.89