Skip to content
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

Heyting 代数の問題文を微修正 #797

Merged
merged 4 commits into from
Sep 16, 2024
Merged

Heyting 代数の問題文を微修正 #797

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
f9a618c
Merge branch 'main' into heyting
Seasawher Sep 16, 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
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
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