metavariables in lemma statements

Stream: lean4

[Alexander Bentkamp]

Just discovered an interesting difference between Lean 3 and 4. Lean 4 allows metavariables in lemma statements:

theorem one_plus_one : 1 + 1  = _ :=
show (1 + 1 = 2) by rfl

Lean 3 doesn't accept them:

lemma one_plus_one : 1 + 1  = _ := -- don't know how to synthesize placeholder context: ⊢ ℕ
  show 1 + 1 = 2, by refl

[Adam Topaz]

Interesting... this work in lean3:

example : 1 + 1 = _ := show 1 + 1 = 2, by refl

[Adam Topaz]

Must be something about lemma vs. example

[Gabriel Ebner]

Right. In Lean 3 the lemma statement is elaborated first, and the proof is elaborated separately. There are two reasons:

1. The statement of a lemma shouldn't depend on its proof. (Otherwise you might accidentally prove something weaker than you want.)
2. We want to check proofs in parallel. For this to work we need to know the theorem statement without elaborating the proof.

[Eric Wieser]

Does that make this a shortcoming in lean 4? And if so, is it by design, accident, or just low prioritization?

[Leonardo de Moura]

@Eric Wieser This part is still missing. That being said, the behavior will still be slightly different from Lean 3. Significant changes:

• We are removing unused variables from theorems. So, the behavior here is similar to def in Lean 3.
• If the user provides the type in a def, we will ensure it doesn't contain metavariables before we elaborate its body as we do for theorem in Lean 3.

The goal is to reduce the number of differences between theorem and def.

[Leonardo de Moura]

I just pushed https://github.com/leanprover/lean4/commit/36008271eacc7af3c22828c3d3238650349017d4 since this change may create compatibility issues in the future.
It ensures the header of a theorem must not contain metavariable (aka holes) before we elaborate its body/value. Same for def when the type is explicitly provided. That is, we can still write

def inc x := x + 1

but the following is an error

def inc x : id _ := x+1