lemma works not synonymously for theorem or def

[LKlinke]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following minimal example does not work:

def add2 x := x + 2

def add4 x := x + 4

lemma broken: (add4 x) = add2 (add2 x) := by simp [add4, add2]

whereas

def add2 x := x + 2

def add4 x := x + 4

theorem broken: (add4 x) = add2 (add2 x) := by simp [add4, add2]

works fine.

Expected behavior: Both programs should work fine.

Actual behavior: the theorem version works, the lemma version does not.

Versions

4.12.0-nightly-2024-10-22
live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks for the report. The lemma command is a feature of mathlib (or batteries) and simply does not exist in lean. Maybe it would be desirable to have a better error message when a command name is unknown or misspelled, or have stricter indentation rules that make this fail more clearly, but for now I'd say it works as advertised.

[digama0]

Note that batteries has a lemma command which is implemented specifically so that it can tell you that it is not lean syntax and suggests theorem instead. I would like such support to be upstreamed, where it can be more useful.

[LKlinke]

I think my issue was that when reading the reference manual (Version 3) is says:

Lean provides ways of adding new objects to the environment. The following provide straightforward ways of declaring
new objects:

constant c : α : declares a constant named c of type α, where c is a declaration name.
axiom c : α : alternative syntax for constant
def c : α := t : defines c to denote t, which should have type α.
theorem c : p := t : similar to def, but intended to be used when p is a proposition.
lemma c : p := t : alternative syntax for theorem

Here it is never mentioned that lemma is only available when using additional libraries. Of course I should have read version 4 instead of version 3.