From 6f3bdacd068e0aced17a4a7817a12670bd41ae52 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 16 Sep 2024 00:01:40 +0900 Subject: [PATCH 1/3] =?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/3] =?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/3] 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