diff --git a/Examples/Exercise/BarberParadox.lean b/Examples/Exercise/BarberParadox.lean new file mode 100644 index 00000000..60203004 --- /dev/null +++ b/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 diff --git a/Examples/Exercise/DeMorganAndEm.lean b/Examples/Exercise/DeMorganAndEm.lean new file mode 100644 index 00000000..019fe291 --- /dev/null +++ b/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 diff --git a/Examples/Exercise/ImpDefValidness.lean b/Examples/Exercise/ImpDefValidness.lean new file mode 100644 index 00000000..5f785dc0 --- /dev/null +++ b/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` は、`→ᵥ` の部分を同値関係 `↔` に読み替えるとともはや正しくありません。つまり、同値関係の話に読み替えたら成り立たなくなるような要請を、どれか一つ必ず使用するはずですね。 + +-/ diff --git a/Examples/Exercise/README.lean b/Examples/Exercise/README.lean new file mode 100644 index 00000000..17557cf6 --- /dev/null +++ b/Examples/Exercise/README.lean @@ -0,0 +1 @@ +/- # 演習問題 -/ diff --git a/Examples/Solution/BarberParadox.lean b/Examples/Solution/BarberParadox.lean new file mode 100644 index 00000000..e406f125 --- /dev/null +++ b/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 diff --git a/Examples/Solution/DeMorganAndEm.lean b/Examples/Solution/DeMorganAndEm.lean new file mode 100644 index 00000000..df39b7c4 --- /dev/null +++ b/Examples/Solution/DeMorganAndEm.lean @@ -0,0 +1,248 @@ +/- # 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 + -- P ∨ Q が成り立たないと仮定する + intro (h : ¬ (P ∨ Q)) + + -- このとき ¬ P が示せる + have notP : ¬ P := by + -- P を仮定すると + intro hp + -- P ∨ Q が成り立つ。 + have or : P ∨ Q := Or.inl hp + -- これは仮定から矛盾 + contradiction + + -- 同様に ¬ Q も示せる + have notQ : ¬ Q := by + intro hq + have or : P ∨ Q := Or.inr hq + contradiction + + -- したがって `¬ P ∧ ¬ Q` が成り立つ + exact ⟨notP, notQ⟩ + -- sorry + +--##-- +-- 別解：ライブラリを使う場合 +example (P Q : Prop) : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q := by simp [not_or] +--##-- + +theorem not_or_mpr (P Q : Prop) : ¬ P ∧ ¬ Q → ¬ (P ∨ Q) := by + -- sorry + -- ¬ P ∧ ¬ Q と仮定する + intro (h : ¬ P ∧ ¬ Q) + + -- P ∨ Q が成り立つと仮定する + intro hor + + -- P が成り立つか Q が成り立つかで場合分けする + rcases hor with hP | hQ + + -- P が成り立つ場合 + case inl => + -- これは仮定と矛盾 + exact h.left hP + + -- Q が成り立つ場合 + case inr => + -- これも仮定と矛盾 + exact h.right hQ + -- sorry + +--##-- +-- 別解：ライブラリを使う場合 +example (P Q : Prop) : ¬ P ∧ ¬ Q → ¬ (P ∨ Q) := by simp [not_or] +--##-- + +/- ## 問2 +次に、論理積の中に否定を入れる方を Lean で証明してみましょう。以下の `sorry` の部分を埋めてください。 +-/ + +theorem not_and_mp (P Q : Prop) : ¬ (P ∧ Q) → ¬ P ∨ ¬ Q := by + -- sorry + -- ¬ (P ∧ Q) と仮定する + intro h + + -- P が成り立つか否かで場合分けする + by_cases hP : P + + -- P が成り立つ場合 + case pos => + -- このとき `¬ Q` が成り立つ + have nQ : ¬ Q := by + intro hQ + exact h ⟨hP, hQ⟩ + + -- したがって `¬ P ∨ ¬ Q` が成り立つ + right + assumption + + -- P が成り立たない場合 + case neg => + -- このときは明らかに `¬ P ∨ ¬ Q` が成り立つ + left + assumption + -- sorry + +--##-- +-- 別解：ライブラリを使う場合 +example (P Q : Prop) : ¬ (P ∧ Q) → ¬ P ∨ ¬ Q := by + simp [not_and, Classical.or_iff_not_imp_left] +--##-- + +theorem not_and_mpr (P Q : Prop) : ¬ P ∨ ¬ Q → ¬ (P ∧ Q) := by + -- sorry + -- `¬ P ∨ ¬ Q` と仮定する + intro h + + -- `P ∧ Q` が成り立つと仮定する + intro ⟨hP, hQ⟩ + + -- 仮定から `¬ P` または `¬ Q` が成り立つが、 + rcases h with hnP | hnQ + + -- どちらの場合でも矛盾する + all_goals contradiction + -- sorry + +--##-- +-- 別解：ライブラリを使う場合 +example (P Q : Prop) : ¬ P ∨ ¬ Q → ¬ (P ∧ Q) := by + simp [not_and, Classical.or_iff_not_imp_left] +--##-- + +/- ## 問3 +問1の命題は、排中律を使わずに示すことができます。問2も、`not_and_mpr` の方は排中律なしで証明できます。 + +証明で使用した公理を [`#print`](../Command/Diagnostic/Print.md) コマンドで確認してみましょう。排中律を使うと `Classical.choice` という公理が使用されるので、この公理が使われていなければ排中律は使っていません。 + +ここまでの `not_and_mp` 以外の3つの命題について、排中律をもし使っていたら使わない証明に書き換えてみてください。 -/ + +--##-- +-- この模範解答では、不必要な公理を使用しない方法を紹介している。 + +/-- info: 'not_or_mp' does not depend on any axioms -/ +#guard_msgs in + #print axioms not_or_mp + +/-- info: 'not_or_mpr' does not depend on any axioms -/ +#guard_msgs in + #print axioms not_or_mpr + +/-- info: 'not_and_mpr' does not depend on any axioms -/ +#guard_msgs in + #print axioms not_and_mpr +--##-- + +/- ## 問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 + have := @not_and P Q + assumption + -- sorry + +/-- de Morgan の法則（論理積の中に否定を入れる）と弱い排中律が同値 -/ +theorem not_and_iff_weak_em : not_and_mp ↔ weak_em := by + -- sorry + -- 左方向と右方向をそれぞれ示す + constructor <;> intro h + + -- 弱い排中律を示す方向 + case mp => + -- `P : Prop` が与えられたとする + intro P + + -- de Morgan の法則に適用すると、 + -- `¬ (P ∧ ¬ P)` を示せばよいことがわかる + have := h P (¬ P) + apply this + + -- `P ∧ ¬ P` が成り立つと仮定すると、 + intro ⟨hP, hnP⟩ + + -- ただちに矛盾が導かれるので、示すべきことがいえた。 + contradiction + + -- de Morganの法則を示す方向 + case mpr => + -- 命題 `P` と `Q` が与えられたとする + intro P Q + + -- `¬ (P ∧ Q)` が成り立つと仮定する + intro hand + + -- 仮定の弱い排中律を P と Q に適用する + have em_p := h P + have em_q := h Q + + -- これを使って4通りの場合分けをする + rcases em_p with hnP | hnnP <;> rcases em_q with hnQ | hnnQ + + -- `¬¬ P` かつ `¬¬ Q` の場合以外は、あきらか + case inl.inl => exact Or.inl hnP + case inl.inr => exact Or.inl hnP + case inr.inl => exact Or.inr hnQ + + -- `¬¬ P` かつ `¬¬ Q` の場合は、矛盾を示したい + exfalso + + -- currying 補題を使って `P → ¬ Q` が得られる + have := (currying P Q).mp + replace hand := this hand + + -- よって、¬ P であることがわかる + replace : ¬ P := by + -- P だと仮定すると + intro hP + + -- 仮定から ¬ Q が導かれる + have nQ : ¬ Q := hand hP + + -- これは矛盾 + contradiction + + -- 仮定から `¬¬ P` なのでこれは矛盾 + contradiction + -- sorry + +-- 使用した公理を確認する +#print axioms not_and_iff_weak_em + +--##-- +-- 公理に依存していないことを確認している + +/-- info: 'Playground.not_and_iff_weak_em' does not depend on any axioms -/ +#guard_msgs in + #print axioms not_and_iff_weak_em +--##-- + +end Playground diff --git a/Examples/Solution/ImpDefValidness.lean b/Examples/Solution/ImpDefValidness.lean new file mode 100644 index 00000000..03808178 --- /dev/null +++ b/Examples/Solution/ImpDefValidness.lean @@ -0,0 +1,87 @@ +/- # 含意の定義の正当性 + +## イントロダクション + +論理学を学び始めた初心者がよく抱く疑問の一つに、「『ならば』の定義に納得がいかない」というのがあります。「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 + -- Q が成り立つかどうかで場合分けする + by_cases hQ : Q + + -- Q が成り立つ場合 + case pos => + -- 含意の導入から従う + apply imp_introduce hQ + + -- Q が成り立たない場合 + case neg => + -- このとき P も Q も False なので、これらは同値である + have : P ↔ Q := by exact (iff_false_right hQ).mpr nP + rw [this] + + -- したがって含意が反射的であることから従う + exact imp_reflexive + -- sorry + +/- +## ヒント + +どの要請が絶対に必要なのか考えてみるといいかもしれません。示したい命題 `imp_of_ant_false` は、`→ᵥ` の部分を同値関係 `↔` に読み替えるとともはや正しくありません。つまり、同値関係の話に読み替えたら成り立たなくなるような要請を、どれか一つ必ず使用するはずですね。 + +-/ diff --git a/Examples/Solution/README.lean b/Examples/Solution/README.lean new file mode 100644 index 00000000..17557cf6 --- /dev/null +++ b/Examples/Solution/README.lean @@ -0,0 +1 @@ +/- # 演習問題 -/ diff --git a/lake-manifest.json b/lake-manifest.json index 6839f5d8..3270c2e9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,21 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/Seasawher/mdgen", + [{"url": "https://github.com/Seasawher/mk-exercise.git", "type": "git", "subDir": null, "scope": "", - "rev": "bddd1ec2c02d86e4d5fecb0259471bf282df6a0a", + "rev": "fab402156f204c1629afdcb12eb0634cf9123203", + "name": "«mk-exercise»", + "manifestFile": "lake-manifest.json", + "inputRev": "2.0.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/Seasawher/mdgen", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6d86fc91c6ed2b173b6d0b31a6d7b7c9af41d366", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "08ecf4c7e62daf335fa2f9e42d6ad90574211eb5", + "rev": "07a0ae9126dff1d2838a59b03ac6763e22ed6cb4", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lakefile.lean b/lakefile.lean index 0d52bd8b..32f8a584 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,6 +7,9 @@ package «Lean by Example» where ⟨`relaxedAutoImplicit, false⟩ ] +require «mk-exercise» from git + "https://github.com/Seasawher/mk-exercise.git" @ "2.0.0" + require mdgen from git "https://github.com/Seasawher/mdgen" @ "main" @@ -28,6 +31,7 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do return hasError script build do + if ← runCmd "lake" #["exe", "mk_exercise", "Examples/Solution", "Examples/Exercise"] then return 1 if ← runCmd "lake" #["exe", "mdgen", "Examples", "src"] then return 1 if ← runCmd "mdbook" #["build"] then return 1 return 0 diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 28d22d0f..49302759 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -6,6 +6,8 @@ --- +# リファレンス + - [コマンド](./Command/README.md) - [対話的コマンド](./Command/Diagnostic/README.md) - [#check_failure: 意図的なエラー](./Command/Diagnostic/CheckFailure.md) @@ -154,3 +156,10 @@ - [型](./Term/Type/README.md) - [Prop: 命題全体](./Term/Type/Prop.md) - [Type: 型全体](./Term/Type/Type.md) + +# ガイド + +- [演習問題](./Exercise/README.md) + - [床屋のパラドクス](./Exercise/BarberParadox.md) + - [De Morganの法則と排中律](./Exercise/DeMorganAndEm.md) + - [含意の定義の正当性](./Exercise/ImpDefValidness.md)