11
$\begingroup$

What are all the differences between these keywords that allow for defining top level variables?

What I have noticed so far is that theorems can't be anonymous — you can write example : A := B but not theorem : A := B.

$\endgroup$
3
  • $\begingroup$ The difference between theorem and def might have to do with VM compilation. At least, that's what lean says if you try to write theorem thm : ℕ := 0. $\endgroup$ Commented Jul 7, 2022 at 22:41
  • $\begingroup$ @user2395649 I'm talking about lean 4 not 3. $\endgroup$ Commented Jul 7, 2022 at 22:45
  • $\begingroup$ For Lean3, the lean 3 reference manual should provide some explanation. $\endgroup$
    – Eric
    Commented Jul 8, 2022 at 0:02

1 Answer 1

12
$\begingroup$

An outline of the differences in Lean 4, which you mentioned is the version you are interested in:

  • A def is the primary way to define a named function / value in Lean. Unless its result type is Prop or it is marked noncomputable, a def will be compiled into Lean's intermediate representation (IR) in preparation for execution by Lean's interpreter and/or for further compilation into C code.
def add (x y : Nat) : Nat := x + y -- a simple computation
def one_plus_one_eq_two : 1 + 1 = 2 := rfl -- theorems can be defs too!
  • A theorem is essentially a noncomputable def. This means that values defined by a theorem cannot be used in ordinary computation as they will not (and maybe cannot) be compiled down into executable code. Note that Lean erases types (eg., T : Type u, Prop : Type), propositions (e.g., 1 = 1 : Prop) and proofs (e.g., rfl : 1 = 1) -- all of which are technically noncomputable -- before attempting compilation, which is why they are still safe to use in computable code. Such values are termed irrelevant by the Lean compiler IR.
theorem foo : Nat := 5
def addFoo (x : Nat) := x + foo 
/-
error: 
failed to compile definition, consider marking it as 'noncomputable' 
because it depends on 'foo', and it does not have executable code
-/
#eval foo -- same error
theorem addFoo' (x : Nat) : Nat := x + foo -- ok
  • An example creates an anonymous def that is type checked for correctness and then immediately discarded by Lean. Thus, an example has no lasting effect on the environment and cannot be referred to by later declarations. Note that while Lean will end up discarding the code it generates from an example, it does still, by default, generate code. Thus, you must mark an example noncomputable if it uses a noncomputable definition for a (i.e., to define a value that is not erased).
example : 1 + 1 = 2 := rfl
example (x y : Nat) : Nat := x + y
example (x : Nat) : Nat := x + foo -- same error as above
noncomputable example (x : Nat) : Nat := x + foo -- ok

Note that there are other keywords for defining functions / values (e.g., axiom, opaque, abbrev, etc.) which I have not discussed here as you did not ask about them. Furthermore, given your choice of keywords to compare, it seemed best to focus on the named/anonymous, computable/noncomputable distinctions that separate def, theorem, and example.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.