diff --git a/LeanByExample/Declarative/Attribute.lean b/LeanByExample/Declarative/Attribute.lean index 5c43dd1f..e63b72af 100644 --- a/LeanByExample/Declarative/Attribute.lean +++ b/LeanByExample/Declarative/Attribute.lean @@ -75,7 +75,7 @@ example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by simp /- ## 有効範囲を制限する -特定の [`section`](./Section.md) でのみ付与した属性を有効にするには、[`local`](./Local.md) で属性名を修飾します。 +特定の [`section`](./Section.md) でのみ付与した属性を有効にするには、[`local`](#{root}/Modifier/Local.md) で属性名を修飾します。 -/ example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by -- simp だけでは証明が終わらない diff --git a/LeanByExample/Declarative/Axiom.lean b/LeanByExample/Declarative/Axiom.lean index 34aaeed9..97c73bb3 100644 --- a/LeanByExample/Declarative/Axiom.lean +++ b/LeanByExample/Declarative/Axiom.lean @@ -203,7 +203,7 @@ theorem my_funext {f g : (x : α) → β x} (h : ∀ x, f x = g x) : f = g := by #guard_msgs in #print axioms my_funext /- ### 選択原理 Classical.choice { #ClassicalChoice } -選択原理は、ある型が空ではないという情報だけから、「魔法のように」具体的な元を構成することができると主張します。これは計算不可能な操作であるため、選択原理を使用する関数には [`noncomputable`](./Noncomputable.md) 修飾子が必要になります。 +選択原理は、ある型が空ではないという情報だけから、「魔法のように」具体的な元を構成することができると主張します。これは計算不可能な操作であるため、選択原理を使用する関数には [`noncomputable`](#{root}/Modifier/Noncomputable.md) 修飾子が必要になります。 選択原理は数学でいうと NBG(Neumann-Bernays-Gödel) 集合論における大域選択公理(axiom of global choice)とよく似ています。 -/ diff --git a/LeanByExample/Declarative/Opaque.lean b/LeanByExample/Declarative/Opaque.lean index 6677d81b..162be6b9 100644 --- a/LeanByExample/Declarative/Opaque.lean +++ b/LeanByExample/Declarative/Opaque.lean @@ -3,7 +3,7 @@ ## def との違い -[`def`](./Def.md) と異なり `opaque` コマンドを使用して宣言した名前は、`#reduce` コマンドで簡約できません。 +[`def`](./Def.md) コマンドと異なり `opaque` コマンドを使用して宣言した名前は、`#reduce` コマンドで簡約できません。 -/ -- def を使って定義 @@ -29,7 +29,7 @@ opaque opaque_greet : String := "hello world!" /-- info: opaque_greet -/ #guard_msgs in #reduce opaque_greet -/- `opaque` で宣言された名前は [`partial`](./Partial.md) で修飾された名前と同様に証明の中で簡約できなくなり、コンパイラを信頼しないとそれに関する証明ができなくなります。-/ +/- `opaque` で宣言された名前は [`partial`](#{root}/Modifier/Partial.md) で修飾された名前と同様に証明の中で簡約できなくなり、コンパイラを信頼しないとそれに関する証明ができなくなります。-/ -- 等しいものだという判定はできる #eval opaque_greet == greet diff --git a/LeanByExample/Declarative/Section.lean b/LeanByExample/Declarative/Section.lean index 252c2903..f69eac63 100644 --- a/LeanByExample/Declarative/Section.lean +++ b/LeanByExample/Declarative/Section.lean @@ -5,7 +5,7 @@ * [`variable`](./Variable.md) で定義された引数の有効範囲を制限する。 * [`open`](./Open.md) で開いた名前空間の有効範囲を制限する。 * [`set_option`](./SetOption.md) で設定したオプションの有効範囲を制限する。 -* [`local`](./Local.md) で修飾されたコマンドの有効範囲を制限する。 +* [`local`](#{root}/Modifier/Local.md) で修飾されたコマンドの有効範囲を制限する。 `section` コマンドで開いたセクションは `end` で閉じることができますが、`end` は省略することもできます。`end` を省略した場合はそのファイルの終わりまでが有効範囲となります。 diff --git a/LeanByExample/Declarative/Local.lean b/LeanByExample/Modifier/Local.lean similarity index 78% rename from LeanByExample/Declarative/Local.lean rename to LeanByExample/Modifier/Local.lean index d5262a79..8634df99 100644 --- a/LeanByExample/Declarative/Local.lean +++ b/LeanByExample/Modifier/Local.lean @@ -1,5 +1,5 @@ /- # local -`local` はコマンドをその [`section`](./Section.md) の内部でだけ有効にするための修飾子です。 +`local` はコマンドをその [`section`](#{root}/Declarative/Section.md) の内部でだけ有効にするための修飾子です。 -/ import Lean --# section foo @@ -20,7 +20,7 @@ section foo #check_failure succ' end foo -/- コマンドの有効範囲を [`namespace`](./Namespace.md) の内部に限定するのにも使えます。ただし、下記のコードで示しているように、`local` で修飾したコマンドの効果は同じ名前空間の中で永続するのではなく、`end` でその名前空間が閉じられたときに消失します。-/ +/- コマンドの有効範囲を [`namespace`](#{root}/Declarative/Namespace.md) の内部に限定するのにも使えます。ただし、下記のコードで示しているように、`local` で修飾したコマンドの効果は同じ名前空間の中で永続するのではなく、`end` でその名前空間が閉じられたときに消失します。-/ namespace hoge -- local を付けて新しい記法を定義 @@ -43,14 +43,14 @@ end hoge /- ## 修飾可能なコマンド `local` で有効範囲を限定できるコマンドには、次のようなものがあります。 -* [`elab`](./Elab.md), `elab_rules` -* [`infix`](./Infix.md), `infil`, `infixr` -* [`macro`](./Macro.md), [`macro_rules`](./MacroRules.md) -* [`notation`](./Notation.md) -* [`postfix`](./Postfix.md) -* [`prefix`](./Prefix.md) -* [`instance`](./Instance.md) -* [`syntax`](./Syntax.md) +* [`elab`](#{root}/Declarative/Elab.md), `elab_rules` +* [`infix`](#{root}/Declarative/Infix.md), `infil`, `infixr` +* [`macro`](#{root}/Declarative/Macro.md), [`macro_rules`](#{root}/Declarative/MacroRules.md) +* [`notation`](#{root}/Declarative/Notation.md) +* [`postfix`](#{root}/Declarative/Postfix.md) +* [`prefix`](#{root}/Declarative/Prefix.md) +* [`instance`](#{root}/Declarative/Instance.md) +* [`syntax`](#{root}/Declarative/Syntax.md) * などなど リストの全体は、`local` の後に修飾できないコマンドを続けたときのエラーメッセージで確認できます。 @@ -93,7 +93,7 @@ end #check_failure (0 : MyNat) /- ## 属性に対する local -属性付与の効果範囲を限定するためには、[`attribute`](./Attribute.md) コマンドを `local` で修飾するのではなく、`attribute` コマンドの中で `local` を使います。 +属性付与の効果範囲を限定するためには、[`attribute`](#{root}/Declarative/Attribute.md) コマンドを `local` で修飾するのではなく、`attribute` コマンドの中で `local` を使います。 -/ def MyNat.add (n m : MyNat) : MyNat := diff --git a/LeanByExample/Declarative/Noncomputable.lean b/LeanByExample/Modifier/Noncomputable.lean similarity index 70% rename from LeanByExample/Declarative/Noncomputable.lean rename to LeanByExample/Modifier/Noncomputable.lean index d18483c9..f527aea7 100644 --- a/LeanByExample/Declarative/Noncomputable.lean +++ b/LeanByExample/Modifier/Noncomputable.lean @@ -1,9 +1,9 @@ /- # noncomputable `noncomputable` は、宣言された関数が計算可能でないことを Lean に伝えるために使われます。 -Lean は、[`def`](./Def.md) で定義された関数はすべて計算可能であると想定しています。したがって、計算可能でない関数を定義すると、エラーが発生します。 +Lean は、[`def`](#{root}/Declarative/Def.md) コマンドで定義された関数はすべて計算可能であると想定しています。したがって、計算可能でない関数を定義すると、エラーが発生します。 -計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](./Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。 +計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。 -/ variable {X Y : Type} @@ -42,7 +42,7 @@ noncomputable def inverse (f : X → Y) (hf : Surjective f) : Y → X := by have x := Classical.choice this exact x.val -/- `noncomputable` とマークされた式を含む式は文字通り評価不能になり、[`#eval`](../Diagnostic/Eval.md) に渡すことができなくなります。-/ +/- `noncomputable` とマークされた式を含む式は文字通り評価不能になり、[`#eval`](#{root}/Diagnostic/Eval.md) に渡すことができなくなります。-/ -- 補助として `id` という恒等写像が全射であることを示しておく theorem id_surjective : Surjective (id : Nat → Nat) := by diff --git a/LeanByExample/Declarative/Partial.lean b/LeanByExample/Modifier/Partial.lean similarity index 94% rename from LeanByExample/Declarative/Partial.lean rename to LeanByExample/Modifier/Partial.lean index 6379c803..b4529c88 100644 --- a/LeanByExample/Declarative/Partial.lean +++ b/LeanByExample/Modifier/Partial.lean @@ -59,7 +59,7 @@ partial def forever (x : Int) : Int := -- more 関数も停止しないが、partial は不要である def more := @forever -/- これは意外に思えます。`partial` とマークされた関数は停止性が保証されていないので、それを使用した関数も停止性を保証できなくなるはずだからです。なぜこうなるのかというと、`partial` はそもそも「停止性が保証されていない」ことを表すものではなく、[`opaque`](./Opaque.md) と同様に「名前が定義に展開できない」ことを表すものだからです。-/ +/- これは意外に思えます。`partial` とマークされた関数は停止性が保証されていないので、それを使用した関数も停止性を保証できなくなるはずだからです。なぜこうなるのかというと、`partial` はそもそも「停止性が保証されていない」ことを表すものではなく、[`opaque`](#{root}/Declarative/Opaque.md) と同様に「名前が定義に展開できない」ことを表すものだからです。-/ -- 実際に #reduce を実行してみると、 -- forever の部分が簡約されていないことがわかる diff --git a/LeanByExample/Declarative/Private.lean b/LeanByExample/Modifier/Private.lean similarity index 94% rename from LeanByExample/Declarative/Private.lean rename to LeanByExample/Modifier/Private.lean index a41272d5..eb3a8eb3 100644 --- a/LeanByExample/Declarative/Private.lean +++ b/LeanByExample/Modifier/Private.lean @@ -3,7 +3,7 @@ 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。 -/ -import LeanByExample.Declarative.Protected -- protected のページをインポート +import LeanByExample.Modifier.Protected -- protected のページをインポート import Lean namespace Private --# diff --git a/LeanByExample/Declarative/Protected.lean b/LeanByExample/Modifier/Protected.lean similarity index 87% rename from LeanByExample/Declarative/Protected.lean rename to LeanByExample/Modifier/Protected.lean index 3fffb037..b1f5e8c2 100644 --- a/LeanByExample/Declarative/Protected.lean +++ b/LeanByExample/Modifier/Protected.lean @@ -67,7 +67,7 @@ end Foo /- ## protected def 以外の用法 -`def` コマンドに対してだけでなく、[`indudctive`](./Inductive.md) コマンドで生成されるコンストラクタに対しても使用可能です。-/ +`def` コマンドに対してだけでなく、[`indudctive`](#{root}/Declarative/Inductive.md) コマンドで生成されるコンストラクタに対しても使用可能です。-/ section --# /-- 2分木 -/ @@ -88,7 +88,7 @@ open BinTree #check empty end --# -/- また [`structure`](./Structure.md) コマンドで生成されるアクセサ関数やコンストラクタに対しても使用可能です。 -/ +/- また [`structure`](#{root}/Declarative/Structure.md) コマンドで生成されるアクセサ関数やコンストラクタに対しても使用可能です。 -/ section --# structure Sample where -- コンストラクタも protected にできる diff --git a/LeanByExample/Modifier/README.lean b/LeanByExample/Modifier/README.lean new file mode 100644 index 00000000..8f13def6 --- /dev/null +++ b/LeanByExample/Modifier/README.lean @@ -0,0 +1,4 @@ +/- # 修飾子 + +本書では、必ず後ろにトップレベルコマンドが続いて、後続のコマンドに影響を与える構文要素のことを便宜的に修飾子と呼んでいます。 +-/ diff --git a/LeanByExample/Declarative/Scoped.lean b/LeanByExample/Modifier/Scoped.lean similarity index 84% rename from LeanByExample/Declarative/Scoped.lean rename to LeanByExample/Modifier/Scoped.lean index 833d6b74..c41e962c 100644 --- a/LeanByExample/Declarative/Scoped.lean +++ b/LeanByExample/Modifier/Scoped.lean @@ -35,14 +35,14 @@ end /- ## 修飾可能なコマンド `scoped` で有効範囲を限定できるコマンドには、次のようなものがあります。 -* [`elab`](./Elab.md), `elab_rules` -* [`infix`](./Infix.md), `infixl`, `infixr` -* [`instance`](./Instance.md) -* [`macro`](./Macro.md), [`macro_rules`](./MacroRules.md) -* [`notation`](./Notation.md) -* [`postfix`](./Postfix.md) -* [`prefix`](./Prefix.md), -* [`syntax`](./Syntax.md) +* [`elab`](#{root}/Declarative/Elab.md), `elab_rules` +* [`infix`](#{root}/Declarative/Infix.md), `infixl`, `infixr` +* [`instance`](#{root}/Declarative/Instance.md) +* [`macro`](#{root}/Declarative/Macro.md), [`macro_rules`](#{root}/Declarative/MacroRules.md) +* [`notation`](#{root}/Declarative/Notation.md) +* [`postfix`](#{root}/Declarative/Postfix.md) +* [`prefix`](#{root}/Declarative/Prefix.md), +* [`syntax`](#{root}/Declarative/Syntax.md) * などなど リストの全体は、`scoped` の後に修飾できないコマンドを続けたときのエラーメッセージで確認できます。 @@ -65,7 +65,7 @@ error: :1:7: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si run_meta parse `command "scoped def" /- ## open scoped -`open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](./Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。 +`open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](#{root}/Declarative/Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。 -/ namespace Foo diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 56692b5c..db6e1822 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -41,21 +41,15 @@ - [inductive: 帰納型を定義する](./Declarative/Inductive.md) - [infix: 中置記法](./Declarative/Infix.md) - [instance: インスタンスを定義する](./Declarative/Instance.md) - - [local: 有効範囲をセクションで限定](./Declarative/Local.md) - [macro_rules: 構文展開の追加](./Declarative/MacroRules.md) - [macro: 簡便なマクロ定義](./Declarative/Macro.md) - [namespace: 名前空間を宣言する](./Declarative/Namespace.md) - - [noncomputable: 計算不能にする](./Declarative/Noncomputable.md) - [notation: 記法を導入する](./Declarative/Notation.md) - [opaque: 簡約できない名前を宣言](./Declarative/Opaque.md) - [open: 名前空間を開く](./Declarative/Open.md) - - [partial: 再帰の停止証明をしない](./Declarative/Partial.md) - [postfix: 後置記法](./Declarative/Postfix.md) - [prefix: 前置記法](./Declarative/Prefix.md) - - [private: 定義を不可視にする](./Declarative/Private.md) - [proof_wanted: 証明を公募する](./Declarative/ProofWanted.md) - - [protected: フルネームを強制する](./Declarative/Protected.md) - - [scoped: 有効範囲を名前空間で限定](./Declarative/Scoped.md) - [section: 有効範囲を制限する](./Declarative/Section.md) - [set_option: オプション設定](./Declarative/SetOption.md) - [structure: 構造体を定義する](./Declarative/Structure.md) @@ -64,6 +58,14 @@ - [theorem: 命題を証明する](./Declarative/Theorem.md) - [variable: 引数を共通化する](./Declarative/Variable.md) +- [修飾子](./Modifier/README.md) + - [local: 有効範囲をセクションで限定](./Modifier/Local.md) + - [noncomputable: 計算不能にする](./Modifier/Noncomputable.md) + - [partial: 再帰の停止証明をしない](./Modifier/Partial.md) + - [private: 定義を不可視にする](./Modifier/Private.md) + - [protected: フルネームを強制する](./Modifier/Protected.md) + - [scoped: 有効範囲を名前空間で限定](./Modifier/Scoped.md) + - [属性](./Attribute/README.md) - [app_unexpander: 関数適用の表示](./Attribute/AppUnexpander.md) - [cases_eliminator: 独自場合分け](./Attribute/CasesEliminator.md)