From 6f3bdacd068e0aced17a4a7817a12670bd41ae52 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 16 Sep 2024 00:01:40 +0900 Subject: [PATCH 1/4] =?UTF-8?q?Heyting=E4=BB=A3=E6=95=B0=E3=81=AE=E5=95=8F?= =?UTF-8?q?=E9=A1=8C=E3=81=AE=E5=95=8F=E9=A1=8C=E6=96=87=E3=81=AE=E5=BE=AE?= =?UTF-8?q?=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Solution/HeytingAndBooleanAlgebra.lean | 14 ++++++-------- Exercise/HeytingAndBooleanAlgebra.lean | 14 ++++++-------- 2 files changed, 12 insertions(+), 16 deletions(-) diff --git a/Examples/Solution/HeytingAndBooleanAlgebra.lean b/Examples/Solution/HeytingAndBooleanAlgebra.lean index 663bd5d6..4c41e1c3 100644 --- a/Examples/Solution/HeytingAndBooleanAlgebra.lean +++ b/Examples/Solution/HeytingAndBooleanAlgebra.lean @@ -153,8 +153,8 @@ instance : LT Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --- 例: --- `local add_aesop_rules unsafe 50% [tactic (by apply True.intro)]` +-- 以下に示すのは一例です: +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` は半順序集合 -/ @@ -176,8 +176,8 @@ instance : Inf Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --- 例: --- `local add_aesop_rules safe [tactic (by simp only [Nat.add_zero])]` +-- 以下に示すのは一例です: +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` は束 -/ @@ -209,8 +209,8 @@ instance : Bot Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --- 例: --- `local add_aesop_rules norm [simp Nat.add_zero]` +-- 以下に示すのは一例です: +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 @@ -235,8 +235,6 @@ class BooleanAlgebra (α : Type) extends HeytingAlgebra α where /-- `⊤ = x ⊔ xᶜ` が成り立つ -/ top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ -open PartialOrder Lattice HeytingAlgebra - /-- `{0, 1, 2}` という集合。これが反例になる。 -/ abbrev Three := Fin 3 diff --git a/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean index 948cebd3..6d52558d 100644 --- a/Exercise/HeytingAndBooleanAlgebra.lean +++ b/Exercise/HeytingAndBooleanAlgebra.lean @@ -153,8 +153,8 @@ instance : LT Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --- 例: --- `local add_aesop_rules unsafe 50% [tactic (by apply True.intro)]` +-- 以下に示すのは一例です: +local add_aesop_rules unsafe 50% [tactic (by apply True.intro)] /-- 上記の定義のもとで `Prop` は半順序集合 -/ instance : PartialOrder Prop where @@ -175,8 +175,8 @@ instance : Inf Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --- 例: --- `local add_aesop_rules safe [tactic (by simp only [Nat.add_zero])]` +-- 以下に示すのは一例です: +local add_aesop_rules safe [tactic (by simp only [Nat.add_zero])] /-- 上記の定義のもとで `Prop` は束 -/ instance : Lattice Prop where @@ -207,8 +207,8 @@ instance : Bot Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --- 例: --- `local add_aesop_rules norm [simp Nat.add_zero]` +-- 以下に示すのは一例です: +local add_aesop_rules norm [simp Nat.add_zero] instance : HeytingAlgebra Prop where le_top := by aesop @@ -232,8 +232,6 @@ class BooleanAlgebra (α : Type) extends HeytingAlgebra α where /-- `⊤ = x ⊔ xᶜ` が成り立つ -/ top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ -open PartialOrder Lattice HeytingAlgebra - /-- `{0, 1, 2}` という集合。これが反例になる。 -/ abbrev Three := Fin 3 From 47c23bd4976e360333b17ea1e53a6b840786c11a Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 16 Sep 2024 00:04:28 +0900 Subject: [PATCH 2/4] =?UTF-8?q?Heyting=20=E4=BB=A3=E6=95=B0=E3=81=AE?= =?UTF-8?q?=E5=95=8F=E9=A1=8C=E3=81=A7=E3=81=AE=E8=A8=98=E8=BF=B0=E3=81=A8?= =?UTF-8?q?=E3=80=81`add=5Faesop=5Frules`=20=E3=81=A7=E3=81=AE=E8=A8=98?= =?UTF-8?q?=E8=BF=B0=E3=81=A7=E6=95=B4=E5=90=88=E6=80=A7=E3=82=92=E5=8F=96?= =?UTF-8?q?=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Solution/HeytingAndBooleanAlgebra.lean | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Examples/Solution/HeytingAndBooleanAlgebra.lean b/Examples/Solution/HeytingAndBooleanAlgebra.lean index 4c41e1c3..e0c01123 100644 --- a/Examples/Solution/HeytingAndBooleanAlgebra.lean +++ b/Examples/Solution/HeytingAndBooleanAlgebra.lean @@ -154,8 +154,8 @@ instance : LT Prop where -- ここに `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])] --## +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 @@ -177,8 +177,8 @@ instance : Inf Prop where -- ここに `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 *)] --## +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 @@ -210,8 +210,8 @@ instance : Bot Prop where -- ここに `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 *)] --## +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 @@ -246,9 +246,9 @@ abbrev Three := Fin 3 -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 --##-- -local add_aesop_rules safe [cases Fin] -local add_aesop_rules norm [simp Fin.le_def] -local add_aesop_rules safe [tactic (by omega)] +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 @@ -275,7 +275,7 @@ instance : Inf Three where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 -local add_aesop_rules norm [tactic (by dsimp [Sup.sup, Inf.inf])] --## +local add_aesop_rules norm tactic [(by dsimp [Sup.sup, Inf.inf])] --## /-- 束になる -/ instance : Lattice Three where @@ -312,7 +312,7 @@ instance : HasCompl Three where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 -local add_aesop_rules norm [tactic (by dsimp [Bot.bot, Top.top, HImp.himp, HasCompl.compl])] --## +local add_aesop_rules norm tactic [(by dsimp [Bot.bot, Top.top, HImp.himp, HasCompl.compl])] --## /-- Heyting 代数になる -/ instance : HeytingAlgebra Three where From 7050aa6ebeef306348d0a6c0fb426f5fec0e2822 Mon Sep 17 00:00:00 2001 From: GitHub Action Date: Sun, 15 Sep 2024 15:05:47 +0000 Subject: [PATCH 3/4] generated by GitHub Action --- Exercise/HeytingAndBooleanAlgebra.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean index 6d52558d..5fcd93cc 100644 --- a/Exercise/HeytingAndBooleanAlgebra.lean +++ b/Exercise/HeytingAndBooleanAlgebra.lean @@ -154,7 +154,7 @@ instance : LT Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 -- 以下に示すのは一例です: -local add_aesop_rules unsafe 50% [tactic (by apply True.intro)] +local add_aesop_rules unsafe 50% tactic [(by apply True.intro)] /-- 上記の定義のもとで `Prop` は半順序集合 -/ instance : PartialOrder Prop where @@ -176,7 +176,7 @@ instance : Inf Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 -- 以下に示すのは一例です: -local add_aesop_rules safe [tactic (by simp only [Nat.add_zero])] +local add_aesop_rules safe tactic [(by simp only [Nat.add_zero])] /-- 上記の定義のもとで `Prop` は束 -/ instance : Lattice Prop where @@ -208,7 +208,7 @@ instance : Bot Prop where -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。 -- いくつルールを追加しても構いません。 -- 以下に示すのは一例です: -local add_aesop_rules norm [simp Nat.add_zero] +local add_aesop_rules norm simp [Nat.add_zero] instance : HeytingAlgebra Prop where le_top := by aesop From a688105652deb00b984595b83e1b50881d68788f Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 16 Sep 2024 03:24:45 +0900 Subject: [PATCH 4/4] =?UTF-8?q?Cantor=20=E3=81=AE=E5=AF=BE=E9=96=A2?= =?UTF-8?q?=E6=95=B0=E3=81=AB=E3=81=A4=E3=81=84=E3=81=A6=E3=81=AE=E8=A8=BC?= =?UTF-8?q?=E6=98=8E=E3=81=AF=E5=87=BA=E5=85=B8=E3=82=92=E7=A4=BA=E3=81=99?= =?UTF-8?q?=20Fixes=20#800?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Solution/CantorPairing.lean | 4 +++- Exercise/CantorPairing.lean | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Examples/Solution/CantorPairing.lean b/Examples/Solution/CantorPairing.lean index 046c56f0..94109332 100644 --- a/Examples/Solution/CantorPairing.lean +++ b/Examples/Solution/CantorPairing.lean @@ -8,7 +8,7 @@ だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。 -無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。 +無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note] ## 問1: sum 関数 @@ -188,3 +188,5 @@ theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by specialize ih m' (n + 1) this simp [unpair, ih] -- sorry + +/- [^note]: 本項での証明を書くにあたって [Cantor の対関数の全単射性の証明](http://iso.2022.jp/math/pairing_function.pdf) を参考にいたしました。 -/ diff --git a/Exercise/CantorPairing.lean b/Exercise/CantorPairing.lean index 5a4794f7..9da84c22 100644 --- a/Exercise/CantorPairing.lean +++ b/Exercise/CantorPairing.lean @@ -8,7 +8,7 @@ だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。 -無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。 +無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note] ## 問1: sum 関数 @@ -152,3 +152,5 @@ theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by -- 後は帰納法の仮定から従う。 sorry + +/- [^note]: 本項での証明を書くにあたって [Cantor の対関数の全単射性の証明](http://iso.2022.jp/math/pairing_function.pdf) を参考にいたしました。 -/