From d678742aef20510bc0267afe775ecff06f4b37e6 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 9 Sep 2024 22:08:08 +0900
Subject: [PATCH 1/2] =?UTF-8?q?De=20Morgan=E3=81=AE=E5=95=8F=E9=A1=8C?=
 =?UTF-8?q?=E3=82=92=E3=80=81Heyting=E4=BB=A3=E6=95=B0=E3=81=AE=E5=85=AC?=
 =?UTF-8?q?=E7=90=86=E3=81=8B=E3=82=89Bool=E4=BB=A3=E6=95=B0=E3=81=AE?=
 =?UTF-8?q?=E5=85=AC=E7=90=86=E3=81=8C=E7=8B=AC=E7=AB=8B=E3=81=A7=E3=81=82?=
 =?UTF-8?q?=E3=82=8B=E3=81=93=E3=81=A8=E3=82=92=E7=A4=BA=E3=81=99=E5=95=8F?=
 =?UTF-8?q?=E9=A1=8C=E3=81=AB=E5=B7=AE=E3=81=97=E6=9B=BF=E3=81=88=E3=82=8B?=
 =?UTF-8?q?=20Fixes=20#721?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Solution/HeytingAndBooleanAlgebra.lean    | 350 ++++++++++++++++++
 Exercise/HeytingAndBooleanAlgebra.lean        | 339 +++++++++++++++++
 src/SUMMARY.md                                |   1 +
 3 files changed, 690 insertions(+)
 create mode 100644 Examples/Solution/HeytingAndBooleanAlgebra.lean
 create mode 100644 Exercise/HeytingAndBooleanAlgebra.lean

diff --git a/Examples/Solution/HeytingAndBooleanAlgebra.lean b/Examples/Solution/HeytingAndBooleanAlgebra.lean
new file mode 100644
index 00000000..631b1516
--- /dev/null
+++ b/Examples/Solution/HeytingAndBooleanAlgebra.lean
@@ -0,0 +1,350 @@
+/- # Heyting 代数と Bool 代数
+直観主義論理において、排中律 `P ∨ ¬ P` は独立な命題であることが知られています。つまり、証明も反証(否定を証明すること)もできません。今回の演習問題では、それに関連した話題として、Bool 代数ではない Heyting 代数が存在することを示します。
+
+ここでは Mathlib をなぞるように理論を構成していきます。
+
+## 半順序集合
+まず準備として、半順序集合を定義します。半順序集合には順序が定義されていますが、要素を2つ与えられたときにどちらが大きいのか比較できるとは限らないことに注意してください。
+-/
+import Aesop --#
+set_option autoImplicit false --#
+set_option relaxedAutoImplicit false --#
+
+/-- 半順序集合 -/
+class PartialOrder (α : Type) extends LE α, LT α where
+  /-- `≤` は反射的である -/
+  le_refl : ∀ a : α, a ≤ a
+
+  /-- `≤` は推移的である -/
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+
+  /-- `<` のデフォルト実装 -/
+  lt := fun a b => a ≤ b ∧ ¬ b ≤ a
+
+  /-- `<` と `≤` の関係 -/
+  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a
+
+  /-- `≤` は半対称的 -/
+  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
+
+/- ## 束
+半順序集合であって、任意の2つの要素 `a, b` に対して上限 `a ⊔ b` と下限 `a ⊓ b` が存在するものを束といいます。上限は最小の上界を意味し、下限は最大の下界を意味します。
+
+上限の記号 `⊔` は論理和 `∨` に、下限の記号 `⊓` は論理積 `∧` に、それぞれ似ています。またそれぞれ集合の合併 `∪` と共通部分 `∩` にも似ています。これは、`Prop` と `Set α` がともに束になっていることと整合性があります。
+-/
+
+section Lattice
+
+/-- `⊔` という記号のための型クラス -/
+class Sup (α : Type) where
+  /-- 最小上界、上限 -/
+  sup : α → α → α
+
+/-- `⊓` という記号のための型クラス -/
+class Inf (α : Type) where
+  /-- 最大下界、下限 -/
+  inf : α → α → α
+
+@[inherit_doc] infixl:68 " ⊔ " => Sup.sup
+
+@[inherit_doc] infixl:69 " ⊓ " => Inf.inf
+
+/-- 任意の2つの要素 `a, b` に対して上限 `a ⊔ b` が存在するような半順序集合 -/
+class SemilatticeSup (α : Type) extends Sup α, PartialOrder α where
+  /-- `a ⊔ b` は `a` と `b` の上界になっている -/
+  le_sup_left : ∀ a b : α, a ≤ a ⊔ b
+
+  /-- `a ⊔ b` は `a` と `b` の上界になっている -/
+  le_sup_right : ∀ a b : α, b ≤ a ⊔ b
+
+  /-- `a ⊔ b` は `a`, `b` の上界の中で最小のもの -/
+  sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c
+
+/--  任意の2つの要素 `a, b` に対して下限 `a ⊓ b` が存在するような半順序集合 -/
+class Semilatticeinf (α : Type) extends Inf α, PartialOrder α where
+  /-- `a ⊓ b` は `a` と `b` の下界になっている -/
+  inf_le_left : ∀ a b : α, a ⊓ b ≤ a
+
+  /-- `a ⊓ b` は `a` と `b` の下界になっている -/
+  inf_le_right : ∀ a b : α, a ⊓ b ≤ b
+
+  /-- `a ⊓ b` は `a`, `b` の下界の中で最大のもの -/
+  le_inf : ∀ a b c : α, c ≤ a → c ≤ b → c ≤ a ⊓ b
+
+/-- 束 -/
+class Lattice (α : Type) extends SemilatticeSup α, Semilatticeinf α
+
+end Lattice
+
+/- ## Heyting 代数
+ここまでの準備の下、Heyting 代数を定義することができます。Heyting 代数とは束であって、以下の条件を満たすものです。
+
+1. 最大の要素 `⊤` が存在する。
+2. 最小の要素 `⊥` が存在する。
+3. 下限 `· ⊓ b` の右随伴 `b ⇨ ·` が存在する。つまり任意の `a, b, c` に対して `a ⊓ b ≤ c` と `a ≤ b ⇨ c` が同値。
+-/
+
+section HeytingAlgebra
+
+/-- `⊤` という記号のための型クラス -/
+class Top (α : Type) where
+  /-- 最大元 -/
+  top : α
+
+@[inherit_doc] notation "⊤" => Top.top
+
+/-- `⊥` という記号のための型クラス -/
+class Bot (α : Type) where
+  /-- 最小元 -/
+  bot : α
+
+@[inherit_doc] notation "⊥" => Bot.bot
+
+/-- `⇨` という記号のための型クラス -/
+class HImp (α : Type) where
+  /-- Heyting 含意 `⇨` -/
+  himp : α → α → α
+
+@[inherit_doc] infixr:60 " ⇨ " => HImp.himp
+
+/-- `ᶜ` という記号のためのクラス -/
+class HasCompl (α : Type) where
+  /-- 補元 -/
+  compl : α → α
+
+@[inherit_doc] postfix:1024 "ᶜ" => HasCompl.compl
+
+/-- Heyting 代数 -/
+class HeytingAlgebra (α : Type) extends Lattice α, Top α, Bot α, HasCompl α, HImp α where
+  /-- ⊤ は最大元 -/
+  le_top : ∀ a : α, a ≤ ⊤
+
+  /-- ⊥ は最小元 -/
+  bot_le : ∀ a : α, ⊥ ≤ a
+
+  /-- `· ⊓ b` の右随伴 `b ⇨ ·` が存在する -/
+  le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
+
+  /-- 補元の定義 -/
+  himp_bot (a : α) : a ⇨ ⊥ = aᶜ
+
+end HeytingAlgebra
+
+/- ## 問1 Prop は Heyting 代数
+
+いよいよ問題です。`Prop` が Heyting 代数のインスタンスであることを示しましょう。
+
+しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。
+
+こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。
+
+### aesop ルールの記述方法
+
+`add_aesop_rules` コマンドで `aesop` をカスタマイズすることができます。`add_aesop_rules` は構文的には `add_aesop_rules (phase) [(rule builder) (rule)]` という構成になっています。
+
+* `phase` は `norm` と `safe` と `unsafe` の３通りです。
+  * `norm`: 正規化ルールを表します。
+  * `safe`: 正規化ルールの後に実行されます。`safe` ルールは「適用しても証明可能性が変わらない」ことを前提にしているため、適用後に同じゴールが再検討されることはありません。
+  * `unsafe`: すべての `safe` ルールが失敗した場合に適用されます。直後に成功する確率(%)も指定します。
+
+* `rule builder` には多くの選択肢がありますが、この演習問題では以下のものだけ使用すれば解くことができます。
+  * `tactic`: タクティクを指定します。たとえば `add_aesop_rules safe [tacitc (by simp_all)]` などのように使います。
+  * `cases`: 帰納型 `T` に対して使用することで、仮定に `t : T` がある場合に `cases` を再帰的に適用して分解します。
+  * `simp`: `simp` 補題を登録します。
+
+`aesop` タクティクのカスタマイズ方法については、最も詳しい資料は [leanprover-community/aesop](https://github.com/leanprover-community/aesop) の README です。必要に応じて参考にしてください。
+
+### 問1.1 半順序集合であること
+-/
+section PropInstance --#
+
+/-- `P Q : Prop` に対して、順序関係 `P ≤ Q` を
+`P → Q` が成り立つこととして定める -/
+instance : LE Prop where
+  le a b := a → b
+
+/-- `P < Q` の定義は `P → Q` かつ同値ではないこと -/
+instance : LT Prop where
+  lt a b := (a → b) ∧ ¬ (b → a)
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+-- 例:
+-- `local add_aesop_rules unsafe 50% [tactic (by apply True.intro)]`
+local add_aesop_rules norm [tactic (by dsimp only [LE.le, LT.lt])] --##
+
+/-- 上記の定義のもとで `Prop` は半順序集合 -/
+instance : PartialOrder Prop where
+  le_refl := by aesop
+  le_trans := by aesop
+  lt_iff_le_not_le := by aesop
+  le_antisymm := by aesop
+
+/- ### 問1.2 束であること -/
+
+/-- 論理和 `∨` を上限とする -/
+instance : Sup Prop where
+  sup a b := a ∨ b
+
+/-- 論理積 `∧` を下限とする -/
+instance : Inf Prop where
+  inf a b := a ∧ b
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+-- 例:
+-- `local add_aesop_rules safe [tactic (by simp only [Nat.add_zero])]`
+local add_aesop_rules norm [tactic (by dsimp only [Sup.sup, Inf.inf] at *)] --##
+
+/-- 上記の定義のもとで `Prop` は束 -/
+instance : Lattice Prop where
+  le_sup_left := by aesop
+  le_sup_right := by aesop
+  sup_le := by aesop
+  inf_le_left := by aesop
+  inf_le_right := by aesop
+  le_inf := by aesop
+
+/- ### 問1.3 Heyting 代数であること -/
+
+/-- `a ⇨ b` には `a → b` を対応させる -/
+instance : HImp Prop where
+  himp a b := a → b
+
+/-- `aᶜ` には `¬ a` を対応させる -/
+instance : HasCompl Prop where
+  compl a := ¬ a
+
+/-- True が最大元 -/
+instance : Top Prop where
+  top := True
+
+/-- False が最小元 -/
+instance : Bot Prop where
+  bot := False
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+-- 例:
+-- `local add_aesop_rules norm [simp Nat.add_zero]`
+local add_aesop_rules norm [tactic (by dsimp only [HImp.himp, HasCompl.compl, Top.top, Bot.bot] at *)] --##
+
+instance : HeytingAlgebra Prop where
+  le_top := by aesop
+  bot_le := by aesop
+  le_himp_iff := by aesop
+  himp_bot := by aesop
+
+end PropInstance --#
+/- ## 問2 Bool 代数でない Heyting 代数
+Bool 代数を定義し、Heyting 代数であって Bool 代数でない例を具体的に構成します。これにより、Heyting 代数の公理から Bool 代数の公理を証明することができないことが分かります。
+
+反例の集合はシンプルで、３つの要素からなる集合として構成することができます。
+-/
+section BooleanCounterExample --#
+
+/-- Bool 代数 -/
+class BooleanAlgebra (α : Type) extends HeytingAlgebra α where
+  /-- `x ⊓ xᶜ = ⊥` が成り立つ -/
+  inf_compl_le_bot : ∀ x : α, x ⊓ xᶜ ≤ ⊥
+
+  /-- `⊤ = x ⊔ xᶜ` が成り立つ -/
+  top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ
+
+open PartialOrder Lattice HeytingAlgebra
+
+/-- `{0, 1, 2}` という集合。これが反例になる。 -/
+abbrev Three := Fin 3
+
+-- 順序関係が既に定義されている
+#synth LE Three
+
+/- ### 問2.1 半順序集合であること -/
+
+-- この二つの定理は使用して良い
+theorem min_def (a b : Nat) : min a b = if a ≤ b then a else b := by aesop
+theorem max_def (a b : Nat) : max a b = if a ≤ b then b else a := by aesop
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+--##--
+local add_aesop_rules norm [simp [min_def, max_def]]
+local add_aesop_rules safe [cases Fin]
+local add_aesop_rules norm [simp Fin.le_def]
+local add_aesop_rules safe [tactic (by omega)]
+--##--
+
+instance : PartialOrder Three where
+  le_refl := by aesop
+  le_trans := by aesop
+  le_antisymm := by aesop
+  lt_iff_le_not_le := by aesop
+
+/- ### 問2.2 束であること -/
+
+/-- 上限の定義 -/
+instance : Sup Three where
+  sup a b := {
+    val := max a.val b.val
+    isLt := by omega
+  }
+
+/-- 下限の定義 -/
+instance : Inf Three where
+  inf a b := {
+    val := min a.val b.val
+    isLt := by omega
+  }
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+local add_aesop_rules norm [tactic (by dsimp [Sup.sup, Inf.inf])] --##
+
+/-- 束になる -/
+instance : Lattice Three where
+  le_sup_left := by aesop
+  le_sup_right := by aesop
+  sup_le := by aesop
+  inf_le_left := by aesop
+  inf_le_right := by aesop
+  le_inf := by aesop
+
+/- ### 問2.3 Heyting 代数であるが Bool 代数ではないこと -/
+
+/-- 最大元は2 -/
+instance : Top Three where
+  top := 2
+
+/-- 最小元は0 -/
+instance : Bot Three where
+  bot := 0
+
+/-- Heyting 含意の定義 -/
+instance : HImp Three where
+  himp a b := {
+    val := if a ≤ b then 2 else b.val
+    isLt := by aesop
+  }
+
+/-- 補元の定義 -/
+instance : HasCompl Three where
+  compl a := {
+    val := if a = 0 then 2 else 0
+    isLt := by aesop
+  }
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+local add_aesop_rules norm [tactic (by dsimp [Bot.bot, Top.top, HImp.himp, HasCompl.compl])] --##
+
+/-- Heyting 代数になる -/
+instance : HeytingAlgebra Three where
+  le_top := by aesop
+  bot_le := by aesop
+  le_himp_iff := by aesop
+  himp_bot := by aesop
+
+/-- Three は上記の構成の下で Bool 代数ではない -/
+theorem three_not_boolean : (1 : Three) ⊔ 1ᶜ ≠ ⊤ := by aesop
+
+end BooleanCounterExample --#
diff --git a/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean
new file mode 100644
index 00000000..3876dd07
--- /dev/null
+++ b/Exercise/HeytingAndBooleanAlgebra.lean
@@ -0,0 +1,339 @@
+/- # Heyting 代数と Bool 代数
+直観主義論理において、排中律 `P ∨ ¬ P` は独立な命題であることが知られています。つまり、証明も反証(否定を証明すること)もできません。今回の演習問題では、それに関連した話題として、Bool 代数ではない Heyting 代数が存在することを示します。
+
+ここでは Mathlib をなぞるように理論を構成していきます。
+
+## 半順序集合
+まず準備として、半順序集合を定義します。半順序集合には順序が定義されていますが、要素を2つ与えられたときにどちらが大きいのか比較できるとは限らないことに注意してください。
+-/
+import Aesop --#
+set_option autoImplicit false --#
+set_option relaxedAutoImplicit false --#
+
+/-- 半順序集合 -/
+class PartialOrder (α : Type) extends LE α, LT α where
+  /-- `≤` は反射的である -/
+  le_refl : ∀ a : α, a ≤ a
+
+  /-- `≤` は推移的である -/
+  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+
+  /-- `<` のデフォルト実装 -/
+  lt := fun a b => a ≤ b ∧ ¬ b ≤ a
+
+  /-- `<` と `≤` の関係 -/
+  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a
+
+  /-- `≤` は半対称的 -/
+  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
+
+/- ## 束
+半順序集合であって、任意の2つの要素 `a, b` に対して上限 `a ⊔ b` と下限 `a ⊓ b` が存在するものを束といいます。上限は最小の上界を意味し、下限は最大の下界を意味します。
+
+上限の記号 `⊔` は論理和 `∨` に、下限の記号 `⊓` は論理積 `∧` に、それぞれ似ています。またそれぞれ集合の合併 `∪` と共通部分 `∩` にも似ています。これは、`Prop` と `Set α` がともに束になっていることと整合性があります。
+-/
+
+section Lattice
+
+/-- `⊔` という記号のための型クラス -/
+class Sup (α : Type) where
+  /-- 最小上界、上限 -/
+  sup : α → α → α
+
+/-- `⊓` という記号のための型クラス -/
+class Inf (α : Type) where
+  /-- 最大下界、下限 -/
+  inf : α → α → α
+
+@[inherit_doc] infixl:68 " ⊔ " => Sup.sup
+
+@[inherit_doc] infixl:69 " ⊓ " => Inf.inf
+
+/-- 任意の2つの要素 `a, b` に対して上限 `a ⊔ b` が存在するような半順序集合 -/
+class SemilatticeSup (α : Type) extends Sup α, PartialOrder α where
+  /-- `a ⊔ b` は `a` と `b` の上界になっている -/
+  le_sup_left : ∀ a b : α, a ≤ a ⊔ b
+
+  /-- `a ⊔ b` は `a` と `b` の上界になっている -/
+  le_sup_right : ∀ a b : α, b ≤ a ⊔ b
+
+  /-- `a ⊔ b` は `a`, `b` の上界の中で最小のもの -/
+  sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c
+
+/--  任意の2つの要素 `a, b` に対して下限 `a ⊓ b` が存在するような半順序集合 -/
+class Semilatticeinf (α : Type) extends Inf α, PartialOrder α where
+  /-- `a ⊓ b` は `a` と `b` の下界になっている -/
+  inf_le_left : ∀ a b : α, a ⊓ b ≤ a
+
+  /-- `a ⊓ b` は `a` と `b` の下界になっている -/
+  inf_le_right : ∀ a b : α, a ⊓ b ≤ b
+
+  /-- `a ⊓ b` は `a`, `b` の下界の中で最大のもの -/
+  le_inf : ∀ a b c : α, c ≤ a → c ≤ b → c ≤ a ⊓ b
+
+/-- 束 -/
+class Lattice (α : Type) extends SemilatticeSup α, Semilatticeinf α
+
+end Lattice
+
+/- ## Heyting 代数
+ここまでの準備の下、Heyting 代数を定義することができます。Heyting 代数とは束であって、以下の条件を満たすものです。
+
+1. 最大の要素 `⊤` が存在する。
+2. 最小の要素 `⊥` が存在する。
+3. 下限 `· ⊓ b` の右随伴 `b ⇨ ·` が存在する。つまり任意の `a, b, c` に対して `a ⊓ b ≤ c` と `a ≤ b ⇨ c` が同値。
+-/
+
+section HeytingAlgebra
+
+/-- `⊤` という記号のための型クラス -/
+class Top (α : Type) where
+  /-- 最大元 -/
+  top : α
+
+@[inherit_doc] notation "⊤" => Top.top
+
+/-- `⊥` という記号のための型クラス -/
+class Bot (α : Type) where
+  /-- 最小元 -/
+  bot : α
+
+@[inherit_doc] notation "⊥" => Bot.bot
+
+/-- `⇨` という記号のための型クラス -/
+class HImp (α : Type) where
+  /-- Heyting 含意 `⇨` -/
+  himp : α → α → α
+
+@[inherit_doc] infixr:60 " ⇨ " => HImp.himp
+
+/-- `ᶜ` という記号のためのクラス -/
+class HasCompl (α : Type) where
+  /-- 補元 -/
+  compl : α → α
+
+@[inherit_doc] postfix:1024 "ᶜ" => HasCompl.compl
+
+/-- Heyting 代数 -/
+class HeytingAlgebra (α : Type) extends Lattice α, Top α, Bot α, HasCompl α, HImp α where
+  /-- ⊤ は最大元 -/
+  le_top : ∀ a : α, a ≤ ⊤
+
+  /-- ⊥ は最小元 -/
+  bot_le : ∀ a : α, ⊥ ≤ a
+
+  /-- `· ⊓ b` の右随伴 `b ⇨ ·` が存在する -/
+  le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c
+
+  /-- 補元の定義 -/
+  himp_bot (a : α) : a ⇨ ⊥ = aᶜ
+
+end HeytingAlgebra
+
+/- ## 問1 Prop は Heyting 代数
+
+いよいよ問題です。`Prop` が Heyting 代数のインスタンスであることを示しましょう。
+
+しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。
+
+こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。
+
+### aesop ルールの記述方法
+
+`add_aesop_rules` コマンドで `aesop` をカスタマイズすることができます。`add_aesop_rules` は構文的には `add_aesop_rules (phase) [(rule builder) (rule)]` という構成になっています。
+
+* `phase` は `norm` と `safe` と `unsafe` の３通りです。
+  * `norm`: 正規化ルールを表します。
+  * `safe`: 正規化ルールの後に実行されます。`safe` ルールは「適用しても証明可能性が変わらない」ことを前提にしているため、適用後に同じゴールが再検討されることはありません。
+  * `unsafe`: すべての `safe` ルールが失敗した場合に適用されます。直後に成功する確率(%)も指定します。
+
+* `rule builder` には多くの選択肢がありますが、この演習問題では以下のものだけ使用すれば解くことができます。
+  * `tactic`: タクティクを指定します。たとえば `add_aesop_rules safe [tacitc (by simp_all)]` などのように使います。
+  * `cases`: 帰納型 `T` に対して使用することで、仮定に `t : T` がある場合に `cases` を再帰的に適用して分解します。
+  * `simp`: `simp` 補題を登録します。
+
+`aesop` タクティクのカスタマイズ方法については、最も詳しい資料は [leanprover-community/aesop](https://github.com/leanprover-community/aesop) の README です。必要に応じて参考にしてください。
+
+### 問1.1 半順序集合であること
+-/
+section PropInstance --#
+
+/-- `P Q : Prop` に対して、順序関係 `P ≤ Q` を
+`P → Q` が成り立つこととして定める -/
+instance : LE Prop where
+  le a b := a → b
+
+/-- `P < Q` の定義は `P → Q` かつ同値ではないこと -/
+instance : LT Prop where
+  lt a b := (a → b) ∧ ¬ (b → a)
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+-- 例:
+-- `local add_aesop_rules unsafe 50% [tactic (by apply True.intro)]`
+
+/-- 上記の定義のもとで `Prop` は半順序集合 -/
+instance : PartialOrder Prop where
+  le_refl := by aesop
+  le_trans := by aesop
+  lt_iff_le_not_le := by aesop
+  le_antisymm := by aesop
+
+/- ### 問1.2 束であること -/
+
+/-- 論理和 `∨` を上限とする -/
+instance : Sup Prop where
+  sup a b := a ∨ b
+
+/-- 論理積 `∧` を下限とする -/
+instance : Inf Prop where
+  inf a b := a ∧ b
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+-- 例:
+-- `local add_aesop_rules safe [tactic (by simp only [Nat.add_zero])]`
+
+/-- 上記の定義のもとで `Prop` は束 -/
+instance : Lattice Prop where
+  le_sup_left := by aesop
+  le_sup_right := by aesop
+  sup_le := by aesop
+  inf_le_left := by aesop
+  inf_le_right := by aesop
+  le_inf := by aesop
+
+/- ### 問1.3 Heyting 代数であること -/
+
+/-- `a ⇨ b` には `a → b` を対応させる -/
+instance : HImp Prop where
+  himp a b := a → b
+
+/-- `aᶜ` には `¬ a` を対応させる -/
+instance : HasCompl Prop where
+  compl a := ¬ a
+
+/-- True が最大元 -/
+instance : Top Prop where
+  top := True
+
+/-- False が最小元 -/
+instance : Bot Prop where
+  bot := False
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+-- 例:
+-- `local add_aesop_rules norm [simp Nat.add_zero]`
+
+instance : HeytingAlgebra Prop where
+  le_top := by aesop
+  bot_le := by aesop
+  le_himp_iff := by aesop
+  himp_bot := by aesop
+
+end PropInstance --#
+/- ## 問2 Bool 代数でない Heyting 代数
+Bool 代数を定義し、Heyting 代数であって Bool 代数でない例を具体的に構成します。これにより、Heyting 代数の公理から Bool 代数の公理を証明することができないことが分かります。
+
+反例の集合はシンプルで、３つの要素からなる集合として構成することができます。
+-/
+section BooleanCounterExample --#
+
+/-- Bool 代数 -/
+class BooleanAlgebra (α : Type) extends HeytingAlgebra α where
+  /-- `x ⊓ xᶜ = ⊥` が成り立つ -/
+  inf_compl_le_bot : ∀ x : α, x ⊓ xᶜ ≤ ⊥
+
+  /-- `⊤ = x ⊔ xᶜ` が成り立つ -/
+  top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ
+
+open PartialOrder Lattice HeytingAlgebra
+
+/-- `{0, 1, 2}` という集合。これが反例になる。 -/
+abbrev Three := Fin 3
+
+-- 順序関係が既に定義されている
+#synth LE Three
+
+/- ### 問2.1 半順序集合であること -/
+
+-- この二つの定理は使用して良い
+theorem min_def (a b : Nat) : min a b = if a ≤ b then a else b := by aesop
+theorem max_def (a b : Nat) : max a b = if a ≤ b then b else a := by aesop
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+
+instance : PartialOrder Three where
+  le_refl := by aesop
+  le_trans := by aesop
+  le_antisymm := by aesop
+  lt_iff_le_not_le := by aesop
+
+/- ### 問2.2 束であること -/
+
+/-- 上限の定義 -/
+instance : Sup Three where
+  sup a b := {
+    val := max a.val b.val
+    isLt := by omega
+  }
+
+/-- 下限の定義 -/
+instance : Inf Three where
+  inf a b := {
+    val := min a.val b.val
+    isLt := by omega
+  }
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+
+/-- 束になる -/
+instance : Lattice Three where
+  le_sup_left := by aesop
+  le_sup_right := by aesop
+  sup_le := by aesop
+  inf_le_left := by aesop
+  inf_le_right := by aesop
+  le_inf := by aesop
+
+/- ### 問2.3 Heyting 代数であるが Bool 代数ではないこと -/
+
+/-- 最大元は2 -/
+instance : Top Three where
+  top := 2
+
+/-- 最小元は0 -/
+instance : Bot Three where
+  bot := 0
+
+/-- Heyting 含意の定義 -/
+instance : HImp Three where
+  himp a b := {
+    val := if a ≤ b then 2 else b.val
+    isLt := by aesop
+  }
+
+/-- 補元の定義 -/
+instance : HasCompl Three where
+  compl a := {
+    val := if a = 0 then 2 else 0
+    isLt := by aesop
+  }
+
+-- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
+-- いくつルールを追加しても構いません。
+
+/-- Heyting 代数になる -/
+instance : HeytingAlgebra Three where
+  le_top := by aesop
+  bot_le := by aesop
+  le_himp_iff := by aesop
+  himp_bot := by aesop
+
+/-- Three は上記の構成の下で Bool 代数ではない -/
+theorem three_not_boolean : (1 : Three) ⊔ 1ᶜ ≠ ⊤ := by aesop
+
+end BooleanCounterExample --#
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 59927285..77f73925 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -168,3 +168,4 @@
   - [騎士と悪党のパズル](./Exercise/KnightAndKnave.md)
   - [Cantorの定理](./Exercise/CantorTheorem.md)
   - [Cantorの対関数の全単射性](./Exercise/CantorPairing.md)
+  - [Heying代数とBool代数](./Exercise/HeytingAndBooleanAlgebra.md)

From fde636a0b91d589e93221e3c6efcd15bac741d48 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 9 Sep 2024 22:09:58 +0900
Subject: [PATCH 2/2] =?UTF-8?q?=E6=97=A7=E3=83=90=E3=83=BC=E3=82=B8?=
 =?UTF-8?q?=E3=83=A7=E3=83=B3=E3=81=AE=E6=8E=92=E4=B8=AD=E5=BE=8B=E3=81=AE?=
 =?UTF-8?q?=E5=95=8F=E9=A1=8C=E3=81=AF=E5=89=8A=E9=99=A4=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Solution/DeMorganAndEm.lean | 249 ---------------------------
 Exercise/DeMorganAndEm.lean          |  71 --------
 src/SUMMARY.md                       |   1 -
 3 files changed, 321 deletions(-)
 delete mode 100644 Examples/Solution/DeMorganAndEm.lean
 delete mode 100644 Exercise/DeMorganAndEm.lean

diff --git a/Examples/Solution/DeMorganAndEm.lean b/Examples/Solution/DeMorganAndEm.lean
deleted file mode 100644
index 897a5788..00000000
--- a/Examples/Solution/DeMorganAndEm.lean
+++ /dev/null
@@ -1,249 +0,0 @@
-/- # De Morgan の法則と排中律
-
-論理和 `∨` と論理積 `∧` の間に次の関係が成立することが知られています。
-
-1. `¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q`
-1. `¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q`
-
-これは De Morgan の法則と呼ばれているものの一部です。
-
-## 問1
-
-最初の、論理和の中に否定を入れる方を Lean で証明していきましょう。以下の `sorry` の部分を埋めてください。
-
-`simp` や `rw` でライブラリの命題を引用する方法でも示すことができますし、使わずに自力で示すこともできます。どちらでも構いませんが、Lean に慣れていない人は自力で示すのに挑戦してみてください。
--/
-set_option autoImplicit false --#
-
-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/Exercise/DeMorganAndEm.lean b/Exercise/DeMorganAndEm.lean
deleted file mode 100644
index 9629112a..00000000
--- a/Exercise/DeMorganAndEm.lean
+++ /dev/null
@@ -1,71 +0,0 @@
-/- # De Morgan の法則と排中律
-
-論理和 `∨` と論理積 `∧` の間に次の関係が成立することが知られています。
-
-1. `¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q`
-1. `¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q`
-
-これは De Morgan の法則と呼ばれているものの一部です。
-
-## 問1
-
-最初の、論理和の中に否定を入れる方を Lean で証明していきましょう。以下の `sorry` の部分を埋めてください。
-
-`simp` や `rw` でライブラリの命題を引用する方法でも示すことができますし、使わずに自力で示すこともできます。どちらでも構いませんが、Lean に慣れていない人は自力で示すのに挑戦してみてください。
--/
-set_option autoImplicit false --#
-
-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/src/SUMMARY.md b/src/SUMMARY.md
index 77f73925..921f819c 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -163,7 +163,6 @@
 
 - [演習問題](./Exercise/README.md)
   - [床屋のパラドクス](./Exercise/BarberParadox.md)
-  - [De Morganの法則と排中律](./Exercise/DeMorganAndEm.md)
   - [「ならば」の定義を疑う](./Exercise/DoubtImplication.md)
   - [騎士と悪党のパズル](./Exercise/KnightAndKnave.md)
   - [Cantorの定理](./Exercise/CantorTheorem.md)