lean-ja · Seasawher · Dec 19, 2024 · Dec 19, 2024 · Dec 19, 2024 · Dec 19, 2024
@@ -11,13 +11,11 @@
 > 開発に使用する mdbook のバージョンは `0.4.35` に固定してください。`0.4.35` 以外のバージョンではレイアウトが崩れます。
 
 * [mdgen](https://github.com/Seasawher/mdgen) を Lean ファイルから markdown ファイルを生成するために使用しています。
-* [mk_exercise](https://github.com/Seasawher/mk-exercise) を使い、Lean の解答ファイルから演習問題ファイルを生成しています。
 
 ## 開発の流れ
 
 * このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に `lake exe cache get` を実行してください。
-* `LeanByExample/Tutorial/Exercise` ディレクトリ配下のファイルは `mk_exercise` により `LeanByExample/Solution` の内容から自動生成されるので、手動で編集しないでください。
-* 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば mk_exercise の実行と markdown の生成と `mdbook build` が一括実行されます。
+* 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば markdown の生成と `mdbook build` が一括実行されます。
 
 ## ルール
 

@@ -1,6 +1,6 @@
 /- # declare_aesop_rule_sets
 
-`declare_aesop_rule_sets` コマンドは、[`aesop`](#{root}/Reference/Tactic/Aesop.md) タクティクで使用させるための特定のルールセットを宣言します。
+`declare_aesop_rule_sets` コマンドは、[`aesop`](#{root}/Tactic/Aesop.md) タクティクで使用させるための特定のルールセットを宣言します。
 
 ```admonish warning title="注意"
 このページの内容は <i class="fa fa-play"></i> ボタンから Lean 4 Web で実行することができません。
@@ -18,7 +18,7 @@ declare_aesop_rule_sets [HogeRules]
 
 このとき、以下のように `aesop` の `rule_sets` に `HogeRules` を渡すことで、`HogeRules` に登録されたルールセットを使用することができます。
 -/
-import LeanByExample.Reference.Declarative.DeclareAesopRuleSetsLib --#
+import LeanByExample.Declarative.DeclareAesopRuleSetsLib --#
 import Mathlib.Tactic.Says --#
 
 example : True := by

@@ -93,7 +93,7 @@ def even : Nat → Bool
 
 /- 両者の違いは何でしょうか？双方にメリットとデメリットがあります。
 
-再帰関数として定義するメリットとして、計算可能になることが挙げられます。再帰関数として定義されていれば [`#eval`](#{root}/Reference/Diagnostic/Eval.md) コマンドなど、Lean に組み込まれた機能を使って計算を行うことができます。一方で帰納的述語として定義されていると、計算をさせるための準備をこちらで行う必要があります。-/
+再帰関数として定義するメリットとして、計算可能になることが挙げられます。再帰関数として定義されていれば [`#eval`](#{root}/Diagnostic/Eval.md) コマンドなど、Lean に組み込まれた機能を使って計算を行うことができます。一方で帰納的述語として定義されていると、計算をさせるための準備をこちらで行う必要があります。-/
 
 -- すぐに計算できる
 #guard even 4

@@ -3,7 +3,7 @@
 
 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
 -/
-import LeanByExample.Reference.Declarative.Protected -- protected のページをインポート
+import LeanByExample.Declarative.Protected -- protected のページをインポート
 import Lean
 namespace Private --#
 

@@ -62,7 +62,7 @@ instance instMonadMany : Monad Many where
   pure := Many.one
   bind := Many.bind
 
-/- `Monad` 型クラスは [`Functor`](#{root}/Reference/TypeClass/Functor.md) クラスや `Applicative` クラスの実装を含むので、`Many` は `Functor` や `Applicative` のインスタンスでもあります。このインスタンスは次のように `inferInstance` という関数で構成することができますが、その中身を `#print` で出力してみても実装がわかりません。-/
+/- `Monad` 型クラスは [`Functor`](#{root}/TypeClass/Functor.md) クラスや `Applicative` クラスの実装を含むので、`Many` は `Functor` や `Applicative` のインスタンスでもあります。このインスタンスは次のように `inferInstance` という関数で構成することができますが、その中身を `#print` で出力してみても実装がわかりません。-/
 
 def instManyFunctor : Functor Many := inferInstance
 

@@ -4,7 +4,7 @@
 
 ## 背景
 
-証明を書く際のベストプラクティスとして、[`simp`](#{root}/Reference/Tactic/Simp.md) タクティクのような柔軟性のあるタクティクは、証明の末尾以外で使わないほうがよいということが知られています。[^non-terminal-simp] `simp` タクティクはどういう補題が `[simp]` 属性で登録されているかに応じて挙動が変わるため、引用しているライブラリに `simp` 補題が新たに追加されたり、削除されたりするたびに挙動が変わってしまうためです。
+証明を書く際のベストプラクティスとして、[`simp`](#{root}/Tactic/Simp.md) タクティクのような柔軟性のあるタクティクは、証明の末尾以外で使わないほうがよいということが知られています。[^non-terminal-simp] `simp` タクティクはどういう補題が `[simp]` 属性で登録されているかに応じて挙動が変わるため、引用しているライブラリに `simp` 補題が新たに追加されたり、削除されたりするたびに挙動が変わってしまうためです。
 
 たとえば、以下のような証明を考えてみます。
 -/
@@ -46,7 +46,7 @@ end --#
 これは `simp` が柔軟(flexible)なタクティクであることが原因で、対策として次のような方法が知られています。
 
 * 証明末でしか `simp` タクティクを使わない。証明末であれば、「壊れる前の証明において `simp` が何を行っていたか」は常に「残りのゴールを閉じる」であり明確で、ライブラリの変更があってもどう修正すればいいかがわかりやすいからです。
-* [`have`](#{root}/Reference/Tactic/Have.md) タクティクや [`suffices`](#{root}/Reference/Tactic/Suffices.md) タクティクを使って証明末そのものを増やす。
+* [`have`](#{root}/Tactic/Have.md) タクティクや [`suffices`](#{root}/Tactic/Suffices.md) タクティクを使って証明末そのものを増やす。
 * `simp only` 構文を使って、ライブラリ側に変更があっても `simp` タクティクの挙動が変わらないようにする。
 * `simpa` タクティクのような、ゴールを閉じなければならないという制約を持つタクティクで書き換える。
 -/

@@ -42,7 +42,7 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
 
 /- 上記の例により、とくに `aesop` が実行の過程で [`simp_all`](./SimpAll.md) タクティクや `intro` タクティク等を使用することがわかります。
 特に、`aesop` は `simp_all` の強化版であるということができます。
-実際には `aesop` は `simp_all` とは異なり、単純化だけでなく「試行錯誤しながらよい証明を探索する」ということができます。これについて詳しくは [`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) のページを参照してください。-/
+実際には `aesop` は `simp_all` とは異なり、単純化だけでなく「試行錯誤しながらよい証明を探索する」ということができます。これについて詳しくは [`add_aesop_rules`](#{root}/Declarative/AddAesopRules.md) のページを参照してください。-/
 
 /- ## カスタマイズ
 `aesop` はユーザがカスタマイズ可能です。補題やタクティクを登録することで、証明可能な命題を増やすことができます。