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.
Stack Exchange network consists of 181 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.Visit Stack Exchange
Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.Sign up to join this community
An outline of the differences in Lean 4, which you mentioned is the version you are interested in:
defis the primary way to define a named function / value in Lean. Unless its result type is
Propor it is marked
defwill 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!
theoremis 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
examplecreates an anonymous
defthat is type checked for correctness and then immediately discarded by Lean. Thus, an
examplehas 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
noncomputableif 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.,
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
theorem thm : ℕ := 0. $\endgroup$