コンテンツにスキップ

古典論理，選択，商，Lean の追加原理

ここまで見た基本的な証明項の構成は，かなり構成的な性質を持っています． つまり，一般の命題 P : Prop について P ∨ ¬ P を証明するには，P の証明か ¬ P の証明のどちらかを実際に与える必要があります． 排中律や背理法，存在からの非構成的な選択を自由に使う標準的な数学を扱うには，追加の原理が必要になります．

Lean の標準的な基礎には，命題外延性，商，選択などの原理が用意されています． これは Mathlib 独自の仮定ではなく，Lean の上で通常の数学を展開するための基礎です． Mathlib はその上に多くの定義と定理を積み上げています． これらを使う場合も，Lean は最終的にその原理を含む証明項を構成し，カーネルが型を確認します．

参考:

#check Classical.em
#check Classical.choice
#check Quot
#check Quot.sound
#check Quot.lift

排中律は Classical.em P として使えます． 実際の証明では，前に見た by_cases h : P や Classical.byContradiction を通じて使うことが多いです． ここでは，「標準的な数学をするために，Lean にはこのような原理が用意されている」という位置づけを押さえておきます．

example (P : Prop) : P ∨ ¬ P := by
  exact Classical.em P

命題外延性 propext は，論理的に同値な命題を等しい命題として扱うための原理です． P ↔ Q は「互いに導ける」という命題であり，P = Q は Prop の元としての命題そのものの等号です． この 2 つは区別されますが，propext により P ↔ Q から P = Q を作れます．

#check propext

example (P Q : Prop) (h : P = Q) : P ↔ Q := by
  rw [h]

example (P Q : Prop) (h : P ↔ Q) : P = Q := by
  exact propext h

example (P Q : Prop) : (P ∧ Q) = (Q ∧ P) := by
  apply propext
  constructor
  · intro h
    exact ⟨h.2, h.1⟩
  · intro h
    exact ⟨h.2, h.1⟩

商型では，同値関係で同値な代表元を，同じ商の元として扱います． 次の例では，自然数を「2 で割った余りが等しい」という関係で割った商を考えています． 0 と 2 は代表元としては異なりますが，この商の中では等しく，その等式は Quot.sound で作られます．

def SameModTwo (a b : Nat) : Prop :=
  a % 2 = b % 2

example : Quot.mk SameModTwo 0 = Quot.mk SameModTwo 2 := by
  exact Quot.sound (by rfl)

選択は，存在命題から証拠を選ぶときに現れます． 数学では「条件を満たすものを 1 つ取る」と自然に書きますが，Lean でその選んだ値を定義として保存するには Classical.choose を使います． このような定義は一般に計算可能な内容を持たないため，noncomputable として宣言します．

ここでいう「選択」は，集合論の選択公理をそのまま Lean に書き写したものではありません． 集合論の選択公理は，非空集合の族から選択関数が存在する，という集合論内部の命題です． 一方，Lean の型理論で使う Classical.choice は，型 α が空でないという命題 Nonempty α の証明から，実際に α の項を 1 つ返す選択演算子です． つまり Classical.choice : Nonempty α → α は，証明情報からデータを取り出す追加原理です． 各添字 i ごとにこれを使えば，集合論の選択公理に似た選択関数を作れます． ただし，この関数は計算規則を持たないため，値を定義として保存する場合は noncomputable になります．

noncomputable def choiceFunctionFromNonempty {ι : Type} {α : ι → Type}
    (h : ∀ i : ι, Nonempty (α i)) : (i : ι) → α i :=
  fun i => Classical.choice (h i)

example {ι : Type} {α : ι → Type} (h : ∀ i : ι, Nonempty (α i)) :
    Nonempty ((i : ι) → α i) := by
  exact ⟨choiceFunctionFromNonempty h⟩

noncomputable def chosenNatFromExistence (h : ∃ n : Nat, 10 < n) : Nat :=
  Classical.choose h

example (h : ∃ n : Nat, 10 < n) : 10 < chosenNatFromExistence h := by
  exact Classical.choose_spec h

命題外延性 propext は，論理的に同値な命題を等しい命題として扱うために使います． 商型は，同値関係で割った対象を作るために使います． たとえば整数，有理数，剰余類，商群など，標準的な数学では「同値なものを同一視する」構成が頻繁に現れます．

この章で押さえておきたいのは，これらが tactic の小技ではなく，Lean で標準的な数学を表現するための基礎的な仕組みだという点です． 一方で，証明項を構成しているという基本的な見方は変わりません． 古典論理や選択を使う場合も，Lean はその原理を使った証明項を構成し，カーネルが型を確認しています．

演習

propext を使って，論理的に同値な命題を等しい命題として扱ってください．

example (P Q : Prop) (h : P ↔ Q) : P = Q := by
  sorry

Classical.choose と Classical.choose_spec を使って，存在命題から証拠を取り出してください．

noncomputable def chosenNatExercise03 (h : ∃ n : Nat, n > 10) : Nat :=
  Classical.choose h

example (h : ∃ n : Nat, n > 10) : chosenNatExercise03 h > 10 := by
  -- `Classical.choose_spec h`
  sorry

Quot.sound を使って，商型の中で代表元が等しいことを証明してください．

def sameModTwoExercise03 (a b : Nat) : Prop :=
  a % 2 = b % 2

example : Quot.mk sameModTwoExercise03 1 = Quot.mk sameModTwoExercise03 3 := by
  -- `Quot.sound` と `decide`
  sorry