unify

Stream: metaprogramming / tactics

[Fabian Glöckle]

Hi, I seem to be unable to find this in the meta API:
Given an expr e and an expr M potentially containing metavariables, what is the library function which succeeds iff e and M unify under a suitable metavariable assignment? It does not seem to be tactic.unify, which fails e.g. on list nat and list A, A being a metavariable of type Type.
Or is this not what metavariables are made for / the elaborator is accessed differently / ... ?
(I am still an absolute metaprogramming newbie)

[Damiano Testa]

I'm also a newbie, so I do not really know an answer to your question. However, the code below did what I wanted and "unified metavariables":

open tactic

/-- A `tactic bool` computing whether the user-input `e` unifies with `e'`. -/
meta def expr.unify_with (e e' : expr) : tactic bool :=
succeeds $ unify e e'

[Damiano Testa]

This allowed me to pass _ * _ for instance and it unified with 3 * 4 and filled in the _ with a term of type nat.

[Damiano Testa]

However, in my use-case, the metavariables were explicit _, not some expr whose type I did not know. If this even makes sense...

[Fabian Glöckle]

Is _ the same thing as an expr.mvar?

[Henrik Böving]

_ will put a meta variable at the spot it's used yes.

[Fabian Glöckle]

meta def mk_mvar' (pp_name : name) (type : expr) : tactic expr := do
uniq_name ← mk_fresh_name,
return $ mvar uniq_name pp_name type

meta def mwe : tactic unit :=
do
  m ← mk_mvar' `M `(Type),
  n ← to_expr ``(_),
  trace (to_raw_fmt n),
  trace (to_raw_fmt m),
  unify n `(nat),
  unify m `(nat)

[Fabian Glöckle]

With output

(mvar _mlocal._fresh.2495.965 _mlocal._fresh.2495.965 (const 2 []))
(mvar _fresh.2495.962 M (sort 1))

and error

unify tactic failed, failed to unify
  M : Type
and
  ℕ : Type

[Fabian Glöckle]

Why is the type of the _ metavariable (const 2 [])?

[Damiano Testa]

If I understand correctly, the first unify succeeds: i.e. this works:

meta def mwe : tactic unit :=
do
  m ← mk_mvar' `M `(Type),
  n ← to_expr ``(_) tt ff,
  trace (to_raw_fmt n),
  trace (to_raw_fmt m),
  unify n `(nat)

[Fabian Glöckle]

Yes, the _ metavariable unifies, but my handcrafted one doesn't
The difference is the type of the expr.mvar
But I do not see why it should be (const 2 [])... ?!

[Fabian Glöckle]

@Jannis Limperg maybe? :)

[Damiano Testa]

Sorry, I am not sure that I can be of further/any help! I think that the _ is important and should be literally present, but I do not know. :shrug:

[Fabian Glöckle]

Damiano Testa said:

Sorry, I am not sure that I can be of further/any help! I think that the _ is important and should be literally present, but I do not know. :shrug:

Yes, thank you a lot for pointing toward the underscore. That will work and I hope the pros will tell me what is behind the mysterious 2 ;)

[Jannis Limperg]

Exprs representing mvars and hypotheses often contain nonsensical types like these. infer_type will give you the right type. :shrug:

[Fabian Glöckle]

"/- [WARNING] Do not trust the types for mvar and local_const,
they are sometimes dummy values. Use tactic.infer_type instead. -/" I see

[Jannis Limperg]

Yep yep. (Fixed in Lean 4 thankfully.)

[Fabian Glöckle]

So how would I write this instead?

meta def mk_mvar_pis : expr → tactic (list expr × expr)
| (pi n _ d b) := do
  p ← mk_mvar' n d,
  (ps, r) ← mk_mvar_pis (instantiate_var b p),
  return ((p :: ps), r)
| e := return ([], e)

[Fabian Glöckle]

(taken from mk_local_pis)

[Fabian Glöckle]

I would like to retrieve the body of a (nested) pi, but with something unifiable instead of var 0 etc inside

[Jannis Limperg]

I wrote a comprehensive library for this sort of task a while ago. docs#tactic.open_pis_metas should be what you're looking for.

[Fabian Glöckle]

wow great, exactly what I need!

[Fabian Glöckle]

I didn't find it because I was looking for mvars, not metas...

[Fabian Glöckle]

and I am learning from your code that one should not create mvars by the expr.mvar constructor but by mk_meta_var, right?

[Jannis Limperg]

If I used it there, probably. ;) I don't recall the details.

[Jannis Limperg]

Ah yeah if you use the expr constructor directly, you create a malformed expression. Metavariables which are referred to in an expression must be registered in the environment and mk_meta_var does exactly that.

[Henrik Böving]

Just as a learning experience for myself^^ @Jannis Limperg

i put all of my (admittedly rather little) knowledge of the Lean 4 Meta API into this:

def foo : MetaM Unit := do
  let u ← Meta.mkFreshLevelMVar
  let a ← Meta.mkFreshExprMVar (mkSort u)
  let listA := mkApp (mkConst `List [u]) a
  let listNat ← Meta.mkAppM `List #[mkConst `Nat]
  IO.println s!"{listA}"
  IO.println s!"{listNat}"
  if ←Meta.isDefEq listA listNat then
    IO.println "wooo"
    let newlistA ← Meta.instantiateMVars listA
    IO.println s!"{newlistA}"
  else
    let newlistA ← Meta.instantiateMVars listA
    IO.println s!"{newlistA}"
    IO.println "booo"

#eval foo

but I get a boo and no meta variables are instantiated, why's that the case? The types it prints are

List.{?_uniq.1} ?_uniq.2
List.{0} Nat

those look to me like they should be solvable no?

[Jannis Limperg]

Took me a bit to figure out as well. It's a level issue: mkApp (mkConst `List [u]) a is not type-correct. List.{u} has type Type u -> Type u, but a has type Sort u. Complete fix:

import Lean

open Lean
open Lean.Meta

def foo : MetaM Unit := do
  let u ← mkFreshLevelMVar
  let a ← mkFreshExprMVar (mkSort (mkLevelSucc u))
  let listA := mkApp (mkConst ``List [levelZero]) a
  let listNat ← Meta.mkAppM ``List #[mkConst ``Nat]
  IO.println s!"{listA}"
  IO.println s!"{listNat}"
  if ← Meta.isDefEq listA listNat then
    IO.println "wooo"
    let newlistA ← Meta.instantiateMVars listA
    IO.println s!"{newlistA}"
  else
    let newlistA ← Meta.instantiateMVars listA
    IO.println s!"{newlistA}"
    IO.println "booo"

#eval foo

Other comments which are hopefully helpful:

• Use ``List instead of `List where possible.
• I usually use trace[debug] for printf-style debugging.