`example`，`theorem`，`lemma`¶

example は名前を残さない匿名の宣言です．構文やタクティックの小さな実験に向いています．証明の文脈では example : P := ... は「命題 P の証明をその場で与える」という意味です．ただし Lean のコマンドとしての example は，命題に限らず任意の型の項を匿名で確認する用途にも使えます．

example (n : Nat) : n + 0 = n := by
  exact Nat.add_zero n

example : Nat :=
  42

命題そのものも式です．次の最初の例では，2 + 2 = 4 という命題が Prop 型の式であることを示しています．次の例では，その命題の証明を与えています．

example : Prop :=
  2 + 2 = 4

example : 2 + 2 = 4 := by
  rfl

theorem は名前つきの定理を宣言します．後からその名前を使って参照できます． theorem で定義される名前は，ある命題 P : Prop を型にもつ項，つまり P の証明項です． theorem や lemma の型は命題でなければなりません．データや計算内容を名前つきで定義したいときは def を使います．

theorem add_zero_named (n : Nat) : n + 0 = n := by
  exact Nat.add_zero n

theorem two_plus_two_is_four : 2 + 2 = 4 := by
  rfl

theorem positive_three_named : 0 < 3 := by
  decide

example : 5 + 0 = 5 := by
  exact add_zero_named 5

example : 2 + 2 = 4 := by
  exact two_plus_two_is_four

example : 0 < 3 := by
  exact positive_three_named

実用上は，補助的な定理を「lemma」と呼ぶことがよくあります． Core Lean では，補助的な定理も theorem で宣言できます． Mathlib を import している環境では lemma というコマンドもよく使われますが，ここでは Core Lean に合わせて theorem で書きます．

theorem zero_add_named (n : Nat) : 0 + n = n := by
  exact Nat.zero_add n

example : 0 + 5 = 5 := by
  exact zero_add_named 5

example，theorem，lemma はいずれも，命題を証明するためのコマンドです．ただし，example は上で見たように，匿名の型検査例にも使えます．命題証明として使う場合の違いは，主に「名前を残すか」「数学的にどのような位置づけか」です．

def との関係も重要です． Lean の内部では，定義も定理も「名前に型つきの項を結びつける」という点では似ています．たとえば def で Nat 型の値を定義することも，Prop 型の証明を定義することもできます．ただし，数学的な命題の証明には，意図が明確になるように theorem や lemma を使うのが普通です．

def proofByDef : 1 + 1 = 2 := by
  rfl

example : 1 + 1 = 2 := by
  exact proofByDef

example，theorem，lemma¶

`example`，`theorem`，`lemma`¶