Skip to content

Cantor の対関数の演習問題に対して、証明の出典を示す #801

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 4 commits into from
Closed

Cantor の対関数の演習問題に対して、証明の出典を示す #801

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6f3bdac
Heyting代数の問題の問題文の微修正
Seasawher Sep 15, 2024
47c23bd
Heyting 代数の問題での記述と、`add_aesop_rules` での記述で整合性を取る
Seasawher Sep 15, 2024
7050aa6
generated by GitHub Action
actions-user Sep 15, 2024
a688105
Cantor の対関数についての証明は出典を示す
Seasawher Sep 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion Examples/Solution/CantorPairing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。

無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。
無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note]

## 問1: sum 関数

Expand Down Expand Up @@ -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) を参考にいたしました。 -/
30 changes: 14 additions & 16 deletions Examples/Solution/HeytingAndBooleanAlgebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,9 +153,9 @@ 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
Expand All @@ -176,9 +176,9 @@ 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
Expand Down Expand Up @@ -209,9 +209,9 @@ 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
Expand All @@ -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

Expand All @@ -248,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
Expand All @@ -277,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
Expand Down Expand Up @@ -314,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
Expand Down
4 changes: 3 additions & 1 deletion Exercise/CantorPairing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。

無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。
無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note]

## 問1: sum 関数

Expand Down Expand Up @@ -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) を参考にいたしました。 -/
14 changes: 6 additions & 8 deletions Exercise/HeytingAndBooleanAlgebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down