Skip to content

Commit 95e71f0

Browse files
SeasawherSeasawher
authored
Merge pull request #1399 from lean-ja/remove_relative_path
相対パス表現 `..` を削除する
2 parents a5eac03 + f12af9c commit 95e71f0

26 files changed

+30
-30
lines changed

‎LeanByExample/Attribute/Coe.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ attribute [coe] MyNat.succ
1818
/- また、`[coe]` 属性は [`norm_cast`](#{root}/Tactic/NormCast.md) タクティクとも関係があります。-/
1919

2020
/- ## 用途
21-
型強制を [`Coe`](../TypeClass/Coe.md) 型クラスで登録しただけでは、必ずしも型強制を行う関数が `↑` 記号で表示されるわけではありません。`[coe]` 属性を付与することにより、より「型強制らしく」表示されるようになります。
21+
型強制を [`Coe`](#{root}/TypeClass/Coe.md) 型クラスで登録しただけでは、必ずしも型強制を行う関数が `↑` 記号で表示されるわけではありません。`[coe]` 属性を付与することにより、より「型強制らしく」表示されるようになります。
2222
-/
2323

2424
/-- 自然数の組 -/

‎LeanByExample/Attribute/Simps.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
/- # simps
22
3-
補題を [`simp`](../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
3+
補題を [`simp`](#{root}/Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
44
5-
例えば、ユーザが `Point` という[構造体](../Declarative/Structure.md)を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
5+
例えば、ユーザが `Point` という[構造体](#{root}/Declarative/Structure.md)を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
66
-/
77
import Mathlib.Tactic.Simps.Basic -- [simps] 属性を使うため
88

‎LeanByExample/Declarative/Axiom.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ r a b → Quot.mk r a = Quot.mk r b
8888
* 関数の商へのリフト `Quot.lift`
8989
* 商の公理 `Quot.sound`
9090
91-
この中で `Quot.sound` だけが「公理」と呼ばれ、特別扱いされているのは何故でしょうか。以下のように商の公理以外の部分を Lean の[帰納型](../Declarative/Inductive.md)を使って構成してみると理解できるかもしれません。
91+
この中で `Quot.sound` だけが「公理」と呼ばれ、特別扱いされているのは何故でしょうか。以下のように商の公理以外の部分を Lean の[帰納型](#{root}/Declarative/Inductive.md)を使って構成してみると理解できるかもしれません。
9292
-/
9393

9494
/-- 標準ライブラリの Quot を真似して自作した型 -/

‎LeanByExample/Declarative/Class.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,7 @@ instance : Plus Nat (List Nat) (List Nat) where
128128

129129
end Good --#
130130
/- ## class inductive { #ClassInductive }
131-
基本的に型クラスの下部構造は構造体ですが、一般の[帰納型](../Declarative/Inductive.md)を型クラスにすることも可能です。それには `class inductive` というコマンドを使います。
131+
基本的に型クラスの下部構造は構造体ですが、一般の[帰納型](#{root}/Declarative/Inductive.md)を型クラスにすることも可能です。それには `class inductive` というコマンドを使います。
132132
-/
133133

134134
/-- 全単射があるという同値関係 -/

‎LeanByExample/Declarative/SetOption.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/- # set_option
22
`set_option` は、オプションを変更・設定するために使われるコマンドです。
33
4-
`set_option option_name value` という構文で使用すれば `option_name` という名前のオプションの値を `value` に設定することができます。使用できる `option_name` は [`#help`](../Diagnostic/Help.md) コマンドで確認できます。
4+
`set_option option_name value` という構文で使用すれば `option_name` という名前のオプションの値を `value` に設定することができます。使用できる `option_name` は [`#help`](#{root}/Diagnostic/Help.md) コマンドで確認できます。
55
66
有効範囲はその[セクション](./Section.md)の内部またはそのファイルの最後までです。
77
-/

‎LeanByExample/Diagnostic/Check.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535
-- 命題 Prop
3636
#check True
3737

38-
/- 逆に `term` の型が `T` であることを確かめるには [`example`](../Declarative/Example.md) コマンドを使用して `example : T := term` とします。 -/
38+
/- 逆に `term` の型が `T` であることを確かめるには [`example`](#{root}/Declarative/Example.md) コマンドを使用して `example : T := term` とします。 -/
3939

4040
example : Nat := 42
4141

‎LeanByExample/Diagnostic/Eval.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,4 +39,4 @@ error: could not synthesize a 'Repr' or 'ToString' instance for type
3939
#guard_msgs in
4040
#eval (fun x => x + 1)
4141

42-
/- 一般に、[`Repr`](../TypeClass/Repr.md) や [`ToString`](../TypeClass/ToString.md) および `ToExpr` のインスタンスでないような型の項は `#eval` に渡すことができません。-/
42+
/- 一般に、[`Repr`](#{root}/TypeClass/Repr.md) や [`ToString`](#{root}/TypeClass/ToString.md) および `ToExpr` のインスタンスでないような型の項は `#eval` に渡すことができません。-/

‎LeanByExample/Diagnostic/Guard.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
3232
#guard_msgs (whitespace := lax) in
3333
#guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
3434

35-
/- しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
35+
/- しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](#{root}/TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
3636

3737
-- 型は Prop
3838
/-- info: 1 + 1 = 2 : Prop -/

‎LeanByExample/Diagnostic/Help.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
`#help` は、ドキュメントを確認するためのコマンドです。以下のような機能があります。
44
55
* `#help tactic` で全タクティクのリストが見られます。
6-
* `#help option` で全オプションのリストが見られます。オプションは、[`set_option`](../Declarative/SetOption.md) を実行することで切り替えられます。たとえば、`set_option warningAsError true` と書くと、warning(警告) がエラーとして扱われるようになります。
6+
* `#help option` で全オプションのリストが見られます。オプションは、[`set_option`](#{root}/Declarative/SetOption.md) を実行することで切り替えられます。たとえば、`set_option warningAsError true` と書くと、warning(警告) がエラーとして扱われるようになります。
77
* `#help attr` で全 attribute のリストが見られます。たとえば `simp` という attribute なら、`@[simp] def foo := ...` という風にして登録できます。
88
99
* `#help command` で全コマンドのリストが見られます。

‎LeanByExample/Diagnostic/Print.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ but is expected to have type
7171
## \#print axioms: 依存公理の確認
7272
### 概要
7373
74-
`#print axioms` で、与えられた証明項が依存する公理を出します。たとえば Lean では排中律は選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使って証明するので、排中律は選択原理に依存しています。
74+
`#print axioms` で、与えられた証明項が依存する公理を出します。たとえば Lean では排中律は選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を使って証明するので、排中律は選択原理に依存しています。
7575
-/
7676

7777
/-- 排中律 -/

‎LeanByExample/Diagnostic/Whnf.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/- # \#whnf
22
`#whnf` は、式を弱頭正規形(weak head normal form)に簡約するコマンドです。
33
4-
弱頭正規形とは、式の構成要素の最初の部分(head)がそれ以上簡約できない形になっている状態のことです。たとえば式の頭が[帰納型](../Declarative/Inductive.md)のコンストラクタや、ラムダ式になっていれば弱頭正規形です。
4+
弱頭正規形とは、式の構成要素の最初の部分(head)がそれ以上簡約できない形になっている状態のことです。たとえば式の頭が[帰納型](#{root}/Declarative/Inductive.md)のコンストラクタや、ラムダ式になっていれば弱頭正規形です。
55
-/
66
import Mathlib.Tactic.Conv -- `#whnf` コマンドを使うために必要
77

‎LeanByExample/Modifier/Noncomputable.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
44
Lean は、[`def`](#{root}/Declarative/Def.md) コマンドで定義された関数はすべて計算可能であると想定しています。したがって、計算可能でない関数を定義すると、エラーが発生します。
55
6-
計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。
6+
計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](#{root}/Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。
77
-/
88

99
variable {X Y : Type}

‎LeanByExample/Tactic/Cases.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
4343

4444
/- ## 舞台裏
4545
46-
`cases` は、実際には論理和に限らず[帰納型](../Declarative/Inductive.md)をコンストラクタに分解することができるタクティクです。
46+
`cases` は、実際には論理和に限らず[帰納型](#{root}/Declarative/Inductive.md)をコンストラクタに分解することができるタクティクです。
4747
-/
4848

4949
-- 帰納型として定義した例示のための型

‎LeanByExample/Tactic/Choose.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ theorem choice (h : ∀ x, ∃ y, P x y) : ∃ f : X → Y, ∀ x, P x (f x) :=
1313
exact ⟨f, hf⟩
1414

1515
/- ## 舞台裏
16-
`choose` は裏で選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を使用しています。
16+
`choose` は裏で選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を使用しています。
1717
-/
1818

1919
/-- info: 'choice' depends on axioms: [Classical.choice] -/

‎LeanByExample/Tactic/Constructor.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ example (h : P ↔ Q) (hP : P) : Q := by
4545
apply pq
4646
assumption
4747

48-
/- また論理積や同値性は[構造体](../Declarative/Structure.md)なので、次の関数も利用できます。-/
48+
/- また論理積や同値性は[構造体](#{root}/Declarative/Structure.md)なので、次の関数も利用できます。-/
4949

5050
-- 論理積から構成要素を取り出す関数
5151
#check (And.left : P ∧ Q → P)

‎LeanByExample/Tactic/Decide.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/- # decide
22
`decide` は、決定可能な命題を示すタクティクです。
33
4-
命題 `P : Prop` が決定可能であるとは、型クラス [`Decidable`](../TypeClass/Decidable.md) のインスタンスであることを意味します。`P` が `Decidable` のインスタンスであるとき、`decide` 関数を適用することにより `decide P : Bool` が得られるので、これを呼び出すことによって証明したり反証したりすることができます。つまり一言でいえば、決定可能であるとは決定するためのアルゴリズムが存在するということです。
4+
命題 `P : Prop` が決定可能であるとは、型クラス [`Decidable`](#{root}/TypeClass/Decidable.md) のインスタンスであることを意味します。`P` が `Decidable` のインスタンスであるとき、`decide` 関数を適用することにより `decide P : Bool` が得られるので、これを呼び出すことによって証明したり反証したりすることができます。つまり一言でいえば、決定可能であるとは決定するためのアルゴリズムが存在するということです。
55
-/
66
-- 決定可能な命題を決定する関数 decide が存在する
77
#check (decide : (P : Prop) → [Decidable P] → Bool)

‎LeanByExample/Tactic/Exact.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ example (hP : P) (hQ : Q) : P ∧ Q := by
1717

1818
example (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ
1919

20-
/- なお `And` は[構造体](../Declarative/Structure.md)なので[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
20+
/- なお `And` は[構造体](#{root}/Declarative/Structure.md)なので[無名コンストラクタ](#{root}/Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
2121

2222
example (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩
2323

‎LeanByExample/Tactic/Exfalso.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ example (h : P) (hn : ¬ P) : P ∧ Q := by
1919
/- ローカルコンテキスト内に `P` と `¬ P` があって矛盾することを指摘したい場合は、[`contradiction`](./Contradiction.md) を使うとより簡潔です。また、一般に問題が命題論理に帰着されている状況では [`tauto`](./Tauto.md) または [`itauto`](./Itauto.md) が利用できます。-/
2020

2121
/- ## 舞台裏
22-
矛盾つまり `False` の項からはどんな命題でも示せるというのは最初は奇妙に感じるかもしれません。実際に `False` の構成を真似て自分で[帰納型](../Declarative/Inductive.md)を定義することによって、同様のことを再現できます。
22+
矛盾つまり `False` の項からはどんな命題でも示せるというのは最初は奇妙に感じるかもしれません。実際に `False` の構成を真似て自分で[帰納型](#{root}/Declarative/Inductive.md)を定義することによって、同様のことを再現できます。
2323
-/
2424

2525
universe u

‎LeanByExample/Tactic/Exists.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop where
2929
| intro (w : α) (h : p w) : Exists p
3030

3131
end Exists --#
32-
/- したがって `Exists` は単一のコンストラクタを持つ[帰納型](../Declarative/Inductive.md)、つまり[構造体](../Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
32+
/- したがって `Exists` は単一のコンストラクタを持つ[帰納型](#{root}/Declarative/Inductive.md)、つまり[構造体](#{root}/Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](#{root}/Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
3333

3434
example : ∃ x : Nat, 3 * x + 1 = 7 := by
3535
exact ⟨2, show 3 * 2 + 1 = 7 from by rfl⟩

‎LeanByExample/Tactic/Have.lean

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

3131
def hpq : P ∧ Q := ⟨hp, hq⟩

‎LeanByExample/Tactic/Intro.lean

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

3333
example {S : Prop} (hPR : P → R) (hQR : Q → S) : P ∧ Q → R ∧ S := by

‎LeanByExample/Tactic/Itauto.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
# itauto
33
`itauto` は、直観主義論理(intuitionistic logic)の範囲内でトートロジー(tautology)を証明します。
44
5-
命題論理を扱うタクティクには他にも [`tauto`](./Tauto.md) がありますが、あちらは選択原理 [`Classical.choice`](../Declarative/Axiom.md#ClassicalChoice) を勝手に使用することがあります。なお選択原理は Lean が標準で用意している公理のひとつで、排中律 `P ∨ ¬ P` や二重否定の除去 `¬ ¬ P → P` を示すのに必要です。
5+
命題論理を扱うタクティクには他にも [`tauto`](./Tauto.md) がありますが、あちらは選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を勝手に使用することがあります。なお選択原理は Lean が標準で用意している公理のひとつで、排中律 `P ∨ ¬ P` や二重否定の除去 `¬ ¬ P → P` を示すのに必要です。
66
-/
77
import Mathlib.Tactic.ITauto
88
import Mathlib.Tactic.Tauto

‎LeanByExample/Tactic/Obtain.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ example (h : ∃ e : X, P e) : True := by
2828
trivial
2929

3030
/-
31-
`obtain` に与えることのできるパターンは [`rcases`](./Rcases.md) に与えられるパターンと同様で、一般の[帰納型](../Declarative/Inductive.md)を分解することができます。
31+
`obtain` に与えることのできるパターンは [`rcases`](./Rcases.md) に与えられるパターンと同様で、一般の[帰納型](#{root}/Declarative/Inductive.md)を分解することができます。
3232
-/
3333

3434
inductive Sample where

‎LeanByExample/Tactic/Rcases.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ example : P ∧ Q → Q ∧ P := by
2323
-- `Q ∧ P` を証明する
2424
exact ⟨hQ, hP⟩
2525

26-
/- `rcases` は一般には `⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...` という記法で[帰納型](../Declarative/Inductive.md)の分解が可能です。-/
26+
/- `rcases` は一般には `⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...` という記法で[帰納型](#{root}/Declarative/Inductive.md)の分解が可能です。-/
2727

2828
inductive Sample where
2929
| foo (x y : Nat) : Sample

‎LeanByExample/Type/Char.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
#check ('∀' : Char)
1212
#check ('∅' : Char)
1313

14-
/- `Char` は、以下のように [`structure`](../Declarative/Structure.md) として定義されています。 -/
14+
/- `Char` は、以下のように [`structure`](#{root}/Declarative/Structure.md) として定義されています。 -/
1515

1616
--#--
1717
-- Char の定義が変わっていないことを確認するためのコード

0 commit comments

Comments
 (0)