Solutions · Part 2
第2部 命題と証明
第6–10章 · 15問
第6章
命題・証明・含意
問題本文問題1命題とその証明を異なるsortの対象として読む
Problem
問題
章本文の位置で見るP : Prop と p : P に現れる二つのコロンを分析し、左辺と右辺の役割をそれぞれ書いてください。
Bool の値 true、false と、Prop に属する命題、その命題を型として持つ証明項を三列の表にし、それぞれに可能な観察を示します。
次に、同じ命題の二つの証明に対するLeanの証明無関係性と、二つの自然数の等式を比較します。 両者に同じ論法を適用できない理由を、項が属するsortと、証明から計算データを取り出すことへの制約を指して説明してください。
ヒント
P : Prop と p : P のコロンを別々の分類として読みます。
解答
命題 P は Prop に属する式であり、証明 p は型 P に属する項です。従って P : Prop は
「Pは命題」、p : P は「pはPの証明」という異なる判断です。Prop : Type はさらに命題のsortを
上位の宇宙へ分類します。真偽値 Bool の値を計算することと、命題型の項を構成することも別です。
存在命題では命題全体、証人、証人が性質を満たす証明を別々に分類します。依存型でも同じ読み方を保ちます。
theorem proofIrrelevance (P : Prop) (first second : P) : first = second :=
Subsingleton.elim first second
example : (1 : Nat) ≠ 2 := by decide問題2tactic状態をラムダ抽象と関数適用へ戻す
Problem
問題
章本文の位置で見るby intro p; exact p の実行前、intro p の後、exact p の後のゴール状態を書き、証明項 fun p => p の構文へ一対一に対応させてください。
その後、(P → Q) → (Q → R) → P → R について、外側から順に入力を導入し、各時点で利用できる仮定と目標型を記録します。
解答はterm modeとtactic modeの両方を提示します。両方から得られる最終的なラムダ項を示し、 tacticが証明の代替物ではなく、同じ証明項を構成する対話的な記法であることを検証します。
ヒント
intro が仮定を受け取る関数を作り、exact がその本体を与えると読んでください。
解答
目標 P → P に対する intro h は、証明項 fun h : P => ?_ を作り、残りの目標を P にします。
exact h は穴を仮定 h で埋めるため、完成項は fun h : P => h です。apply implication は
関数適用の結果を目標へ合わせ、引数に必要な証明を新しい目標として残します。
theorem identityTerm (P : Prop) : P → P := fun proof => proof
theorem identityTactic (P : Prop) : P → P := by
intro proof
exact proof
theorem compositionTerm (P Q R : Prop) : (P → Q) → (Q → R) → P → R :=
fun pq qr p => qr (pq p)
theorem compositionTactic (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by
intro pq qr p
exact qr (pq p)補足
複雑なtactic証明でも、各操作をラムダ抽象、構成子適用、場合分けへ戻すと依存関係を説明できます。
問題3爆発原理の仮定を隠さずに追跡する
Problem
問題
章本文の位置で見るfalseElimination : False → P を「あらゆる命題 P を証明する関数」と読むだけでは不十分です。この関数を呼び出すために必要な入力を明記し、
False の証明を持たない状態では何も導けないことを型から説明してください。
仮定 h : False を明示的に置いた文脈で、異なる二命題 P、Q を導く証明項を構成し、どの部分だけが共通の矛盾を消費しているかを示します。
最後に定理の型から h を消すことができない理由を述べれば、爆発原理と False の証明を混同していないことを検証できます。
ヒント
任意命題を得るために使う入力が False の証明であることを型に残します。
解答
爆発原理は False → P であり、無条件に任意の P を与える定理ではありません。仮定
h : False を受け取れば、False.elim h : P を構成できます。矛盾を導いた前段の仮定も文脈に残るため、
結論だけを取り出して体系が自明だと解釈してはいけません。
背理法では、矛盾を作るために古典原理を使ったかも追跡します。爆発原理自体は構成論理でも成立します。
theorem twoConsequences (P Q : Prop) (contradiction : False) : P ∧ Q :=
⟨False.elim contradiction, False.elim contradiction⟩第7章
命題論理と構成的・古典的推論
問題本文問題1導入規則と除去規則から証明の情報流を作る
Problem
問題
章本文の位置で見る連言、選言、否定、同値について、導入時に必要な証拠と除去時に得られる証拠を表にしてください。
表を使い P ∧ Q → P ∨ Q の二つの証明項を構成し、連言が持っていたどちらの証拠を選言のタグの中へ残し、どちらを捨てたかを記述します。
notOrIff の両方向を同じ表で追跡し、構成子、場合分け、関数適用がどの導入・除去規則に対応するかを行ごとに注記してください。
証明の各中間項に型を与え、情報が消失したり新しく捏造されたりしていないことが検証基準です。
ヒント
各結合子について、作るときに必要な情報と、使うときに取り出せる情報を対にします。
解答
P ∧ Q の導入は P と Q の両証明を要求し、除去はどちらの成分も取り出せます。P ∨ Q の導入は
左右どちらかの証明とタグを要求し、除去は二つの場合から同じ結論を作ります。P → Q の導入は P を
仮定して Q を作る関数、除去はその関数へ P の証明を適用する操作です。情報の作り方と利用法が対応します。
帰納型のAPIや圏論的普遍性でも、構成データと一意な利用原理を同じ二欄へ整理できます。
theorem keepLeft (P Q : Prop) : P ∧ Q → P ∨ Q :=
fun conjunction => Or.inl conjunction.left
theorem keepRight (P Q : Prop) : P ∧ Q → P ∨ Q :=
fun conjunction => Or.inr conjunction.right問題2分配則を導出木とLeanの場合分けで二重に記述する
Problem
問題
章本文の位置で見るP ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) の導出木を書きます。連言から P と Q ∨ R を取り出す節点、
選言で二分する節点、各枝で連言と最終的な選言を作る節点を明示してください。二枝が同じ結論型を持たなければ Or.elim を完了できないことも型で示します。
次に同じ導出をLeanで実装し、導出木の各節点と証明項の部分項を対応させます。
Or.elim と Classical.em の両方が二分を作るという外見上の類似だけでなく、前者が必要とする入力証拠と後者が追加する原理の差を述べてください。
ヒント
P ∧ (Q ∨ R) の連言を除去した後、選言のタグで場合分けします。
解答
仮定から p : P と qr : Q ∨ R を得ます。qr が左なら Or.inl ⟨p,q⟩、右なら
Or.inr ⟨p,r⟩ を返します。従って P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) です。導出木では最初に
連言除去、次に選言除去を置き、二分岐の末端で連言導入と選言導入を使います。
逆向きの分配則も、外側の選言で場合分けし、各分岐から共通の P と内側の選言を構成します。
theorem distribute (P Q R : Prop) :
P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) := by
rintro ⟨proofP, proofQ | proofR⟩
· exact Or.inl ⟨proofP, proofQ⟩
· exact Or.inr ⟨proofP, proofR⟩問題3古典原理を使った一点だけを定理の仮定へ抽出する
Problem
問題
章本文の位置で見る¬(P ∧ Q) → ¬P ∨ ¬Q の証明において、排中律をどの命題に対して一回だけ使えばよいかを決めます。
その排中律の証拠を関数の引数として外へ出し、残りの証明が構成的な規則だけで書ける定理の型と本体を作ってください。
二重否定導入 P → ¬¬P とその逆向きを比較し、証明項を単に「逆にする」操作が定義されない理由を、関数の始域・終域から説明します。
解答の最後に、どの行までが構成的に成立し、どの一行が追加仮定に依存するかを明示します。
ヒント
全体を Classical にする代わりに、場合分けに必要な命題の排中律だけを引数にします。
解答
¬(P ∧ Q) → ¬P ∨ ¬Q の構成では、P ∨ ¬P を仮定に取れば十分です。¬P なら右側の結論が直ちに得られ、
P なら Q を仮定したとき P ∧ Q が矛盾するので ¬Q を得ます。古典性を
emP : P ∨ ¬P という一引数へ局所化できます。
選択公理や関数外延性でも、使用箇所に必要な原理を明示的な引数として切り出すと、定理の依存範囲を比較できます。
theorem deMorganFromExcludedMiddle (P Q : Prop) (emP : P ∨ ¬P) :
¬(P ∧ Q) → ¬P ∨ ¬Q := by
intro notBoth
cases emP with
| inl proofP => exact Or.inr (fun proofQ => notBoth ⟨proofP, proofQ⟩)
| inr notP => exact Or.inl notP第8章
述語・全称量化・存在量化
問題本文問題1全称量化を依存する関数として追跡する
Problem
問題
章本文の位置で見るmapForall の全変数と仮定に型を書き、任意の x に対する allP x、transform x、transform x (allP x) の型を順に導いてください。
この導出を「任意の値を受け取る」段階と「その値で特殊化した証拠を受け取る」段階へ分け、依存関数の入出力として説明します。
¬∃ x, p x → ∀ x, ¬p x の証明項を同じ方法で構成し、任意の x と p x の証拠から、否定された存在証明をどのように作って矛盾を得るかを記述します。
古典原理を使わずに完成したことが、使用した構成子と関数の一覧から確認できれば完了です。
ヒント
入力 x によって出力型 p x が変わる関数として読みます。
解答
∀ x : α, p x の証明は、任意の x : α を受け取って p x の証明を返す依存関数です。
利用時には特定の a : α へ適用して p a を得ます。mapForall は各 x で
p x → q x を持ち、全称証明 hp から fun x => step x (hp x) を構成します。
依存関数型でも、引数に応じて結果型がどう置換されるかを同じ方法で追います。
theorem mapForall {α : Type} (p q : α → Prop)
(transform : ∀ x, p x → q x) (allP : ∀ x, p x) : ∀ x, q x :=
fun x => transform x (allP x)
theorem notExistsImpliesForallNot {α : Type} (p : α → Prop) :
(¬∃ x, p x) → ∀ x, ¬p x :=
fun noWitness x proof => noWitness ⟨x, proof⟩問題2存在証明の証人を保存して性質だけを変換する
Problem
問題
章本文の位置で見るmapExists の入力を、存在証明の分解、証人の保存、証拠の変換、新しい存在証明の構成という四段階に分けてください。
各段階で手元にある項とその型を表にし、新しい証人を探索する操作が一度も現れないことを示します。
その構造を使って (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x をterm modeとtactic modeの両方で証明します。
存在証人、連言の二成分、再構成された証拠の対応を明記し、二つの記法が同じ情報変換を表すことを示してください。
ヒント
存在証明を証人 x と証拠 p x に分解し、証人はそのまま再利用します。
解答
∃ x, p x から ⟨x,hp⟩ を取り出し、仮定 ∀ x, p x → q x を同じ x と hp へ適用して
hq : q x を得ます。返す存在証明は ⟨x,hq⟩ : ∃ x, q x です。証人を選び直していないため、
変換は性質の証拠だけに作用します。
Σ型の写像でも第一成分を保存して第二成分だけ変換できます。ただし第二成分が計算データか命題の証明かは区別します。
theorem swapExistsAndTerm {α : Type} (p q : α → Prop) :
(∃ x, p x ∧ q x) → ∃ x, q x ∧ p x :=
fun ⟨x, proofP, proofQ⟩ => ⟨x, proofQ, proofP⟩
theorem swapExistsAndTactic {α : Type} (p q : α → Prop) :
(∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
rintro ⟨x, proofP, proofQ⟩
exact ⟨x, proofQ, proofP⟩問題3量化子の順序と限定量化の論理形を反例で固定する
Problem
問題
章本文の位置で見る∀ n : Nat, ∃ m : Nat, n < m と ∃ m : Nat, ∀ n : Nat, n < m について、証明が提供しなければならないデータをそれぞれ関数型と対型の言葉で書いてください。
前者には m := n + 1 を与え、後者には任意の候補 m に対する反例 n := m を与え、真偽の差が量化子の順序だけから生じることを示します。
最後に、限定全称 ∀ x, S x → p x と ∀ x, S x ∧ p x を比較します。S を満たさない値が存在する最小の型と述語を選び、
後者が集合外の値にも S x を要求するため過強であることを反例で検証してください。
ヒント
証人が先行する変数を見て選べるかを比較し、二値の最小反例を作ります。
解答
各自然数 n を受け取った後なら m := n + 1 を選べるため、∀ n, ∃ m, n < m は真です。
一方、∃ m, ∀ n, n < m の証人候補 m には n := m を返すと m < m が必要になり、
反射律に反します。前者の証人は入力へ依存でき、後者では全入力より先に固定される点が違います。
極限の錐や一様連続性でも、対象ごとに選ぶデータと全対象に共通するデータを量化順序から判定します。
theorem everyNaturalHasLarger : ∀ n : Nat, ∃ m : Nat, n < m :=
fun n => ⟨n + 1, by omega⟩
theorem noLargestNatural : ¬∃ m : Nat, ∀ n : Nat, n < m := by
rintro ⟨m, largest⟩
exact (Nat.lt_irrefl m) (largest m)
def splitChoice (b : Bool) (n : Nat) : Prop :=
(b = true ∧ n = 0) ∨ (b = false ∧ n = 1)
theorem pointwiseChoice : ∀ b : Bool, ∃ n : Nat, splitChoice b n := by
intro b
cases b <;> simp [splitChoice]
theorem noUniformChoice : ¬∃ n : Nat, ∀ b : Bool, splitChoice b n := by
rintro ⟨n, all⟩
have atTrue := all true
have atFalse := all false
simp [splitChoice] at atTrue atFalse
omega別解
二値だけの模型でも差を確認できます。関係 R(b,n) を「b=true なら n=0、b=false なら n=1」と
定めます。各 b を見た後なら証人を選べるので ∀b,∃n,R(b,n) は成立します。しかし一つの n を先に
選ぶと、true から n=0、false から n=1 が同時に必要となるため ∃n,∀b,R(b,n) は成立しません。
この最小模型は、量化順序の差が証人の依存可能性そのものであることを示します。
第9章
等式・代入・外延性・一意存在
問題本文問題1等式除去を置き換えの原理として展開する
Problem
問題
章本文の位置で見るh : x = y から y = x を cases h と rfl だけで証明し、cases h の前後で文脈と目標がどう変わったかを書いてください。
この変化を「等式を場合分けした」という表面的な説明で済ませず、任意の述語 p : A → Prop に対して p x から p y へ移送できる原理の特殊例として述べます。
x = y と f = g から f x = g y を二通り証明します。一方は項の等式を先に消去し、他方は関数の等式を先に消去します。
中間目標を全て記録し、除去順が変わっても最終的な証拠の型が一致することを検証してください。
ヒント
等式 x = y と x で成立する性質 p x から、p y を作ります。
解答
等式除去は h : x = y に沿って証明 px : p x を輸送し、p y を得る原理です。h が rfl の場合、
始点と終点は同じなので結果は px そのものです。一般の h は等式帰納法によりこの反射の場合へ還元できます。
関数合同性 f x = f y も、性質を「出力が f x に等しい」と選ぶ置き換えです。
ベクトルの長さや依存対では、性質の結果型そのものが変わります。通常の書換えも輸送の特殊例として追えます。
theorem symmetryByElimination {α : Type} {x y : α} (equal : x = y) : y = x := by
cases equal
rfl
theorem congruenceTwoWays {α β : Type} {x y : α} {f g : α → β}
(equalInput : x = y) (equalFunction : f = g) : f x = g y := by
cases equalInput
cases equalFunction
rfl
theorem congruenceFunctionsFirst {α β : Type} {x y : α} {f g : α → β}
(equalInput : x = y) (equalFunction : f = g) : f x = g y := by
cases equalFunction
cases equalInput
rfl問題2定義的等しさと外延性の役割分担を証明の各段で指す
Problem
問題
章本文の位置で見るcomposeAssociative の証明を、関数等式を点ごとの等式へ移す段階と、各点で両辺が計算によって同じ項になる段階に分けてください。
funext と rfl のどちらかを取り除いた場合に、どの形の目標が未解決で残るかを具体的に示します。
さらに定数関数 fun _ : Bool => 0 を使い、f false = f true が成り立っても false = true は導けないことを反例として完成させます。
関数合同性と関数外延性を逆向きの原理と誤読せず、逆を得るには単射性という追加仮定が必要だと説明してください。
ヒント
計算だけで両辺が同じ式になる段階と、関数全体の等式へ持ち上げる段階を分けます。
解答
合成の結合則を任意の x へ適用すると、両辺は定義の展開により h (g (f x)) へ簡約されます。
この点ごとの等式は rfl で成立します。しかし関数 h ∘ (g ∘ f) と (h ∘ g) ∘ f 自体を同一視するには、
「全ての入力で等しい関数は等しい」という関数外延性を使います。計算と外延原理の役割は別です。
自然変換や構造体の等式でも、成分ごとの計算と、成分等式から全体等式を得る外延原理を分離します。
theorem compositionAssociative {α β γ δ : Type}
(h : γ → δ) (g : β → γ) (f : α → β) :
(fun x => h (g (f x))) = (fun x => (h ∘ g) (f x)) := by
funext x
rfl
example : (fun _ : Bool => 0) false = (fun _ : Bool => 0) true := rfl
example : false ≠ true := by decide問題3存在と一意存在が持つ証拠の成分を分解する
Problem
問題
章本文の位置で見る∃ x, p x の証明と ExistsExactlyOne p の証明を、証人、性質の証明、任意の他の候補との等式という成分に分けてください。
存在証明だけでは二つの候補が異なることを排除できない例と、一意性だけでは候補が一つも存在しない場合を排除できない例をそれぞれ作ります。
最後に、Nat 上で「x + 1 = 3」の一意解を述べる命題を書き、存在、性質、一意性の各部を個別に証明します。
解答は ∃! の記法だけで終えず、Leanの構成子へ展開したときにどの証明がどのフィールドを満たすかまで示します。
ヒント
一意存在には証人、存在性の証拠、任意の別証人が元の証人に等しい証拠があります。
解答
∃ x, p x は x と p x の二成分です。一意存在はさらに、任意の y が p y を満たすなら
y = x であるという一意性を持ちます。述語 fun x : Nat => x + 1 = 3 では証人を 2 とし、
存在性は 2 + 1 = 3、一意性は y + 1 = 3 から y = 2 を導く証明です。
普遍対象では「媒介射が存在する」と「その射が一意である」を同じ三成分で読みます。後の圏論でそのまま再利用します。
def ExistsExactlyOne {α : Type} (p : α → Prop) : Prop :=
∃ x, p x ∧ ∀ y, p y → y = x
theorem uniqueSolution : ExistsExactlyOne (fun x : Nat => x + 1 = 3) := by
refine ⟨2, by omega, ?_⟩
intro y satisfiesEquation
omega第10章
自然演繹・シーケント計算・証明の正規化
問題本文問題1一つの含意証明を三表現で再構成する
Problem
問題
章本文の位置で見る命題 (A ⟶ B) ⟶ A ⟶ B を自然演繹の導出木、NaturalDeduction の構成子、ラムダ項の三通りで
書いてください。各仮定が導入される位置、使用される位置、解除される位置へ同じ番号を振ります。
三表現を並べ、構文が違っても保存される情報と、一方だけに明示される情報を説明できれば完了です。
ヒント
A → A を、導出木、ラムダ項、シーケントの三つで表し、仮定の導入と利用を対応させます。
解答
自然演繹では A ⟶ B と A を仮定し、含意除去で B を得た後、二回の含意導入によって
⊢ (A ⟶ B) ⟶ A ⟶ B を得ます。NaturalDeduction では二つの .impIntro、二つの .hyp、
それらを結ぶ .impElim が同じ導出木を表します。ラムダ項は λf. λa. f a です。
含意合成では二つの含意除去と一つの含意導入が、ラムダ項の二回適用、シーケントのcutへ対応します。
open FormalLab.Logic.ProofSystems
def implicationApplication (A B : Formula) :
NaturalDeduction [] ((A ⟶ B) ⟶ A ⟶ B) :=
.impIntro <| .impIntro <|
.impElim (.hyp (A := A ⟶ B) (by simp)) (.hyp (A := A) (by simp))
def implicationApplicationTerm : ProofTerm :=
.lam (.lam (.app (.var 1) (.var 0)))問題2正規化前後で結論と仮定を保存する
Problem
問題
章本文の位置で見る(λx. x) u と、定数関数を直ちに適用する項を ProofTerm で作り、一段縮約してください。
縮約前後で自由変数が不意に捕獲されないことを添字ごとに確認します。次に内側だけにredexを持つ項を
作り、本章の関数が縮約しない理由を仕様から説明し、完全な正規化器に必要な探索規則を列挙します。
ヒント
導入直後の除去を縮約し、消えた仮定が代入先で正しく使われるかを確認します。
解答
証明項 (λx.t) s は t[x:=s] へ簡約されます。型付けで x:A ⊢ t:B と ⊢ s:A があれば、
代入補題により ⊢ t[x:=s]:B です。従って簡約前後で結論 B は保存されます。自由な仮定は代入で
捕獲されず、元の文脈に残ります。正規化は証明可能な結論を変えず、迂回した導入・除去だけを除きます。
プログラムのβ簡約では「結論」を型へ読み替えると保存定理になります。証明正規化と型安全性を同じ代入補題が支えます。
open FormalLab.Logic.ProofSystems
example :
contractIntroductionElimination? (.app (.lam (.var 0)) (.var 3)) =
some (.var 3) := rfl
example :
contractIntroductionElimination? (.app (.lam (.lam (.var 1))) (.var 0)) =
some (.lam (.var 1)) := rfl問題3cutの便利さと除去可能性を区別する
Problem
問題
章本文の位置で見るヒント
補題を一度証明して再利用する構成と、その補題なしの導出が存在するというメタ定理を分けます。
解答
cut規則は Γ ⊢ A と Δ,A ⊢ B を合成し、Γ,Δ ⊢ B を得ます。中間命題 A を補題として使えるため、
導出を構造化するのに便利です。cut除去定理は、cutを使った任意の導出をcutなしの導出へ変換できると述べます。
これはcutが無意味だという主張ではなく、証明可能性を増やさないという保存的な主張です。
補題、局所定義、中間表現を除去できるという定理でも、記述上の有用性と表現力への影響を別々に評価します。
open FormalLab.Logic.ProofSystems
def identityWithCut (A : Formula) : Sequent [] (A ⟶ A) :=
.cut (sequentIdentity A) (.ax (by simp))
def identityWithoutCut (A : Formula) : CutFree [] (A ⟶ A) :=
.impRight (.ax (by simp))