MVars from implicit variables

Stream: lean4

[Adam Topaz]

I'm trying to get a variant of an apply at tactic to work. So far, I have the following:

import Mathlib.Tactic
import Lean

open Lean Meta Elab Tactic Term

/--
This function is similar to `forallMetaTelescopeReducingUntilDefEq` except that
it will construct mvars until it reaches one whose type is defeq to the given
type `t`. It uses `forallMetaTelescopeReducing`.
-/
def Lean.Meta.forallMetaTelescopeReducingUntilDefEq
    (e t : Expr) (kind : MetavarKind := MetavarKind.natural) :
    MetaM (Array Expr × Array BinderInfo × Expr) := do
  let mut mvs : Array Expr := #[]
  let mut bis : Array BinderInfo := #[]
  let (ms, bs, tp) ← forallMetaTelescopeReducing e (some 1) kind
  unless ms.size == 1 do throwError "Error"
  mvs := ms
  bis := bs
  let mut out : Expr := tp
  while !(← isDefEq (← inferType mvs.toList.getLast!) t) do
    let (ms, bs, tp) ← forallMetaTelescopeReducing out (some 1) kind
    unless ms.size == 1 do throwError "Error"
    mvs := mvs ++ ms
    bis := bis ++ bs
    out := tp
  return (mvs, bis, out)

namespace Mathlib.Tactic

elab "apply" t:term "at" i:ident : tactic => withMainContext do
  let f ← Term.elabTerm t none
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, _, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type
  let mainGoal ← getMainGoal
  let mainGoal ← mainGoal.tryClear ldecl.fvarId
  let mainGoal ← mainGoal.assert ldecl.userName tp (mkAppN f (mvs.pop.push ldecl.toExpr))
  let (_, mainGoal) ← mainGoal.intro1P
  replaceMainGoal <| [mainGoal] ++ mvs.pop.toList.map fun e => e.mvarId!

example {α β γ : Type*} (f : ∀ {a : α}, β → γ) (b : β) : γ := by
  apply f at b
  -- ⊢ γ
  sorry

I can't seem to figure out how to get a goal of type $\alpha$ in the example with the current code. What am I missing here? If sorry is replaced with assumption, an error pops us at f on the first line of the tactic block complaining that Lean doesn't know what to do with the term of alpha, as expected. How would I arrange for this to be an additional goal?

[Adam Topaz]

Are the metavariables introduced by forallMetaTelescopeReducing associated to implicit binders special somehow? Is that what's going on here?

[Damiano Testa]

Using

  apply @f at b

works...

More seriously, maybe if you carefully craft a mkAppOptM' application instead of your mkAppN one, it might work? You would have to inspect all the arguments to f and, for each, decide whether to pass it or not...

[Adam Topaz]

Right, I noticed that @f works. I want something similar to the behavior of the usual apply which introduces goals for implicit binders as well.

[Adam Topaz]

I'll take a look at mkAppOptM'. Thanks!

[Damiano Testa]

If you use f.getAppFn you might get closer to having a "meta" @f?

[Damiano Testa]

E.g., look at the error message with this:

  let mainGoal ← mainGoal.assert ldecl.userName tp (← mkAppOptM' f.getAppFn
    (#[some (← mkFreshExprMVar none)] ++ (mvs.pop.push ldecl.toExpr).map fun x => some x))


-- error:
/-
application type mismatch
  @f ?m.13218
argument
  ?m.13218
has type
  ?m.13217 : Sort ?u.13216
but is expected to have type
  α : Type u_1
-/

Is this progress?

[Adam Topaz]

Where is the @ elaborator defined?

[Damiano Testa]

I do not know...

[Adam Topaz]

Ah it's in Lean/Parser/Term.

[Adam Topaz]

well, the parser at least: docs#Lean.Parser.Term.explicit

[Adam Topaz]

LOL, here's a hack:

import Mathlib.Tactic
import Lean

open Lean Meta Elab Tactic Term

/--
This function is similar to `forallMetaTelescopeReducingUntilDefEq` except that
it will construct mvars until it reaches one whose type is defeq to the given
type `t`. It uses `forallMetaTelescopeReducing`.
-/
def Lean.Meta.forallMetaTelescopeReducingUntilDefEq
    (e t : Expr) (kind : MetavarKind := MetavarKind.natural) :
    MetaM (Array Expr × Array BinderInfo × Expr) := do
  let mut mvs : Array Expr := #[]
  let mut bis : Array BinderInfo := #[]
  let (ms, bs, tp) ← forallMetaTelescopeReducing e (some 1) kind
  unless ms.size == 1 do throwError "Error"
  mvs := ms
  bis := bs
  let mut out : Expr := tp
  while !(← isDefEq (← inferType mvs.toList.getLast!) t) do
    let (ms, bs, tp) ← forallMetaTelescopeReducing out (some 1) kind
    unless ms.size == 1 do throwError "Error"
    mvs := mvs ++ ms
    bis := bis ++ bs
    out := tp
  return (mvs, bis, out)

namespace Mathlib.Tactic

elab "apply" t:term "at" i:ident : tactic => withMainContext do
  let t ← `(@$t)
  let f ← Term.elabTerm t none
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, _, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type
  let mainGoal ← getMainGoal
  let mainGoal ← mainGoal.tryClear ldecl.fvarId
  let mainGoal ← mainGoal.assert ldecl.userName tp
    (← mkAppOptM' f (mvs.pop.push ldecl.toExpr |>.map fun e => some e))
  let (_, mainGoal) ← mainGoal.intro1P
  replaceMainGoal <| [mainGoal] ++ mvs.pop.toList.map fun e => e.mvarId!

example {α β γ : Type*} (f : ∀ {a : α}, β → γ) (b : β) : γ := by
  apply f at b
  sorry

[Damiano Testa]

I do not know if it is awesome or terrible that this works.

[Damiano Testa]

--  let t ← `(@$t)
  let f ← Term.elabTerm t none
  let f := f.getAppFn

[Adam Topaz]

oh, but that's not the intended behavior, I think. What if f is a partially applied function?

[Damiano Testa]

With this, I suspect that then you would have roll up your sleeves and collect all the previous arguments.

[Damiano Testa]

That could be information that the forallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEqforallMetaTelescopeReducingUntilDefEq gives back to you, along with everything else, maybe

[Damiano Testa]

In fact, a common situation would be one where f has some typeclass assumptions, so even if you do not want this tactic to be extra-robust, you are right that this is an issue that you need to address.

[Damiano Testa]

EDIT: this is nonsense!
Adam, maybe this is closer to what you wanted?

  let f := f.getAppFn
  let initial_args := f.getAppArgs
  let f := mkAppN f initial_args

[Damiano Testa]

It had not occurred to me until now that f and mkAppN f f.getAppArgs could not be the same expression.

[Damiano Testa]

This might be a way to build on Lean.MVarId.apply:

elab "apply" t:term "at" i:ident : tactic => withMainContext do
  let f ← Term.elabTerm t none
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, _, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type  -- no `mvs` needed
  let mainGoal ← (← getMainGoal).assert ldecl.userName tp f
  let (_, mainGoal) ← mainGoal.intro1P
  let gs ← mainGoal.apply f
  let gs := ← gs.mapM fun x => x.apply ldecl.toExpr <|> pure [x]
  replaceMainGoal <| gs.join

[Adam Topaz]

(deleted) sorry what I said was wrong... working on it now.

[Adam Topaz]

Sigh. I"m still confused:

import Mathlib.Tactic
import Lean

open Lean Meta Elab Tactic Term

/--
This function is similar to `forallMetaTelescopeReducingUntilDefEq` except that
it will construct mvars until it reaches one whose type is defeq to the given
type `t`. It uses `forallMetaTelescopeReducing`.
-/
def Lean.Meta.forallMetaTelescopeReducingUntilDefEq
    (e t : Expr) (kind : MetavarKind := MetavarKind.natural) :
    MetaM (Array Expr × Array BinderInfo × Expr) := do
  let mut mvs : Array Expr := #[]
  let mut bis : Array BinderInfo := #[]
  let (ms, bs, tp) ← forallMetaTelescopeReducing e (some 1) kind
  unless ms.size == 1 do throwError "Error"
  mvs := ms
  bis := bs
  let mut out : Expr := tp
  while !(← isDefEq (← inferType mvs.toList.getLast!) t) do
    let (ms, bs, tp) ← forallMetaTelescopeReducing out (some 1) kind
    unless ms.size == 1 do throwError "Error"
    mvs := mvs ++ ms
    bis := bis ++ bs
    out := tp
  return (mvs, bis, out)

namespace Mathlib.Tactic

elab "apply" t:term "at" i:ident : tactic => withMainContext do
  let f ← Term.elabTerm t none
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, _, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type
  logInfo m!"{mvs.size}"
  let mainGoal ← getMainGoal
  let mainGoal ← mainGoal.tryClear ldecl.fvarId
  let mainGoal ← mainGoal.assert ldecl.userName tp
    (← mkAppOptM' f (mvs.pop.push ldecl.toExpr |>.map fun e => some e))
  let (_, mainGoal) ← mainGoal.intro1P
  replaceMainGoal <| [mainGoal] ++ mvs.pop.toList.map fun e => e.mvarId!

example {α β γ : Type*} (f : {_ : α} → β → γ) (b : β) (a : α) : γ := by
  run_tac withMainContext do
    let lctx ← getLCtx
    let f ← lctx.findFromUserName? `f
    let b ← lctx.findFromUserName? `b
    let (mvs, _, tp) ← forallMetaTelescopeReducingUntilDefEq f.type b.type
    logInfo m!"{mvs.size}" -- 2
  apply f at b -- 1
  sorry

[Adam Topaz]

Ok, I think I minimized it down to the following:

import Mathlib.Tactic
import Lean

open Lean Meta Elab Tactic Term

def foo {n : Nat} (a : Nat × Nat) : Nat × Nat × Nat := (n,a)

example (bar : {n : Nat} → Nat × Nat → Nat × Nat × Nat) : True := by
  run_tac withMainContext do
    let foo ← Term.elabTerm (← `(foo)) none
    let fdecl ← (← getLCtx).findFromUserName? `bar
    let (mvs, _, tp) ← forallMetaTelescopeReducing (← inferType foo)
    let (mvs', _, tp') ← forallMetaTelescopeReducing fdecl.type
    logInfo m!"{mvs.size} {mvs'.size}" -- 1 2
    return
  sorry

I guess there's a difference in the behavior of forallMetaTelescopeReducing when applied to the type of an elaborated term vs. the type of a local declaration. I still don't really understand why this is the case. Can someone explain the difference between the two, just for my understanding?

[Adam Topaz]

Aha, I guess the following is the reason:

import Mathlib.Tactic
import Lean

open Lean Meta Elab Tactic Term

def foo : {_ : Nat} → Nat × Nat → Nat × Nat × Nat := fun {n} a => (n,a)

example (bar : {n : Nat} → Nat × Nat → Nat × Nat × Nat) : True := by
  run_tac withMainContext do
    let foo ← Term.elabTerm (← `(foo)) none
    let fdecl ← (← getLCtx).findFromUserName? `bar
    logInfo m!"{fdecl.type}" -- {n : ℕ} → ℕ × ℕ → ℕ × ℕ × ℕ
    logInfo m!"{← inferType foo}" -- ℕ × ℕ → ℕ × ℕ × ℕ
  sorry

So maybe the `($f) hack above wasn't so crazy?

[Adam Topaz]

I went with `($t): #7527

[Adam Topaz]

Damiano Testa said:

This might be a way to build on Lean.MVarId.apply:

elab "apply" t:term "at" i:ident : tactic => withMainContext do
  let f ← Term.elabTerm t none
  let ldecl ← (← getLCtx).findFromUserName? i.getId
  let (mvs, _, tp) ← forallMetaTelescopeReducingUntilDefEq (← inferType f) ldecl.type  -- no `mvs` needed
  let mainGoal ← (← getMainGoal).assert ldecl.userName tp f
  let (_, mainGoal) ← mainGoal.intro1P
  let gs ← mainGoal.apply f
  let gs := ← gs.mapM fun x => x.apply ldecl.toExpr <|> pure [x]
  replaceMainGoal <| gs.join

@Damiano Testa I'm confused about what you're trying to do here... in the assert step is it not the case that f needs to have type tp?

[Damiano Testa]

Adam, I think that has I answered this in the other thread. Briefly, I wanted to create new mvars, to then use Lean.MVarId.apply instead of mkAppWhatever.