partially resolve mvars in expression

Stream: lean4

[Tomas Skrivan]

I have an expression containing meta variables but some of them can be resolved. How can I do that?

Example: let's have x : X and expression @Prod.mk ?α ?β x ?b. It can be inferred that ?α = X. How can I do that?

mwe

import Lean
open Lean Meta

#eval show MetaM Unit from do
  let u ← mkFreshLevelMVar
  let v ← mkFreshLevelMVar
  let α ← mkFreshExprMVar (mkSort u) (userName := `α)
  let β ← mkFreshExprMVar (mkSort v) (userName := `β)
  let b ← mkFreshExprMVar β (userName := `b)
  withLocalDeclD `x (.const ``Nat []) fun x => do
    let e := mkAppN (.const `Prod.mk [u,v]) #[α,β,x,b]

    -- what to do here? Such that the next line prints `Nat`

    IO.println (← ppExpr (← instantiateMVars α))

[Joachim Breitner]

It seems that running check will instantiate these. Note that you got the level off by one:

import Lean
open Lean Meta

#eval show MetaM Unit from do
  let u ← mkFreshLevelMVar
  let v ← mkFreshLevelMVar
  let α ← mkFreshExprMVar (mkSort u.succ) (userName := `α)
  let β ← mkFreshExprMVar (mkSort v.succ) (userName := `β)
  let b ← mkFreshExprMVar β (userName := `b)
  withLocalDeclD `x (.const ``Nat []) fun x => do
    let e := mkAppN (.const `Prod.mk [u,v]) #[α,β,x,b]
    check e
    -- what to do here? Such that the next line prints `Nat`

    IO.println (← ppExpr (← instantiateMVars α))

[Mario Carneiro]

I think mkAppM will unify the types, and unlike check it doesn't recursively re-check the arguments, it just does enough to ensure the application is well typed if the arguments are

[Tomas Skrivan]

I have hard time using mkAppM in my use-case as it accepts only explicit arguments.

Also check does not work in my use-case, but so far I'm unable to minimize the problem.

[Damiano Testa]

There are also docs#Lean.Meta.mkAppOptM and docs#Lean.Meta.mkAppOptM' allowing you to pass implicit arguments, in case this is helpful.

[Tomas Skrivan]

Ok this works for me:

  let type ← instantiateMVars (← inferType thm.proof)
  let mut (xs, bis, type) ← forallMetaTelescope type

  -- fix some arguments of a theorem
  xs[id_f]!.mvarId!.assign f
  xs[id_g]!.mvarId!.assign g

  -- force some mvars to be resolved
  let prf ← mkAppOptM' (thm.proof) (xs.map .some)
  check prf

Actually, this might be XY problem. I want to apply a theorem and to make unification easier/succeed I want to manually set some arguments of the theorem.

[Tomas Skrivan]

Also mkAppOptM does not work as I would hope here, calling let e ← mkAppOptM ``Prod.mk (#[α,β,x,b].map .some) in the original example gives an error

application type mismatch
  Prod.mk x
argument
  x
has type
  Nat : Type
but is expected to have type
  ?α : Type ?u.1

[Mario Carneiro]

do those actually unify if you use isDefEq?

[Mario Carneiro]

It might be that it doesn't unify because you are at the wrong mvar depth or the universe variable is not assignable or something

[Kyle Miller]

mkAppOptM can't assign to pre-existing metavariables because it bumps up the metavariables depth, right?

[Mario Carneiro]

how would it ever work in that case then?

[Mario Carneiro]

(not saying you are wrong, I have seen issues of this kind before)

[Kyle Miller]

I think a mental model for mkAppM and mkAppOptM is that they do a meta telescope on the function's type, then unify each provided argument with a respective metavariable, and then do instance synthesis as for the instance arguments. (That's just a mental model because they're written in a more optimized way.)

[Kyle Miller]

And the metavariables created by the meta telescope are at a higher depth, and the isDefEq checks are also done in this higher depth.

[Kyle Miller]

(I never remember exactly what can unify with what when there are varying depths though.)

[Mario Carneiro]

From that description it sounds like mkAppOptM f (args.map some) will indeed be equivalent to mkAppN f args, except that it fails if the types don't match

[Mario Carneiro]

that's awkward since it means that if you want the mvar to unify you have to pass none, but in that case you don't have the mvar afterward unless you look in the resulting expression

[Kyle Miller]

Here's the code done in an explicit way using a meta telescope and doing isDefEq directly, which works fine:

import Lean
import Std.Tactic.Exact

open Lean Meta

#eval show MetaM Unit from do
  let u ← mkFreshLevelMVar
  let v ← mkFreshLevelMVar
  let α ← mkFreshExprMVar (mkSort u) (userName := `α)
  let β ← mkFreshExprMVar (mkSort v) (userName := `β)
  let b ← mkFreshExprMVar β (userName := `b)
  withLocalDeclD `x (.const ``Nat []) fun x => do
    let fn ← mkConstWithFreshMVarLevels ``Prod.mk
    let (mvars, _, _) ← forallMetaTelescope (← inferType fn)
    mvars[0]!.mvarId!.assignIfDefeq α
    mvars[1]!.mvarId!.assignIfDefeq β
    mvars[2]!.mvarId!.assignIfDefeq x
    mvars[3]!.mvarId!.assignIfDefeq b

    let e ← instantiateMVars (mkAppN fn mvars)

    IO.println s!"α = {← ppExpr α}"
    IO.println s!"e = {← ppExpr e}"
/-
α = Nat
e = (x, ?b)
-/

[Kyle Miller]

Mario Carneiro said:

From that description it sounds like mkAppOptM f (args.map some) will indeed be equivalent to mkAppN f args, except that it fails if the types don't match

I thought when you're in a higher metavariable context depth, then if isDefEq would need to assign a metavariable of a lower depth it fails. In Tomas's example, the problem is that mkAppN or mkAppOptN is needing to unify Nat with α, which in the context of these functions is at a lower metavariable context depth, so it fails.

[Tomas Skrivan]

Here is almost exactly what I'm trying to do. The main issue is to resolve the the type β in Continuous_comp

import Lean
import Qq
import Mathlib.Analysis.NormedSpace.ContinuousLinearMap

open Lean Meta Qq

variable {α : Type} {β : Type} {γ : Type} {δ : Type}

variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]

theorem Continuous_comp {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) :
    Continuous (fun x => g (f x)) :=
  continuous_def.2 fun _ h => (h.preimage hg).preimage hf

#eval show MetaM Unit from do

  let goal := q(Continuous fun x : ℝ => ((1:ℝ),(x,x)))
  let g := q(fun x : (ℝ×ℝ) => ((1:ℝ),x))
  let f := q(fun x : ℝ => (x,x))

  let info ← getConstInfo ``Continuous_comp

  let type ← instantiateMVars (← inferType info.value!)
  let mut (xs, bis, type) ← forallMetaTelescope type

  xs[6]!.mvarId!.assign g
  xs[7]!.mvarId!.assign f


  -- does not resolve ?β in Continuous_comp
  -- check (mkAppN info.value! xs)

  -- does resolve ?β in Continuous_comp
  -- let prf := (← instantiateMVars (← mkAppOptM' (info.value!) (xs.map .some)))
  -- check prf

  -- print `xs` and see if they have been resolved
  if ← isDefEq type goal then
    IO.println (← xs.mapM (fun x => pure x >>= instantiateMVars >>= ppExpr))

[Kyle Miller]

Note that assign just assigns. It doesn't do any isDefEq checks, which are necessary to propagate the assignment's type.

[Kyle Miller]

That's a reason I used std's assignIfDefeq

[Kyle Miller]

(There are probably a good number of meta bugs out there from assigning metavariables but not unifying types.)

[Tomas Skrivan]

Cool! using assignIfDefeq fixed all the issues I had and I do not have to use check anymore.

[Kyle Miller]

Added this problem to https://github.com/leanprover-community/mathlib4/wiki/Metaprogramming-gotchas

[Kyle Miller]

Incidentally, the documentation for docs#Lean.MVarId.assign seems to be misleading. It claims you should do isDefEq (mkMVar mvarId) x as a safer alternative, but this doesn't assign the metavariable if these are proofs (and I seem to remember that there was a case where the types don't get unified). Better is what assignIfDefeq does: check it's not already assigned, check isDefEq on the types, and then assign.

[Kyle Miller]

lean4#2054 issue

[Tomas Skrivan]

Thanks a lot for the explanation!

[Tomas Skrivan]

(deleted)