From 661c32271dbbbbc247727a02344b5efdfed6a1e1 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 21 Oct 2024 21:29:24 +0900
Subject: [PATCH 1/2] =?UTF-8?q?`cases`=20=E3=81=AE=E3=83=9A=E3=83=BC?=
 =?UTF-8?q?=E3=82=B8=E3=81=A7=E3=81=AE=20Or=20=E3=81=AE=E7=B4=B9=E4=BB=8B?=
 =?UTF-8?q?=E3=81=AE=E4=BB=95=E6=96=B9=E3=82=92=E5=A4=89=E3=81=88=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Tactic/Cases.lean | 34 +++++++++++++----------
 1 file changed, 19 insertions(+), 15 deletions(-)

diff --git a/LeanByExample/Reference/Tactic/Cases.lean b/LeanByExample/Reference/Tactic/Cases.lean
index bbff3f1e..592f4da1 100644
--- a/LeanByExample/Reference/Tactic/Cases.lean
+++ b/LeanByExample/Reference/Tactic/Cases.lean
@@ -44,22 +44,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
 /- ## 舞台裏
 
 `cases` は、実際には論理和に限らず[帰納型](../Declarative/Inductive.md)をコンストラクタに分解することができるタクティクです。
-論理和を分解することができるのも、`Or` が帰納型として定義されているからです。
 -/
-namespace Cases --#
-
-/--
-info: inductive Or : Prop → Prop → Prop
-number of parameters: 2
-constructors:
-Or.inl : ∀ {a b : Prop}, a → a ∨ b
-Or.inr : ∀ {a b : Prop}, b → a ∨ b
--/
-#guard_msgs in #print Or
-
--- Or のコンストラクタ
-#check (Or.inl : P → P ∨ Q)
-#check (Or.inr : Q → P ∨ Q)
 
 -- 帰納型として定義した例示のための型
 inductive Sample where
@@ -76,4 +61,23 @@ example (s : Sample) : True := by
   case bar z =>
     trivial
 
+/- 論理和を分解することができるのも、`Or` が次のように帰納型として定義されているからです。 -/
+namespace Cases --#
+
+--#--
+-- Or の定義が変わっていないことを確認するためのコード
+/--
+info: inductive Or : Prop → Prop → Prop
+number of parameters: 2
+constructors:
+Or.inl : ∀ {a b : Prop}, a → a ∨ b
+Or.inr : ∀ {a b : Prop}, b → a ∨ b
+-/
+#guard_msgs in #print Or
+--#--
+
+inductive Or (a b : Prop) : Prop where
+  | inl (h : a) : Or a b
+  | inr (h : b) : Or a b
+
 end Cases --#

From b3e82e86bf784dd56d4c77d053f721666aa4ad34 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 21 Oct 2024 21:40:18 +0900
Subject: [PATCH 2/2] =?UTF-8?q?#print=20=E3=81=A7=E6=97=A2=E5=AD=98?=
 =?UTF-8?q?=E3=82=B3=E3=83=BC=E3=83=89=E3=82=92=E7=A2=BA=E8=AA=8D=E3=81=97?=
 =?UTF-8?q?=E3=81=AA=E3=81=84?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Tactic/Exists.lean     | 18 ++++++++----------
 .../Reference/TypeClass/Decidable.lean         |  9 +++++++++
 2 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/LeanByExample/Reference/Tactic/Exists.lean b/LeanByExample/Reference/Tactic/Exists.lean
index f4c3959d..c731d77f 100644
--- a/LeanByExample/Reference/Tactic/Exists.lean
+++ b/LeanByExample/Reference/Tactic/Exists.lean
@@ -5,16 +5,13 @@
 ゴールが `⊢ ∃ x, P x` のとき、`x: X` がローカルコンテキストにあれば、`exists x` によりゴールが `P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
 import Lean --#
 
-namespace Exists --#
-
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
 /- ## 内部処理についての補足
 なお Lean での存在量化の定義は次のようになっています。-/
-
-universe u
-
+--#--
+-- Exists の定義が変わっていないことを確認する
 /--
 info: inductive Exists.{u} : {α : Sort u} → (α → Prop) → Prop
 number of parameters: 2
@@ -22,11 +19,14 @@ constructors:
 Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
 -/
 #guard_msgs in #print Exists
+--#--
+namespace Exists --#
 
--- `p : α → Prop` は `α` 上の述語とする。
--- このとき `w : α` と `h : p w` が与えられたとき `∃ x : α, p x` が成り立つ。
-#check (Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α) (_h : p w), Exists p)
+inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop where
+  /-- `a : α` と `h : p a` から `∃ x : α, p x` の証明を得る -/
+  | intro (w : α) (h : p w) : Exists p
 
+end Exists --#
 /- したがって `Exists` は単一のコンストラクタを持つ[帰納型](../Declarative/Inductive.md)、つまり[構造体](../Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
@@ -56,5 +56,3 @@ elab "#expand " t:macro_stx : command => do
 /-- info: (refine ⟨1, 2, 3, ?_⟩; try trivial) -/
 #guard_msgs in
   #expand exists 1, 2, 3
-
-end Exists --#
diff --git a/LeanByExample/Reference/TypeClass/Decidable.lean b/LeanByExample/Reference/TypeClass/Decidable.lean
index b1e530ab..98cf82a0 100644
--- a/LeanByExample/Reference/TypeClass/Decidable.lean
+++ b/LeanByExample/Reference/TypeClass/Decidable.lean
@@ -46,6 +46,8 @@ example : Even 4 := by decide
 /- ## class inductive
 `Decidable` 型クラスの定義は少し特殊です。コンストラクタが複数あり、[構造体](../Declarative/Structure.md)ではなく[帰納型](../Declarative/Inductive.md)の構造をしています。これは `Decidable` が [`class inductive`](../Declarative/Class.md#ClassInductive) というコマンドで定義されているためです。-/
 
+--#--
+-- Decidable の定義が変わっていないことを確認する
 /--
 info: inductive Decidable : Prop → Type
 number of parameters: 1
@@ -54,5 +56,12 @@ Decidable.isFalse : {p : Prop} → ¬p → Decidable p
 Decidable.isTrue : {p : Prop} → p → Decidable p
 -/
 #guard_msgs in #print Decidable
+--#--
+
+class inductive Decidable (p : Prop) where
+  /-- `¬ p` であることが分かっているなら、`p` は決定可能 -/
+  | isFalse (h : Not p) : Decidable p
+  /-- `p` であることが分かっているなら、`p` は決定可能 -/
+  | isTrue (h : p) : Decidable p
 
 end Decidable --#