Status of "lemma" keyword in Lean 4

Stream: new members

[Lars Ericson]

I was tempted to use a "lemma" keyword while working on a proof exercise in Lean 4 like this:

variable (p q r : Prop)

lemma ex3a : (p ∧ q) ∧ r → p ∧ q ∧ r :=   -- unexpected identifier; expected command
  sorry

theorem ex3a : (p ∧ q) ∧ r → p ∧ q ∧ r := -- no problem here
  sorry

#check ex3a

theorem ex3 : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  Iff.intro
    (fun h : (p ∧ q) ∧ r  => ex3a p q r h)
    (fun h : p ∧ (q ∧ r) => sorry)

However, the lemma gets the red underscore: it no longer works. This is confusing, because lemma is used in many places in the Lean 4 mathlib source, for example on line 500 of Data/Complex/Module.lean

What is the current status of lemma in Lean 4? Deprecated, gone, out of style guide?

[Ruben Van de Velde]

lemma is a synonym for theorem that's defined in mathlib. Jury's still out on whether we'll keep it

[Lars Ericson]

It's gone in https://live.lean-lang.org/, so I guess the jury decided. Is there an archive like PEP for these kinds of language design decisions?

[Alex J. Best]

The jury in this case means the mathlib community, if you import Mathlib in live.lean-lang it will work fine of course. Its just not a core feature anymore

[Julian Berman]

(Since you've mentioned it in at least one other place, I'll just mention that at least in Python I wouldn't personally expect a PEP for that kind of thing, they're for more... 'elaborate' language changes -- Lean (core) has something like PEPs, they're the RFCs that folks occasionally write in issues: https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3ARFC )

[Lars Ericson]

@Julian Berman, the Lean 4 Mathlib source has 2,491 uses of the lemma synonym, which doesn't work in https://live.lean-lang.org. So even though it is a redundant synonym, it is still somewhat impactful to delete it (i.e., those 2,491 uses might want to be changed to theorem prior to removing the synonym). That's what elevates it somewhat to an RFC.

Having RFCs is as good as having PEPs. But, I like the structure and presentation of the PEP website, because the PEPs align directly with release versions of Python. PEPs are frequently quoted in Stack Exchange questions about the presence or absence of particular language features. I don't know that people would quote RFCs as fluently or be able to align them with particular Lean 4 releases. Lean 4 will see a greatly expanding user base over time. Lean 4 will also change constantly. It is helpful for a wider user base to have a kind of "bible" that people can refer to that aligns language releases and the presence or absence of particular language features.

[Kyle Miller]

The reason there are so few lemmas in mathlib right now is that mathport turned all lemmas into theorems.

[Kyle Miller]

Lars Ericson said:

the lemma synonym, which doesn't work in https://live.lean-lang.org

Maybe you were writing this comment while Alex Best answered you, but lemma does in fact work in on https://live.lean-lang.org just like in any other mathlib file; you just have to import a relevant module to get the syntax.

[Kyle Miller]

import Mathlib.Tactic.Basic

[Eric Wieser]

There is a PR in the works (std4#413) that adds lemma to std with a better error message