Rules of metavariable unification

Stream: lean4

[Thomas Bourgeat]

I am having trouble building a mental model for metavariable unification, when one is trying to use them as a hole that get refined in a new constructed hypothesis.
Here is an example, where we would like to use the tactic mode to construct a term of type even _ for some _ that will get decided when we refines the hole in tactic mode:

inductive even : nat -> Prop
  | z : even 0
  | l : forall n, even n -> even (n+2)

-- V1
def y : True := by
  have x: (@even _ _) := by -- complains here that _ it does not know how to synthesize _, seems reasonable
    apply even.l
    apply even.z

-- V2
def y : True := by
  have x: (@even ?_ ?_) := by -- is happy here
    apply even.l -- complains here that it cannot unify (even (?n + 2) and even ?refine_2
    apply even.z

Interestingly on older version of Lean4, the first version worked fine, but the second version also failed.
I am a bit puzzle with the V2 error message, of why the two metavar could not unify. Any insight?

[Marcus Rossel]

Is that really the definition of even that you intended?

#check even -- even {nat : Type} : nat → Prop

Note that nat is not the type of natural numbers (which is Nat), so you're using autoimplicits in the definition of even.

[Thomas Bourgeat]

Oh, the specific example is not very relevant, the issue occured in a bigger project and I tried to isolate the issue on a minimal example. The same problem exist using Nat instead of nat, I believe. Thanks for the remark though, I will minimize more.

Edit: Getting rid of unnecessary extra type parameter:

inductive even : Nat -> Prop
  | z : even 0
  | l : forall n, even n -> even (n+2)

def y : True := by
  -- Let's say I want to construct that some number is even,
  have x: (even ?_) := by
    apply even.l -- Complains here that it cannot unify even (?n  +2) and  even ?refine
    apply even.z

[Anand Rao Tadipatri]

It works when you use let instead of have and avoid the synthetic metavariable ?_ in the type:

inductive even : Nat -> Prop
  | z : even 0
  | l : forall n, even n -> even (n+2)

def y : True := by
  -- Let's say I want to construct that some number is even
  let x: (even _) := by
    apply even.l
    apply even.z
  trivial

[Thomas Bourgeat]

Thanks! Is it the case that synthetic metavariable have different unification rules? Any insight on what these rules are?

[Yann Herklotz]

There is a brief description here, which describes the unification rules: https://leanprover-community.github.io/mathlib4_docs/Lean/MetavarContext.html#Lean.MetavarKind. I feel like using _ in have should still work though and give the same behaviour as let.

A hacky solution (that seems to work) to support synthetic metavariables:

import Lean
open Lean Meta Elab

inductive even : Nat -> Prop
  | z : even 0
  | l : forall n, even n -> even (n+2)

def y : True := by
  -- Let's say I want to construct that some number is even
  let x: (even _) := by
    apply even.l
    apply even.z

  have y: (even ?x) := by
    run_tac Lean.Meta.withAssignableSyntheticOpaque do
      Tactic.evalTactic (← `(tactic| apply even.l))
      Tactic.evalTactic (← `(tactic| apply even.z))

  trivial

I'm not sure if it was intended to make metavariables syntheticOpaque instead of just synthetic in the have declaration.

[Thomas Bourgeat]

Interestingly, the following works:

def y : True := by
  have foo : even (_ : Nat) := by {  -- Adding the annotation : Nat
    apply even.l
    apply even.z
  }
  trivial

And that one too:

def y : True := by
  have foo : even (_ : _) := by {  -- Adding the annotation : Nat
    apply even.l
    apply even.z
  }
  trivial

[Thomas Bourgeat]

Observing that the braces are semantically significative:

inductive even : Nat -> Prop
  | z : even 0
  | l : forall n, even n -> even (n+2)

def doesNotWork : True := by
  -- Let's say I want to construct that some number is even
  have x: (even _) := by
    apply even.l
    apply even.z
  trivial

def works : True := by
  have foo : (even _) := by {
    apply even.l
    apply even.z
  }
  trivial

[Kyle Miller]

What version of Lean are you using (#eval Lean.versionString)?

[Kyle Miller]

I'm observing that doesNotWork works with 4.9.0-rc3

[Thomas Bourgeat]

EDIT

[Thomas Bourgeat]

Oops fixed the snippet, I had put a let instead of a have locally. The bug does show up in the playground.

[Kyle Miller]

It looks like this has to do with incrementality. It seems odd that curly braces have anything to do with it, but it's actually that the feature is looking for a very specific syntax. Putting parentheses also "fixes" it:

def doesNotWorkNowWorks : True := by
  have x: (even _) := (by
    apply even.l
    apply even.z)
  trivial

[Kyle Miller]

(Pinging @Sebastian Ullrich )

[Sebastian Ullrich]

Hmm. If anything, I would argue that both should fail: theorem does not allow you to place an unresolved mvar there and I think of have as "local theorem". Note that this change did not break a single line in all of Mathlib.

[Kyle Miller]

I agree with that, but I just wanted to make sure the by syntax matcher was as robust as you wanted it to be here.

[Sebastian Ullrich]

This invariant would also make parallelizing haves a bit more feasible, though no promises on that front yet

[Sebastian Ullrich]

Kyle Miller said:

I agree with that, but I just wanted to make sure the by syntax matcher was as robust as you wanted it to be here.

You mean about by {...} specifically? I didn't consciously disallow it but I didn't think very hard about it either because I never see it being used in practice. But yes, it should at least not lead to different semantics.

[Kyle Miller]

Yeah, by { ... } vs by ... (and hopefully that's it?)

Sometimes in teaching material we use by {...} to help deal with the lack of :tada:

[Mario Carneiro]

@Sebastian Ullrich said:

Hmm. If anything, I would argue that both should fail: theorem does not allow you to place an unresolved mvar there and I think of have as "local theorem". Note that this change did not break a single line in all of Mathlib.

This is confusing to me, are you saying that have x : even _ := even.z is not going to be allowed anymore? That seems extremely common to me. I don't really agree with the comparison of have to "local theorem", and in fact I have frequently run into issues with have being too aggressive about half-instantiated types; being able to partially write out a type is extremely important and I would not want the type/proof firewall from theorem/def anywhere inside a proof body, as the tools for working around it are limited.

[Kim Morrison]

(That is agreeing that metavariables need to be able to leak, not agreeing that this won't be allowed anymore!)

[Sebastian Ullrich]

Yes, I realize this may be too restrictive for all haves. I guess I was mostly surprised that it did not break any tactic have bys in Mathlib. So we could accept this difference in behavior in exchange for incrementality support. Or figure out a much more complicated implementation...

[Sebastian Ullrich]

Note that there are already term/tactic differences in degrees of leakage, perhaps what Mario referenced above. The first example works, the second one fails at have.

example : 0 = 0 :=
  have : _ = _ := rfl
  this

example : 0 = 0 := by
  have : _ = _ := by { rfl }
  exact this

[Sebastian Ullrich]

#4626 restricts only the by { ... } case for now to make it consistent with the braceless case, as that syntactic distinction really should not make a semantic difference