Merge pull request #632 from lean-ja/guide

演習問題を追加する

Examples/Exercise/BarberParadox.lean

@@ -0,0 +1,35 @@
+/- # 床屋のパラドックス
+集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。
+
+この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。
+
+以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。
+
+その内容は自然言語では次のように説明できます。
+
+> ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？
+>
+> 仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。
+>
+> いずれにせよ矛盾が生じてしまいます。
+
+この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。
+-/
+namespace Barber
+
+/-- 全体集合となる人々の集合 -/
+opaque Person : Type
+
+/-- p さんが q さんの髭を剃るという述語 -/
+opaque shave (p q : Person) : Prop
+
+-- 床屋が存在するという仮定
+variable (barber : Person)
+
+-- 床屋の信念を仮定として表現したもの
+variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p)
+
+example : False := by
+  sorry
+
+end Barber

Examples/Exercise/DeMorganAndEm.lean

@@ -0,0 +1,70 @@
+/- # De Morgan の法則と排中律
+
+論理和 `∨` と論理積 `∧` の間に次の関係が成立することが知られています。
+
+1. `¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q`
+1. `¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q`
+
+これは De Morgan の法則と呼ばれているものの一部です。
+
+## 問1
+
+最初の、論理和の中に否定を入れる方を Lean で証明していきましょう。以下の `sorry` の部分を埋めてください。
+
+`simp` や `rw` でライブラリの命題を引用する方法でも示すことができますし、使わずに自力で示すこともできます。どちらでも構いませんが、Lean に慣れていない人は自力で示すのに挑戦してみてください。
+-/
+
+theorem not_or_mp (P Q : Prop) : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q := by
+  sorry
+
+
+theorem not_or_mpr (P Q : Prop) : ¬ P ∧ ¬ Q → ¬ (P ∨ Q) := by
+  sorry
+
+
+/- ## 問2
+次に、論理積の中に否定を入れる方を Lean で証明してみましょう。以下の `sorry` の部分を埋めてください。
+-/
+
+theorem not_and_mp (P Q : Prop) : ¬ (P ∧ Q) → ¬ P ∨ ¬ Q := by
+  sorry
+
+
+theorem not_and_mpr (P Q : Prop) : ¬ P ∨ ¬ Q → ¬ (P ∧ Q) := by
+  sorry
+
+
+/- ## 問3
+問1の命題は、排中律を使わずに示すことができます。問2も、`not_and_mpr` の方は排中律なしで証明できます。
+
+証明で使用した公理を [`#print`](../Command/Diagnostic/Print.md) コマンドで確認してみましょう。排中律を使うと `Classical.choice` という公理が使用されるので、この公理が使われていなければ排中律は使っていません。
+
+ここまでの `not_and_mp` 以外の3つの命題について、排中律をもし使っていたら使わない証明に書き換えてみてください。 -/
+
+
+/- ## 問4
+4つの中で唯一排中律が必要だったのは `not_and_mp` です。実はこの命題は、直観主義論理において弱い排中律 `¬ P ∨ ¬ ¬ P` と同値になることが知られています。
+
+これを Lean で証明してみましょう。以下の `sorry` の部分を埋めてください。証明が終わったら、証明が排中律に依存していないことを `#print` コマンドで確認することをお忘れなく。
+-/
+namespace Playground
+
+/-- de Morgan の法則（論理積の中に否定を入れる） -/
+def not_and_mp := ∀ (P Q : Prop), ¬ (P ∧ Q) → ¬ P ∨ ¬ Q
+
+/-- 弱い排中律 -/
+def weak_em := ∀ (P : Prop), ¬ P ∨ ¬ ¬ P
+
+/-- カリー化の特殊な場合。証明の中で役に立つかも？ -/
+theorem currying (P Q : Prop) : ¬ (P ∧ Q) ↔ (P → ¬ Q) := by
+  sorry
+
+/-- de Morgan の法則（論理積の中に否定を入れる）と弱い排中律が同値 -/
+theorem not_and_iff_weak_em : not_and_mp ↔ weak_em := by
+  sorry
+
+-- 使用した公理を確認する
+#print axioms not_and_iff_weak_em
+
+
+end Playground

Examples/Exercise/ImpDefValidness.lean

@@ -0,0 +1,70 @@
+/- # 含意の定義の正当性
+
+## イントロダクション
+
+論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「P ならば Q」は論理学では P が偽ならば Q が何であっても真であるものとして定義しますが、それが直観に反するという疑問です。
+
+自然言語における「ならば」は、あまりこのような使い方をしませんので、確かに違和感がありますね。たとえば、「意味が分かると怖い話」の中にただただ意味不明なだけの話は普通含まれませんよね！
+
+この演習問題では、この疑問に対する一つの答えを提示します。つまり、含意が満たしていて欲しい最低限の性質をいくつか列挙し、それを満たす「何か」の定義はただ一つしかないということを確認します。
+
+> **注意**
+>
+> 自然言語における「ならば」と論理学における含意の間には埋めがたい溝もあります。たとえば「`1 = 1` ならば、すべての実数 `x` に対して `x ^ 2 ≥ 0` である」という命題は正しいですが、自然言語としてはかなり違和感があります。ここでの前提と結論の間には何も意味上の関係がないように見えるからです。
+>
+> しかし、命題から命題への関数として含意を定義しようとしている以上、同値な命題同士を入れ替えても真偽が変わってはいけないので、意味上の関連を持たせることは不可能です。つまり、関数で自然言語の「ならば」を再現することはできないのです。
+>
+> したがって、ここで私たちが主張できることは、あくまで「関数で自然言語の『ならば』を近似しようとするならば、現行の論理学における定義が最も近い」ということであって、決して「自然言語の『ならば』と論理学における含意に実質的な違いがない」ということではありません。注意して下さい。
+
+## 含意が満たしていて欲しい性質
+
+まずは、含意に相当する「何か」を定義しましょう。それは、命題から命題への2引数関数になっているはずです。ここではその何かに `Imp` という名前をつけ、`→ᵥ` という記号で表すことにします。
+-/
+-- 含意が満たすべき性質を満たす「何か」
+opaque Imp (P Q : Prop) : Prop
+
+-- 含意っぽい記法の導入
+-- `v` は `virtual` の略
+infixr:40 " →ᵥ " => Imp
+
+/- これだけだと型があるだけのノッペラボーなので、性質を与えていきましょう。含意が満たしているべき性質とはなんでしょうか？
+
+含意は、直観的には「～を前提とすれば…が成り立つ」ということを意味しています。ですから、特に前提と結論が同じであれば必ず成り立つはずですね。したがって反射性を要請することは妥当に思えます。 -/
+
+/-- 含意は反射的。前提 P が真だろうと偽だろうと「P ならば P」は正しい。 -/
+axiom imp_reflexive {P : Prop} : P →ᵥ P
+
+/- また、「～を前提とすれば…が成り立つ」という解釈から、`P →ᵥ Q` と `P` が両方成り立っていたら結論の `Q` が成り立っているべきであることも要請できそうです。 -/
+
+/-- モーダスポネンス。「P ならば Q」は、P が正しければ Q が成り立つことを意味する。 -/
+axiom modus_ponens {P Q : Prop} (hpq : P →ᵥ Q) (hP : P) : Q
+
+/- さらに、ある推論で `Q` が結論できるなら、前提を増やしても同じ結論が得られるはずですね。このことにより、結論 `Q` が前提なしで真ならば、任意の `P` に対して `P →ᵥ Q` が成り立っているべきだということが要請できます。 -/
+
+/-- 結論が無条件に正しいなら、仮定をつけても正しい -/
+axiom imp_introduce {P Q : Prop} (hQ : Q) : P →ᵥ Q
+
+/- 最後に、含意による関係は推移的であることを要請できます。つまり `P` から `Q` が結論出来て、`Q` から `R` が結論できるなら `P` から `R` が結論できるはずでしょう。 -/
+
+/-- 含意は推移的 -/
+axiom imp_transitive {P Q R : Prop} (hpq : P →ᵥ Q) (hqr : Q →ᵥ R) : P →ᵥ R
+
+/- ## 問題
+以上の要請のもとで、前提 `P` が偽であるとき `P →ᵥ Q` が `Q` に関係なく真になることが証明できます。以下の注意点に気を付けながら、`sorry` を埋めてみてください。
+
+* 排中律は自由に使って構いません。
+* 本文中で課した4つの要請は、全部使う必要はありません。
+-/
+
+variable {P Q : Prop}
+
+/-- 前件(antecedent)が偽であるとき、「P ならば Q」は真 -/
+theorem imp_of_ant_false (nP : ¬ P) : P →ᵥ Q := by
+  sorry
+
+/-
+## ヒント
+
+どの要請が絶対に必要なのか考えてみるといいかもしれません。示したい命題 `imp_of_ant_false` は、`→ᵥ` の部分を同値関係 `↔` に読み替えるとともはや正しくありません。つまり、同値関係の話に読み替えたら成り立たなくなるような要請を、どれか一つ必ず使用するはずですね。
+
+-/

Examples/Exercise/README.lean

@@ -0,0 +1 @@
+/- # 演習問題 -/

Examples/Solution/BarberParadox.lean

@@ -0,0 +1,41 @@
+/- # 床屋のパラドックス
+集合論が提唱された当初、任意の述語 `P` に対して `P` を満たす要素の集合 `{ x | P x }` が存在するとされていました。このルールを内包公理と呼びます。`P` が成り立つ要素を集めてくることができると主張しているわけで、直観的で受け入れやすいと思われます。しかし、特に述語 `P` として「自分自身を含まない」という述語を採用すると、矛盾が生じることが知られています。これは Russel のパラドックスと呼ばれています。
+
+この問題を回避する方法は複数ありえますが、現在広く採用されている ZFC 集合論では、内包公理の適用範囲を部分集合に限定して主張を弱めることで Russel のパラドックスを回避しています。
+
+以上が Russel のパラドックスの概要です。床屋のパラドックスとは、Russel のパラドックスの内容をわかりやすく説明するために考えられた比喩です。
+
+その内容は自然言語では次のように説明できます。
+
+> ある村に床屋がいます。その床屋は、自分で髭を剃る村人の髭は剃らず、自分で髭を剃らない村人の髭を剃るという信念を持っています。このとき、その床屋は自分の髭を剃るでしょうか？
+>
+> 仮に剃るとしたら、その床屋はまさに「自分で自分の髭を剃っている」ので剃ってはならないはずで、矛盾が生じます。逆に剃らないとすると、その床屋はまさに「自分で自分の髭を剃らない」ので自分の髭を剃らなければならないことになり、矛盾が生じます。
+>
+> いずれにせよ矛盾が生じてしまいます。
+
+この内容を Lean で表現してみましょう。演習問題として、`sorry` の部分を埋めてみてください。
+-/
+namespace Barber
+
+/-- 全体集合となる人々の集合 -/
+opaque Person : Type
+
+/-- p さんが q さんの髭を剃るという述語 -/
+opaque shave (p q : Person) : Prop
+
+-- 床屋が存在するという仮定
+variable (barber : Person)
+
+-- 床屋の信念を仮定として表現したもの
+variable (policy : ∀ p : Person, shave barber p ↔ ¬ shave p p)
+
+example : False := by
+  -- sorry
+  -- 床屋は自分自身の髭を剃るだろうか？
+  replace policy := policy barber
+
+  -- `P ↔ ¬ P` という形の仮定が得られて、これは矛盾
+  simp at policy
+  -- sorry
+
+end Barber