Zulip Chat Archive

Stream: lean4

Topic: metavariables in lemma statements

view this post on Zulip Alexander Bentkamp (Jan 11 2021 at 18:02):

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

view this post on Zulip Adam Topaz (Jan 11 2021 at 18:06):

Interesting... this work in lean3:

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

view this post on Zulip Adam Topaz (Jan 11 2021 at 18:06):

Must be something about lemma vs. example

view this post on Zulip Gabriel Ebner (Jan 11 2021 at 18:08):

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.

view this post on Zulip Eric Wieser (Jan 11 2021 at 23:03):

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

view this post on Zulip Leonardo de Moura (Jan 11 2021 at 23:56):

@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.

view this post on Zulip Leonardo de Moura (Jan 12 2021 at 00:50):

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

Last updated: May 18 2021 at 23:14 UTC