Synthetic MVars vs MVars

Stream: lean4

[Henrik Böving]

This piece of meta code:

import Lean
open Lean Meta Elab Term Command
elab "#unify" lhs:term " =?= " rhs:term : command => do
  liftTermElabM do
    let lhs <- elabTerm lhs none
    let rhs <- elabTerm rhs none
    if <- isDefEq lhs rhs then
      logInfo m!"Unifies!"
    else
      logInfo "Nu-uh!"

#unify List Nat =?= List _
#unify List Nat =?= List ?a

Spits out Unifies for the first case and Nu-uh for the second case. According to go to definition on _ and ?a the former is a "hole" while the latter is a "synthetic hole".

I've got two questions:

1. What is the difference between these?
2. Why does the unification work out for one of them and not for the other?

[Max Nowak 🐉]

To add to the confusion: If we add let holes := rhs.collectMVars default |>.result before isDefEq, it finds one hole for ?a, and no holes for _.

[Max Nowak 🐉]

It would be nice to have a command like this, which prints the hole assignment after unification.

[Leonardo de Moura]

https://github.com/leanprover/lean4/blob/master/src/Lean/MetavarContext.lean#L84-L108

[Damiano Testa]

... and if you want to see more people fumbling through similar issues recently, there is a similar discussion towards the beginning of this thread

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Help.20with.20writing.20tactic

I'm on mobile and I do not know how to link to a specific comment.

[Kevin Buzzard]

(I believe it's not possible to do so on mobile)

[Eric Wieser]

Kevin Buzzard said:

(I believe it's not possible to do so on mobile)

The trick is to use the "quote and reply" feature, then tediously backspace everything but the link

[Damiano Testa]

Just to try Eric's suggestion: this is where the discussion starts:

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Help.20with.20writing.20tactic/near/398061102

[Damiano Testa]

(sent from my phone!)

[Damiano Testa]

Hmm, except that yo check if it worked, I probably need a computer... :man_facepalming:

[Gareth Ma]

That's me in the thread :eyes:

[Gareth Ma]

But yes, the docs Leonardo linked to is pretty clear. As it says, SyntheticOpaque is never assigned by isDefEq, while natural and synthetic correspond to how "greedy" the matching should be

[Gareth Ma]

You can use set_option trace.Meta.isDefEq true to see matching outputs. It's really useful and cool to read too.

[Gareth Ma]

I had to something similar to yours, and I did something like this:

def setMCore (e : Expr) (stx : TSyntax `term) (loc : Location) : TacticM Unit := withMainContext do
  let (origPattern, mvarIds) ← elabTermWithHoles stx none (← getMainTag) (allowNaturalHoles := true)
  /- Named holes are by default syntheticOpaque and not assignable, so we change that -/
  mvarIds.forM fun mvarId => mvarId.setKind .natural
  trace[Tactic.setm] "origPattern : {← ppExpr origPattern}"
  /- ... -/

[Gareth Ma]

Taken straight from my code :P

[Max Nowak 🐉]

Ooooo, mvarId.setKind .natural is ideal. That'll help me a lot.

[Max Nowak 🐉]

What is the correct way to get the name of a synthetic variable? I am currently doing (<- mymyvarid.getDecl).userName, but that turns up [anonymous] sometimes despite initially giving it a name such as ?a

[Gareth Ma]

Max Nowak 🐉 said:

What is the correct way to get the name of a synthetic variable? I am currently doing (<- mymyvarid.getDecl).userName, but that turns up [anonymous] sometimes despite initially giving it a name such as ?a

That is the correct way to do it (ideally there should be a .getUserName, and I probably should PR for it lol). If it says [anonymous] for the name it means you didn't give it a name properly

[Gareth Ma]

import Lean

open Lean Parser Tactic Elab Tactic Meta in
elab "myTactic" : tactic => do
  let mvar ← mkFreshExprMVar none (userName := `a)
  let mvarId := mvar.mvarId!
  logInfo m!"mvar : {mvar}"
  logInfo m!"mvarId : {mvarId}"
  logInfo m!"name : {(←mvarId.getDecl).userName}"

example : true := by
  myTactic
  trivial

logged:

▶ 1 goal
⊢ true = true

▶ 12:3-12:11: information:
mvar : ?a

▶ 12:3-12:11: information:
mvarId : case a
⊢ ?m.2484

▶ 12:3-12:11: information:
name : a

[Gareth Ma]

closer to your code:

import Lean

open Lean Parser Tactic Elab Tactic Meta in
elab "myTactic" expr:term : tactic => do
  let expr ← elabTerm expr none
  let mvarId := expr.mvarId!
  logInfo m!"expr : {expr}"
  logInfo m!"mvarId : {mvarId}"
  logInfo m!"name : {(←mvarId.getDecl).userName}"

example : true := by
  myTactic ?a
  trivial

same output (with different id)

[Max Nowak 🐉]

With the following code:

import Lean
open Lean Elab Command Meta Term
elab "#unify" lhs:term " =?= " rhs:term : command => do
  liftTermElabM do
    let lhs <- elabTerm lhs none
    let rhs <- elabTerm rhs none
    let holes := rhs.collectMVars default |>.result
    holes.forM fun h => h.setKind .natural
    if <- isDefEq lhs rhs then
      let assignments <- holes.mapM fun h => do
        let name := (<- h.getDecl).userName
        let val := Expr.mvar h
        pure m!"{name} ↦ {val}"
      logInfo m!"{assignments}"
    else
      logError "Nu-uh!"

I get the following result:

#unify List Nat =?= List ?a -- [a ↦ Nat]
#unify (α : Type) -> List α =?= (α : Type) -> List ?hole -- [[anonymous] ↦ fun α => α]

I have two issues with this code:

• The name should be hole, not [anonymous].
• The assigned value does not fit exactly into the hole, I would have expected simply α, instead it is fun α => α.

[Gareth Ma]

For your second question I think it's because the ?hole (might) depend on α, so it should be a function.

[Gareth Ma]

For your first question, it's because ?hole here is not a mvar, it's a bvar (bound variable)

[Gareth Ma]

If it is clearer, write it like this:

#unify (λ α ↦ List (List α)) =?= (λ α ↦ ?b)

[Gareth Ma]

You can also log {repr rhs} to see it's a bvar

[Gareth Ma]

Also, please write ← (type with \l) instead of <- :) - at least that's the convention in Mathlib4, afaik. Though looking at the source code, there are 4 occassions where people used <- instead, they should probably be PR'ed