Merge pull request #1398 from lean-ja/Seasawher/issue1258

構造体の定義の曖昧さ問題
lean-ja · Jan 28, 2025 · a5eac03 · a5eac03
2 parents d885b85 + 2a72d75
commit a5eac03
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 9 deletions.
diff --git a/LeanByExample/Declarative/Axiom.lean b/LeanByExample/Declarative/Axiom.lean
@@ -253,7 +253,7 @@ variable {p : α → Prop}
 #check (Classical.choose_spec : (h : ∃ x, p x) → p (Classical.choose h))
 
 /- #### なぜ証明無関係と矛盾しないのか
-[証明無関係](../Type/Prop.md#ProofIrrel)の節で詳しく述べているように、存在命題は「何かがある」としか主張しておらず、具体的な項を復元するのに必要な情報を持っていません。したがって存在が主張されている項を取り出して関数の返り値にすることはできないはずですが、選択原理を使うと存在命題から具体的な項が得られてしまいます。これが矛盾を生まないのはなぜでしょうか？
+[証明無関係](#{root}/Type/Prop.md#ProofIrrel)の節で詳しく述べているように、存在命題は「何かがある」としか主張しておらず、具体的な項を復元するのに必要な情報を持っていません。したがって存在が主張されている項を取り出して関数の返り値にすることはできないはずですが、選択原理を使うと存在命題から具体的な項が得られてしまいます。これが矛盾を生まないのはなぜでしょうか？
 
 答えは、選択原理は証明方法が異なる証明項であっても、同じ命題であれば一様に同じ項を返すからです。以下の例では、「証拠」が異なるような存在命題の証明項を２つ与えていますが、そこから選択される項は同じです。つまり、選択原理は同値な存在命題すべてに対して一斉に同じ項を取り出す方法があると主張しているのであって、「存在が主張されている項を取り出して関数の返り値にする」ことができるとまでは主張していないのです。-/
 

diff --git a/LeanByExample/Declarative/Structure.lean b/LeanByExample/Declarative/Structure.lean
@@ -1,6 +1,6 @@
 /-
 # structure
-`structure` は構造体を定義するためのコマンドです。構造体とは、複数のデータをまとめて一つの型として扱えるようにしたものです。
+`structure` は構造体を定義するためのコマンドです。構造体とは、大雑把に説明すれば複数のデータをまとめて一つの型として扱えるようにしたものです。
 -/
 
 /-- 2次元空間の点 -/
@@ -148,14 +148,19 @@ structure ColorPoint3D (α : Type) extends Point α, RGBValue where
   z : α
 
 /- ## 舞台裏
-構造体は、帰納型の特別な場合であり、おおむねコンストラクタが一つしかないケースに対応します。上記の `Point` は以下のように定義された帰納型 `Point'` と同様の構造を持ちます。-/
+
+構造体は、コンストラクタが一つしかない帰納型であると見なすことができます。
+
+### 帰納型による模倣
+
+`structure` コマンドを使って定義した上記の `Point` を、`inductive` コマンドで模倣してみましょう。まず `mk` という単一のコンストラクタだけを持つ帰納型を定義します。このコンストラクタの各引数がフィールドに相当します。 -/
 
 inductive Point' (α : Type) : Type where
-  | mk : (x : α) → (y : α) → Point' α
+  | mk (x y : α)
 
-/- ただしこの場合、アクセサ関数が自動的に作られないため、フィールド記法は自分で実装しないと使用できないほか、波括弧記法が使えません。 -/
+/- アクセサ関数が自動的に作られませんが、自分で作ることができます。-/
 
--- フィールド記法が利用できない
+-- アクセサ関数が利用できない
 #guard_msgs (drop warning) in --#
 #check_failure Point'.x
 
@@ -164,18 +169,34 @@ def Point'.x {α : Type} (p : Point' α) : α :=
   match p with
   | Point'.mk x _ => x
 
--- フィールド記法が使えるようになった
+-- アクセサ関数が使えるようになった
 #eval
   let p := Point'.mk 1 2
   p.x
 
+/- 無名コンストラクタは最初から使用できます。 -/
+
 -- 無名コンストラクタは使用できる
 def origin' : Point Int := ⟨0, 0⟩
 
+/- 波括弧記法は `structure` コマンドで定義された型でなければ使用できないようです。 -/
+
 -- 波括弧記法は使用できない
 /--
 warning: invalid {...} notation, structure type expected
   Point' Int
 -/
 #guard_msgs in
-  #check_failure ({ x := 1, y := 2 } : Point' Int)
+  #check_failure { x := 1, y := 2 : Point' Int}
+
+/- ### 用途
+この `structure` コマンドの代わりに `inductive` コマンドを用いる方法は、定義しようとしている構造体が命題をパラメータに持っているときに必要になります。[`Prop` の Large Elimination が許可されていない](#{root}/Type/Prop.md#NoLargeElim)ことにより、この場合はアクセサ関数が生成できないので `structure` コマンドが使用できず、エラーになります。 -/
+
+-- `w` はデータなので、アクセサ関数が生成できなくてエラーになる
+/-- error: failed to generate projections for 'Prop' structure, field 'w' is not a proof -/
+#guard_msgs in
+  structure Exists'.{v} {α : Sort v} (p : α → Prop) : Prop where
+    intro ::
+
+    w : α
+    h : p w
diff --git a/LeanByExample/Type/Prop.lean b/LeanByExample/Type/Prop.lean
@@ -122,7 +122,7 @@ theorem my_proof_irrel (P : Prop) (h1 h2 : P) : h1 = h2 := rfl
 /-- info: 'proof_irrel' does not depend on any axioms -/
 #guard_msgs in #print axioms proof_irrel
 
-/- ### No Large Elimination
+/- ### No Large Elimination { #NoLargeElim }
 証明無関係の重要な帰結のひとつに、「証明から値を取り出すことができるのは、証明の中だけ」というものがあります。この現象は、「`Prop` は large elimination を許可しない」という言葉で表現されることがあります。
 
 たとえば次のように、証明の中であれば証明項を [`cases`](../Tactic/Cases.md) や [`rcases`](../Tactic/Rcases.md) で分解して値を取り出すことができます。-/