From 1a6539208f57eaa24cd2495a1a2af9e30c49d322 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Fri, 4 Oct 2024 01:01:36 +0900 Subject: [PATCH] =?UTF-8?q?=E3=80=8C=E5=B8=B0=E7=B4=8D=E5=9E=8B=E3=80=8D?= =?UTF-8?q?=E3=82=84=E3=80=8C=E6=A7=8B=E9=80=A0=E4=BD=93=E3=80=8D=E3=82=82?= =?UTF-8?q?=E3=83=AA=E3=83=B3=E3=82=AF=E3=81=AB=E3=81=99=E3=82=8B=20Fixes?= =?UTF-8?q?=20#930?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Attribute/CasesEliminator.lean | 2 +- Examples/Attribute/InductionEliminator.lean | 2 +- Examples/Attribute/Simps.lean | 2 +- Examples/Declarative/AddAesopRules.lean | 2 +- Examples/Declarative/Axiom.lean | 2 +- Examples/Declarative/Class.lean | 4 ++-- Examples/Declarative/Structure.lean | 2 +- Examples/Diagnostic/Whnf.lean | 2 +- Examples/Tactic/Cases.lean | 2 +- Examples/Tactic/Constructor.lean | 2 +- Examples/Tactic/Exact.lean | 4 ++-- Examples/Tactic/Exfalso.lean | 2 +- Examples/Tactic/Exists.lean | 2 +- Examples/Tactic/Ext.lean | 2 +- Examples/Tactic/Have.lean | 4 ++-- Examples/Tactic/Obtain.lean | 2 +- Examples/Tactic/Rcases.lean | 2 +- Examples/Type/Prop.lean | 4 ++-- Examples/TypeClass/Decidable.lean | 2 +- Examples/TypeClass/Repr.lean | 2 +- 20 files changed, 24 insertions(+), 24 deletions(-) diff --git a/Examples/Attribute/CasesEliminator.lean b/Examples/Attribute/CasesEliminator.lean index ce54a0ba..63befd12 100644 --- a/Examples/Attribute/CasesEliminator.lean +++ b/Examples/Attribute/CasesEliminator.lean @@ -2,7 +2,7 @@ `[cases_eliminator]` 属性は、[`cases`](../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。 -より詳しくいうと、[`cases`](../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。 +より詳しくいうと、[`cases`](../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、[帰納型](../Declarative/Inductive.md) `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。 -/ namespace CasesEliminator --# diff --git a/Examples/Attribute/InductionEliminator.lean b/Examples/Attribute/InductionEliminator.lean index 235a5887..cfb263cf 100644 --- a/Examples/Attribute/InductionEliminator.lean +++ b/Examples/Attribute/InductionEliminator.lean @@ -2,7 +2,7 @@ `[induction_eliminator]` 属性は、帰納法の枝を変更することを可能にします。 -より詳しくいうと、[`induction`](../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。 +より詳しくいうと、[`induction`](../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、[帰納型](../Declarative/Inductive.md) `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。 -/ namespace InductionEliminator --# diff --git a/Examples/Attribute/Simps.lean b/Examples/Attribute/Simps.lean index 04f17c7c..f37892f6 100644 --- a/Examples/Attribute/Simps.lean +++ b/Examples/Attribute/Simps.lean @@ -2,7 +2,7 @@ 補題を [`simp`](../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。 -例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。 +例えば、ユーザが `Point` という[構造体](../Declarative/Structure.md)を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。 -/ import Mathlib.Tactic.Simps.Basic -- [simps] 属性を使うため diff --git a/Examples/Declarative/AddAesopRules.lean b/Examples/Declarative/AddAesopRules.lean index 2705b2bd..eca3db1c 100644 --- a/Examples/Declarative/AddAesopRules.lean +++ b/Examples/Declarative/AddAesopRules.lean @@ -131,7 +131,7 @@ example (a b c d e : Nat) aesop end --# /- ### constructors -`constructors` ビルダーは、帰納型 `T` の形をしたゴールに遭遇した際に、コンストラクタを適用するように指示します。 +`constructors` ビルダーは、[帰納型](../Declarative/Inductive.md) `T` の形をしたゴールに遭遇した際に、コンストラクタを適用するように指示します。 -/ /-- 自前で定義した偶数を表す命題 -/ diff --git a/Examples/Declarative/Axiom.lean b/Examples/Declarative/Axiom.lean index b88acdc8..048a855f 100644 --- a/Examples/Declarative/Axiom.lean +++ b/Examples/Declarative/Axiom.lean @@ -88,7 +88,7 @@ r a b → Quot.mk r a = Quot.mk r b * 関数の商へのリフト `Quot.lift` * 商の公理 `Quot.sound` -はいずれも他の型からは独立したオブジェクトですが、`Quot.sound` だけが「公理」と呼ばれ、特別扱いされているのは何故でしょうか。以下のように商の公理以外の部分を Lean の帰納型を使って構成してみると理解できるかもしれません。 +はいずれも他の型からは独立したオブジェクトですが、`Quot.sound` だけが「公理」と呼ばれ、特別扱いされているのは何故でしょうか。以下のように商の公理以外の部分を Lean の[帰納型](../Declarative/Inductive.md)を使って構成してみると理解できるかもしれません。 -/ /-- 標準ライブラリの Quot を真似して自作した型 -/ diff --git a/Examples/Declarative/Class.lean b/Examples/Declarative/Class.lean index 8a407155..c4e39a02 100644 --- a/Examples/Declarative/Class.lean +++ b/Examples/Declarative/Class.lean @@ -43,7 +43,7 @@ instance {α : Type} : Monoid (List α) where /- ## 型クラス解決 -型クラスが行っていることを `class` を使わずにDIYしてみると、型クラスの理解が深まるでしょう。`class` として上で定義したものを、もう一度 [`structure`](./Structure.md) として定義してみます。-/ +型クラスが行っていることを `class` を使わずにDIYしてみると、型クラスの理解が深まるでしょう。`class` として上で定義したものを、もう一度 [構造体](./Structure.md)として定義してみます。-/ /-- 構造体でモノイドクラスを真似たもの -/ structure Monoid' (α : Type) where @@ -127,7 +127,7 @@ instance : Plus Nat (List Nat) (List Nat) where end Good --# /- ## class inductive { #ClassInductive } -基本的に型クラスの下部構造は構造体ですが、一般の帰納型を型クラスにすることも可能です。それには `class inductive` というコマンドを使います。 +基本的に型クラスの下部構造は構造体ですが、一般の[帰納型](../Declarative/Inductive.md)を型クラスにすることも可能です。それには `class inductive` というコマンドを使います。 -/ /-- 全単射があるという同値関係 -/ diff --git a/Examples/Declarative/Structure.lean b/Examples/Declarative/Structure.lean index ad9a2a2c..ff663c31 100644 --- a/Examples/Declarative/Structure.lean +++ b/Examples/Declarative/Structure.lean @@ -81,7 +81,7 @@ def foo' : Nat × (Int × String) := ⟨1, 2, "foo"⟩ #guard foo = foo' -/- 一般の帰納型に対しては使用できません。-/ +/- 一般の[帰納型](../Declarative/Inductive.md)に対しては使用できません。-/ inductive Sample where | fst (foo bar : Nat) : Sample diff --git a/Examples/Diagnostic/Whnf.lean b/Examples/Diagnostic/Whnf.lean index fc60dd0f..482fbda1 100644 --- a/Examples/Diagnostic/Whnf.lean +++ b/Examples/Diagnostic/Whnf.lean @@ -1,7 +1,7 @@ /- # \#whnf `#whnf` は、式を弱頭正規形(weak head normal form)に簡約するコマンドです。 -弱頭正規形とは、式の構成要素の最初の部分(head)がそれ以上簡約できない形になっている状態のことです。たとえば式の頭が帰納型のコンストラクタや、ラムダ式になっていれば弱頭正規形です。 +弱頭正規形とは、式の構成要素の最初の部分(head)がそれ以上簡約できない形になっている状態のことです。たとえば式の頭が[帰納型](../Declarative/Inductive.md)のコンストラクタや、ラムダ式になっていれば弱頭正規形です。 -/ import Mathlib.Tactic.Conv -- `#whnf` コマンドを使うために必要 diff --git a/Examples/Tactic/Cases.lean b/Examples/Tactic/Cases.lean index 5117bea3..fb4fdc82 100644 --- a/Examples/Tactic/Cases.lean +++ b/Examples/Tactic/Cases.lean @@ -43,7 +43,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by /- ## 舞台裏 -`cases` は、実際には論理和に限らず帰納型をコンストラクタに分解することができるタクティクです。 +`cases` は、実際には論理和に限らず[帰納型](../Declarative/Inductive.md)をコンストラクタに分解することができるタクティクです。 論理和を分解することができるのも、`Or` が帰納型として定義されているからです。 -/ namespace Cases --# diff --git a/Examples/Tactic/Constructor.lean b/Examples/Tactic/Constructor.lean index 9b271db5..de80960c 100644 --- a/Examples/Tactic/Constructor.lean +++ b/Examples/Tactic/Constructor.lean @@ -45,7 +45,7 @@ example (h : P ↔ Q) (hP : P) : Q := by apply pq assumption -/- また論理積や同値性は構造体なので、次の関数も利用できます。-/ +/- また論理積や同値性は[構造体](../Declarative/Structure.md)なので、次の関数も利用できます。-/ -- 論理積から構成要素を取り出す関数 #check (And.left : P ∧ Q → P) diff --git a/Examples/Tactic/Exact.lean b/Examples/Tactic/Exact.lean index 258b55db..536e34e2 100644 --- a/Examples/Tactic/Exact.lean +++ b/Examples/Tactic/Exact.lean @@ -16,10 +16,10 @@ example (hP : P) (hQ : Q) : P ∧ Q := by example (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ -/-! なお `And` は構造体なので[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/ +/- なお `And` は[構造体](../Declarative/Structure.md)なので[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/ example (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩ -/-! ## assumption との関連 +/- ## assumption との関連 `exact` は常にどの命題を使うか明示する必要がありますが、「ゴールを `exact` で閉じることができるような命題をローカルコンテキストから自動で探す」 [`assumption`](./Assumption.md) というタクティクもあります。-/ diff --git a/Examples/Tactic/Exfalso.lean b/Examples/Tactic/Exfalso.lean index 6224a3fd..58be2091 100644 --- a/Examples/Tactic/Exfalso.lean +++ b/Examples/Tactic/Exfalso.lean @@ -19,7 +19,7 @@ example (h : P) (hn : ¬ P) : P ∧ Q := by /- ローカルコンテキスト内に `P` と `¬ P` があって矛盾することを指摘したい場合は、[`contradiction`](./Contradiction.md) を使うとより簡潔です。また、一般に問題が命題論理に帰着されている状況では [`tauto`](./Tauto.md) または [`itauto`](./Itauto.md) が利用できます。-/ /- ## 舞台裏 -矛盾つまり `False` の項からはどんな命題でも示せるというのは最初は奇妙に感じるかもしれません。実際に `False` の構成を真似て自分で帰納型を定義することによって、同様のことを再現できます。 +矛盾つまり `False` の項からはどんな命題でも示せるというのは最初は奇妙に感じるかもしれません。実際に `False` の構成を真似て自分で[帰納型](../Declarative/Inductive.md)を定義することによって、同様のことを再現できます。 -/ universe u diff --git a/Examples/Tactic/Exists.lean b/Examples/Tactic/Exists.lean index 33096ad3..72b507a5 100644 --- a/Examples/Tactic/Exists.lean +++ b/Examples/Tactic/Exists.lean @@ -27,7 +27,7 @@ Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p -- このとき `w : α` と `h : p w` が与えられたとき `∃ x : α, p x` が成り立つ。 #check (Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α) (h : p w), Exists p) -/- したがって `Exists` は単一のコンストラクタを持つ帰納型、つまり構造体なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/ +/- したがって `Exists` は単一のコンストラクタを持つ[帰納型](../Declarative/Inductive.md)、つまり[構造体](../Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/ example : ∃ x : Nat, 3 * x + 1 = 7 := by exact ⟨2, show 3 * 2 + 1 = 7 from by rfl⟩ diff --git a/Examples/Tactic/Ext.lean b/Examples/Tactic/Ext.lean index 4556fb2c..04721447 100644 --- a/Examples/Tactic/Ext.lean +++ b/Examples/Tactic/Ext.lean @@ -27,7 +27,7 @@ example : s ∩ t = t ∩ s := by aesop /- ## [ext] 属性 -`[ext]` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`[ext]` 属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。 +`[ext]` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`[ext]` 属性は[構造体](../Declarative/Structure.md)に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。 -/ variable {α : Type} diff --git a/Examples/Tactic/Have.lean b/Examples/Tactic/Have.lean index bbd6f403..34221e54 100644 --- a/Examples/Tactic/Have.lean +++ b/Examples/Tactic/Have.lean @@ -21,11 +21,11 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by また `have` で同じ名前を2回宣言すると、古い方はアクセス不能になってしまいます。ローカルコンテキストの補題の置き換えを行いたいときは、代わりに `replace` を使用してください。 -/ -/-! ## 無名コンストラクタ +/- ## 無名コンストラクタ `P` の証明 `hp : P` と `Q` の証明 `hq : Q` があるとき、`P ∧ Q` の証明は `And.intro hp hq` で構成できます。ここで `And.intro` は構造体 `And` 型のコンストラクタです。 -これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の構造体に使用することができます。-/ +これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の[構造体](../Declarative/Structure.md)に使用することができます。-/ variable (hp : P) (hq : Q) def hpq : P ∧ Q := ⟨hp, hq⟩ diff --git a/Examples/Tactic/Obtain.lean b/Examples/Tactic/Obtain.lean index 78f196d2..5271ecc1 100644 --- a/Examples/Tactic/Obtain.lean +++ b/Examples/Tactic/Obtain.lean @@ -29,7 +29,7 @@ example (h : ∃ e : X, P e) : True := by trivial /- -`obtain` に与えることのできるパターンは [`rcases`](./Rcases.md) に与えられるパターンと同様で、一般の帰納型を分解することができます。 +`obtain` に与えることのできるパターンは [`rcases`](./Rcases.md) に与えられるパターンと同様で、一般の[帰納型](../Declarative/Inductive.md)を分解することができます。 -/ inductive Sample where diff --git a/Examples/Tactic/Rcases.lean b/Examples/Tactic/Rcases.lean index 84015a5d..ff2c1b40 100644 --- a/Examples/Tactic/Rcases.lean +++ b/Examples/Tactic/Rcases.lean @@ -23,7 +23,7 @@ example : P ∧ Q → Q ∧ P := by -- `Q ∧ P` を証明する exact ⟨hQ, hP⟩ -/- `rcases` は一般には `⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...` という記法で帰納型の分解が可能です。-/ +/- `rcases` は一般には `⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...` という記法で[帰納型](../Declarative/Inductive.md)の分解が可能です。-/ inductive Sample where | foo (x y : Nat) : Sample diff --git a/Examples/Type/Prop.lean b/Examples/Type/Prop.lean index a94da004..dc671c9e 100644 --- a/Examples/Type/Prop.lean +++ b/Examples/Type/Prop.lean @@ -21,7 +21,7 @@ #guard (False ∧ True) = False #guard (False ∧ False) = False -/- Lean では `And` という名前の構造体(structure)として表現されます。-/ +/- Lean では `And` という名前の[構造体](../Declarative/Structure.md)として表現されます。-/ example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ @@ -34,7 +34,7 @@ example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ #guard False ∨ True #guard (False ∨ False) = False -/- Lean では `Or` という名前の帰納型(inductive type)として表現されます。-/ +/- Lean では `Or` という名前の[帰納型](../Declarative/Inductive.md)として表現されます。-/ example (P Q : Prop) (hP : P) : P ∨ Q := Or.inl hP diff --git a/Examples/TypeClass/Decidable.lean b/Examples/TypeClass/Decidable.lean index e9404c9f..b1e530ab 100644 --- a/Examples/TypeClass/Decidable.lean +++ b/Examples/TypeClass/Decidable.lean @@ -44,7 +44,7 @@ instance (n : Nat) : Decidable (Even n) := by example : Even 4 := by decide /- ## class inductive -`Decidable` 型クラスの定義は少し特殊です。コンストラクタが複数あり、構造体ではなく帰納型の構造をしています。これは `Decidable` が [`class inductive`](../Declarative/Class.md#ClassInductive) というコマンドで定義されているためです。-/ +`Decidable` 型クラスの定義は少し特殊です。コンストラクタが複数あり、[構造体](../Declarative/Structure.md)ではなく[帰納型](../Declarative/Inductive.md)の構造をしています。これは `Decidable` が [`class inductive`](../Declarative/Class.md#ClassInductive) というコマンドで定義されているためです。-/ /-- info: inductive Decidable : Prop → Type diff --git a/Examples/TypeClass/Repr.lean b/Examples/TypeClass/Repr.lean index b4cded2a..15a3fa6e 100644 --- a/Examples/TypeClass/Repr.lean +++ b/Examples/TypeClass/Repr.lean @@ -2,7 +2,7 @@ # Repr `Repr` は、その型の項をどのように表示するかを指示する型クラスです。 -たとえば、以下のように新しく構造体 `Point` を定義したとき、特に何も指定しなければ `Point` の項を `#eval` で表示することはできません。 +たとえば、以下のように新しく[構造体](../Declarative/Structure.md) `Point` を定義したとき、特に何も指定しなければ `Point` の項を `#eval` で表示することはできません。 -/ namespace Repr --#