Merge pull request #1402 from lean-ja/Seasawher/issue1356

無名コンストラクタの説明を「構文」カテゴリに移動させる

Author: Seasawher

LeanByExample/Declarative/Structure.lean

@@ -63,46 +63,8 @@ def Point.isOrigin (p : Point Int) : Bool :=
 -- フィールド記法が使える！
 #guard origin.isOrigin
 
-/- ## 無名コンストラクタ { #AnonymousConstructor }
-**無名コンストラクタ(anonymous constructor)** は、構造体 `T` に対して `T` 型の項を構成する方法のひとつです。これは以下に示すように、`⟨x1, x2, ...⟩` という構文により使うことができます。
--/
-set_option linter.unusedVariables false --#
-
-/-- 2つのフィールドを持つ構造体 -/
-structure Hoge where
-  foo : Nat
-  bar : Nat
-
-def hoge : Hoge := ⟨1, 2⟩
-
-/- コンストラクタが入れ子になっていても平坦化することができます。例えば、以下の2つの定義は同じものを定義します。-/
-
-def foo : Nat × (Int × String) := ⟨1, ⟨2, "foo"⟩⟩
-
-def foo' : Nat × (Int × String) := ⟨1, 2, "foo"⟩
-
-#guard foo = foo'
-
-/- 一般の[帰納型](../Declarative/Inductive.md)に対しては使用できません。-/
-
-inductive Sample where
-  | fst (foo bar : Nat) : Sample
-  | snd (foo bar : String) : Sample
-
--- 「コンストラクタが一つしかない帰納型でなければ使用できない」というエラーになる
-/--
-warning: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor ⏎
-  Sample
--/
-#guard_msgs in
-  #check_failure (⟨"foo", "bar"⟩ : Sample)
-
--- コンストラクタを指定しても使用できない
-#guard_msgs (drop warning) in --#
-#check_failure (Sample.snd ⟨"foo", "bar"⟩ : Sample)
-
 /- ## 項を定義する様々な構文
-構造体の項を定義したい場合、複数の方法があります。波括弧記法が好まれますが、フィールド名が明らかな状況であれば無名コンストラクタを使用することもあります。-/
+構造体の項を定義したい場合、複数の方法があります。波括弧記法が好まれますが、フィールド名が明らかな状況であれば[無名コンストラクタ](#{root}/Parser/AnonymousConstructor.md)を使用することもあります。-/
 
 -- コンストラクタを使う
 def sample0 : Point Int := Point.mk 1 2
@@ -174,11 +136,6 @@ def Point'.x {α : Type} (p : Point' α) : α :=
   let p := Point'.mk 1 2
   p.x
 
-/- 無名コンストラクタは最初から使用できます。 -/
-
--- 無名コンストラクタは使用できる
-def origin' : Point Int := ⟨0, 0⟩
-
 /- 波括弧記法は `structure` コマンドで定義された型でなければ使用できないようです。 -/
 
 -- 波括弧記法は使用できない

LeanByExample/Parser/AnonymousConstructor.lean

@@ -0,0 +1,70 @@
+/- # 無名コンストラクタ
+
+**無名コンストラクタ(anonymous constructor)** を使用すると、単一のコンストラクタしか持たない帰納型 `T` に対して、コンストラクタ名を指定せずに `T` 型の項を構成することができます。`⟨x1, x2, ...⟩` という構文により使うことができます。
+-/
+
+/-- 単一のコンストラクタしか持たない帰納型の例 -/
+inductive Foo where
+  | mk (x y : Nat)
+deriving DecidableEq
+
+#guard
+  -- コンストラクタを使って項を作る場合
+  let foo₁ := Foo.mk 1 2
+
+  -- 無名コンストラクタを使って項を作る場合
+  let foo₂ := ⟨1, 2⟩
+
+  -- 両者は同じものを表す！
+  foo₁ = foo₂
+
+/- 一般の[帰納型](#{root}/Declarative/Inductive.md)に対しては使用できません。-/
+
+/-- 複数のコンストラクタを持つ帰納型の例 -/
+inductive Sample where
+  | fst (foo bar : Nat) : Sample
+  | snd (foo bar : String) : Sample
+
+-- 「コンストラクタが一つしかない帰納型でなければ使用できない」というエラーになる
+/--
+warning: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor ⏎
+  Sample
+-/
+#guard_msgs in
+  #check_failure (⟨"foo", "bar"⟩ : Sample)
+
+/- ## 構造体への使用
+[構造体](#{root}/Declarative/Structure.md)は単一コンストラクタしか持たない帰納型なので、構造体に対しても無名コンストラクタ構文が使用できます。-/
+
+/-- 2つのフィールドを持つ構造体 -/
+structure Hoge where
+  foo : Nat
+  bar : Nat
+
+#check (⟨1, 2⟩ : Hoge)
+
+/- ## 平坦化
+コンストラクタが入れ子になっている場合でも平坦化することができます。-/
+
+#guard
+  -- 入れ子にした場合
+  let x : Nat × (Int × String) := ⟨1, ⟨2, "hello"⟩⟩
+
+  -- 平坦化した場合
+  let y : Nat × (Int × String) := ⟨1, 2, "hello"⟩
+
+  -- 両者は同じものを表している！
+  x = y
+
+/- 上の例は構造体の同種のコンストラクタが入れ子になっている例ですが、構造体でも同種のコンストラクタでもなくても平坦化することができます。 -/
+
+/-- Prod を真似て自作した帰納型 -/
+inductive MyProd (α β : Type) where
+  | mk (fst : α) (snd : β)
+deriving DecidableEq
+
+-- Prod のための中置記法
+@[inherit_doc] infixr:35 " ×ₘ " => MyProd
+
+-- 平坦化ができている！
+#check (⟨1, 2, 1, 2, 1⟩ : Nat × Nat ×ₘ Nat ×ₘ Nat × Nat)

LeanByExample/Tactic/Exact.lean

@@ -17,7 +17,7 @@ example (hP : P) (hQ : Q) : P ∧ Q := by
 
 example (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ
 
-/- なお `And` は[構造体](#{root}/Declarative/Structure.md)なので[無名コンストラクタ](#{root}/Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
+/- なお `And` は[構造体](#{root}/Declarative/Structure.md)なので[無名コンストラクタ](#{root}/Parser/AnonymousConstructor.md)記法を用いて次のように書くこともできます。-/
 
 example (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩
 

LeanByExample/Tactic/Exists.lean

@@ -29,7 +29,7 @@ inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop where
   | intro (w : α) (h : p w) : Exists p
 
 end Exists --#
-/- したがって `Exists` は単一のコンストラクタを持つ[帰納型](#{root}/Declarative/Inductive.md)、つまり[構造体](#{root}/Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](#{root}/Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
+/- したがって `Exists` は単一のコンストラクタを持つ[帰納型](#{root}/Declarative/Inductive.md)、つまり[構造体](#{root}/Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](#{root}/Parser/AnonymousConstructor.md)で次のように書き直すことができます。-/
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exact ⟨2, show 3 * 2 + 1 = 7 from by rfl⟩

LeanByExample/Tactic/Have.lean

@@ -25,7 +25,7 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
 
 `P` の証明 `hp : P` と `Q` の証明 `hq : Q` があるとき、`P ∧ Q` の証明は `And.intro hp hq` で構成できます。ここで `And.intro` は構造体 `And` 型のコンストラクタです。
 
-これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](#{root}/Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の[構造体](#{root}/Declarative/Structure.md)に使用することができます。-/
+これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](#{root}/Parser/AnonymousConstructor.md)と呼ばれるもので、`And` に限らず任意の[構造体](#{root}/Declarative/Structure.md)に使用することができます。-/
 variable (hp : P) (hq : Q)
 
 def hpq : P ∧ Q := ⟨hp, hq⟩

LeanByExample/Tactic/Intro.lean

@@ -27,7 +27,7 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
 /- ## 特定の形の命題に対しての使用法
 
 ### A ∧ B → C
-前提が論理積の形をしていた場合、[無名コンストラクタ](#{root}/Declarative/Structure.md#AnonymousConstructor)で仮定を分解することができます。
+前提が論理積の形をしていた場合、[無名コンストラクタ](#{root}/Parser/AnonymousConstructor.md)で仮定を分解することができます。
 -/
 
 example {S : Prop} (hPR : P → R) (hQR : Q → S) : P ∧ Q → R ∧ S := by

booksrc/SUMMARY.md

@@ -67,6 +67,7 @@
   - [unsafe: Leanのルールを破る](./Modifier/Unsafe.md)
 
 - [構文](./Parser/README.md)
+  - [⟨x₁, x₂, ..⟩: 無名コンストラクタ](./Parser/AnonymousConstructor.md)
   - [`{x y : A}`: 暗黙の引数](./Parser/ImplicitBinder.md)
   - [by: タクティクモードに入る](./Parser/By.md)
   - [show .. from: 項の型を明示](./Parser/Show.md)
@@ -122,7 +123,7 @@
   - [Type: 型の型](./Type/Type.md)
 
 - [タクティク](./Tactic/README.md)
-  - [<;> 生成された全ゴールに適用](./Tactic/SeqFocus.md)
+  - [<;>: 生成された全ゴールに適用](./Tactic/SeqFocus.md)
   - [ac_rfl: 可換性と結合性を使う](./Tactic/AcRfl.md)
   - [aesop: 自明な証明の自動探索](./Tactic/Aesop.md)
   - [all_goals: 全ゴールに対して適用](./Tactic/AllGoals.md)