論理記号の対応まとめ

Chapter 01 で使った論理記号は，ここまで見た依存関数型，structure，inductive 型，class の具体例として理解できます． 一覧にすると次のようになります．

notation	展開後の形	実装の種類	項を作る典型	情報を使う典型
P → Q	非依存関数型	関数型	fun hP => ...	hPQ hP
∀ x : α, P x	依存関数型	依存関数型	fun x => ...	h x
P ∧ Q	And P Q	structure	And.intro hP hQ，⟨hP, hQ⟩	h.left，h.right
P ∨ Q	Or P Q	inductive 型	Or.inl hP，Or.inr hQ	cases h，Or.elim h ... ...
∃ x : α, P x	Exists (fun x => P x)	inductive 型	Exists.intro w hw，⟨w, hw⟩	witness と証明に分解
a = b	Eq a b	inductive 型	Eq.refl a，rfl	rw，subst
P ↔ Q	Iff P Q	structure	Iff.intro hPQ hQP，⟨hPQ, hQP⟩	h.mp，h.mpr
True	True	inductive 型	True.intro	ほぼ情報なし
False	False	constructor なしの inductive 型	通常は作れない	False.elim h
¬ P	Not P，すなわち P → False	def	fun hP => ...	hNot hP : False
x ≤ y	LE.le x y	class LE の field	型ごとの定理や計算	型ごとの定理や計算
x < y	LT.lt x y	class LT の field	型ごとの定理や計算	型ごとの定理や計算

∀ だけは，And や Or のような通常の名前つき inductive 型ではありません． Lean の構文として依存関数型へ elaboration されます．

section LogicConnectivesAsTypes

variable (P Q R : Prop)

#check (P → Q)
#check (∀ n : Nat, IsEvenNat n)
#check (P ∧ Q)
#check (And P Q)
#check (P ∨ Q)
#check (Or P Q)
#check (∃ n : Nat, IsEvenNat n)
#check (P ↔ Q)
#check (Iff P Q)
#check ((2 : Nat) = 2)
#check ((2 : Nat) ≤ 3)
#check ((2 : Nat) < 3)

example (hP : P) (hQ : Q) : P ∧ Q :=
  And.intro hP hQ

example (h : P ∧ Q) : P :=
  h.left

example (hPQ : P → Q) (hQP : Q → P) : P ↔ Q :=
  Iff.intro hPQ hQP

example (h : P ↔ Q) (hP : P) : Q :=
  h.mp hP

example : True :=
  True.intro

example (h : False) : P :=
  False.elim h

example (hP : P) : ¬ ¬ P :=
  fun hNotP => hNotP hP

end LogicConnectivesAsTypes