From 1fcbec71fe2e2208d48326088babfbc19d36256b Mon Sep 17 00:00:00 2001
From: s-taiga <56785231+s-taiga@users.noreply.github.com>
Date: Sat, 23 Nov 2024 13:42:14 +0900
Subject: [PATCH] =?UTF-8?q?Simp=E7=BF=BB=E8=A8=B3=20(#14)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* 翻訳開始

* 翻訳完了
---
 GLOSSARY.md                   |  11 +-
 Manual/Elaboration.lean       |   4 +-
 Manual/Intro.lean             |  14 +-
 Manual/Language.lean          |   2 +-
 Manual/Language/Files.lean    |   4 +-
 Manual/Simp.lean              | 334 ++++++++++++++++++++++++++++++++--
 Manual/Tactics/Reference.lean |   2 +-
 7 files changed, 342 insertions(+), 29 deletions(-)

diff --git a/GLOSSARY.md b/GLOSSARY.md
index f72e33f..2718662 100644
--- a/GLOSSARY.md
+++ b/GLOSSARY.md
@@ -37,6 +37,8 @@
 | command elaboration | コマンドエラボレーション | |
 | compilation | コンパイル | |
 | completion | 補完 | |
+| confluence | 合流性 | |
+| conjunction | 連言 | |
 | consistency | 一貫性 | |
 | constant | 定数 | |
 | construction | 構成 | |
@@ -76,6 +78,7 @@
 | environment | 環境 | |
 | environment extensions | 環境拡張 | |
 | equational lemma | 等式の補題 | |
+| equivalence | 同値性 | |
 | equivalent | 同値 | |
 | evaluate | 評価 | |
 | evidence | 根拠 | |
@@ -162,6 +165,7 @@
 | nested | ネストされた | |
 | newline | 改行 | |
 | non-dependent | 非依存的 | |
+| normal form | 正規形 | |
 | notation | 記法 | |
 | opaque | 不透明 | |
 | operator | 演算子 | |
@@ -178,6 +182,7 @@
 | pretty printer | プリティプリンタ | |
 | primitive | プリミティブ | |
 | primitive recursion | 原始再帰 | |
+| procedure | 手続き | |
 | product type | 直積型 | |
 | projection function | 射影関数 | |
 | proof checker | 証明チェッカ | |
@@ -200,6 +205,7 @@
 | representation | 表現 | |
 | reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
 | reserved word | 予約語 | |
+| rewrite | 書き換え | |
 | run-length encoding | 連長圧縮 | |
 | run-time | ランタイム | |
 | rule | 規則 | |
@@ -208,12 +214,15 @@
 | scope | スコープ | |
 | scrutinee | 被検査対象 | |
 | separator | 区切り文字 | |
-| set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | |
+| set | （数学的な集合の場合）集合、（数学的な集合を意味しない場合でプログラミング上実体のある集まりの場合）セット、（それ以外）あつまり | |
 | section | 節 | |
 | serialize | シリアライズ | |
 | shadow | （変数の隠蔽の意で）シャドーイング | |
 | side effect | 副作用 | |
 | signature | シグネチャ | |
+| simplifier | 単純化器 | |
+| simplify | 単純化 | |
+| simp set | simp セット | |
 | single quote | シングルクォート | |
 | singleton | 単集合 | |
 | soundness | 健全性 | |
diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
index 13bc00b..a0c7297 100644
--- a/Manual/Elaboration.lean
+++ b/Manual/Elaboration.lean
@@ -210,7 +210,7 @@ Term elaboration may modify all of these fields except the open scopes.
 Additionally, it has access to all the machinery needed to create fully-explicit terms in the core language from Lean's terse, friendly syntax, including unification, type class instance synthesis, and type checking.
 :::
 
-コマンドエラボレーションと項エラボレーションは異なる能力を持ちます。コマンドエラボレーションは環境に副作用を与える可能性があり、 {lean}`IO` で任意の計算を実行するアクセス権を持っています。Lean の環境は名前から定義への通常のマッピングに加え、 {deftech}[環境拡張] （environment extension）で定義される追加データを含んでいます；環境拡張は {tactic}`simp` 補題・カスタムのプリティプリンタ・コンパイラの中間表現などの内部を含む、Lean コードに関する他のほとんどの情報を追跡するために使用されます。コマンドエラボレーションはまた、コンパイラの情報出力・警告・およびエラー内容を含むメッセージログ・メタデータをもとの構文に関連付ける {tech}[情報木] のあつまり（証明状態の表示・識別子の補完・ドキュメントの表示などの対話的な機能に使用されます）・蓄積されたデバッグトレース・開いた {tech}[scope] ・マクロ展開に関連するいくつかの内部状態を維持します。項エラボレーションは開いたスコープを除くこれらすべてのフィールドを変更することができます。さらに、Lean の簡潔で親しみやすい構文からコア言語で完全に明示的な項を作成するために必要な単一化・型クラスインスタンス合成・型チェックを含むすべての機構にアクセスすることができます。
+コマンドエラボレーションと項エラボレーションは異なる能力を持ちます。コマンドエラボレーションは環境に副作用を与える可能性があり、 {lean}`IO` で任意の計算を実行するアクセス権を持っています。Lean の環境は名前から定義への通常のマッピングに加え、 {deftech}[環境拡張] （environment extension）で定義される追加データを含んでいます；環境拡張は {tactic}`simp` 補題・カスタムのプリティプリンタ・コンパイラの中間表現などの内部を含む、Lean コードに関する他のほとんどの情報を追跡するために使用されます。コマンドエラボレーションはまた、コンパイラの情報出力・警告・およびエラー内容を含むメッセージログ・メタデータをもとの構文に関連付ける {tech}[情報木] のセット（証明状態の表示・識別子の補完・ドキュメントの表示などの対話的な機能に使用されます）・蓄積されたデバッグトレース・開いた {tech}[scope] ・マクロ展開に関連するいくつかの内部状態を維持します。項エラボレーションは開いたスコープを除くこれらすべてのフィールドを変更することができます。さらに、Lean の簡潔で親しみやすい構文からコア言語で完全に明示的な項を作成するために必要な単一化・型クラスインスタンス合成・型チェックを含むすべての機構にアクセスすることができます。
 
 :::comment
 The first step in both term and command elaboration is macro expansion.
@@ -232,7 +232,7 @@ Command elaborators accept syntax and return no value, but may have monadic side
 While both term and command elaborators have access to {lean}`IO`, it's unusual that they perform side effects; exceptions include interactions with external tools or solvers.
 :::
 
-マクロ展開の後、項とコマンドエラボレータのどちらも、構文の種をエラボレータの処理にマップするテーブルを参照します。項エラボレータは、構文とオプションで期待される型を、前述の非常に機能的なモナドを使用するコア言語の式にマッピングします。コマンドエラボレータは構文を受け入れ、値を返しませんが、グローバルのコマンド状態に対してモナドの副作用を持つかもしれません。項とコマンドエラボレータのどちらも {lean}`IO` にアクセスできますが、副作用を実行するのは一般的ではありません；例外は外部ツールやソルバとのやり取りを含みます。
+マクロ展開の後、項とコマンドエラボレータのどちらも、構文の種をエラボレータの手続きにマップするテーブルを参照します。項エラボレータは、構文とオプションで期待される型を、前述の非常に機能的なモナドを使用するコア言語の式にマッピングします。コマンドエラボレータは構文を受け入れ、値を返しませんが、グローバルのコマンド状態に対してモナドの副作用を持つかもしれません。項とコマンドエラボレータのどちらも {lean}`IO` にアクセスできますが、副作用を実行するのは一般的ではありません；例外は外部ツールやソルバとのやり取りを含みます。
 
 :::comment
 The elaborator tables may be extended to enable the use of new syntax for both terms and commands by extending the tables.
diff --git a/Manual/Intro.lean b/Manual/Intro.lean
index a81bf9f..6ec7507 100644
--- a/Manual/Intro.lean
+++ b/Manual/Intro.lean
@@ -17,7 +17,7 @@ set_option pp.rawOnError true
 /-
 #doc (Manual) "Introduction" =>
 -/
-#doc (Manual) "はじめに" =>
+#doc (Manual) "はじめに（Introduction）" =>
 %%%
 htmlSplit := .never
 %%%
@@ -71,7 +71,7 @@ Lean のプログラムは新しいタクティクや証明の自動化を実装
 ## History
 :::
 
-## 歴史
+## 歴史（History）
 
 :::comment
 Leonardo de Moura launched the Lean project when he was at Microsoft Research in 2013, and Lean 0.1 was officially released on June 16, 2014.
@@ -115,7 +115,7 @@ Leonardo de Moura と彼の共同設立者である Sebastian Ullrich は2023年
 # Typographical Conventions
 :::
 
-# 表記ルール
+# 表記規則（Typographical Conventions）
 
 :::comment
 This document makes use of a number of typographical and layout conventions to indicate various aspects of the information being presented.
@@ -127,7 +127,7 @@ This document makes use of a number of typographical and layout conventions to i
 ## Lean Code
 :::
 
-## Lean のコード
+## Lean のコード（Lean Code）
 
 :::comment
 This document contains many Lean code examples.
@@ -234,7 +234,7 @@ Identifiers in code examples are hyperlinked to their documentation.
 ## Examples
 :::
 
-## 例
+## 例（Examples）
 
 :::comment
 Illustrative examples are in callout boxes, as below:
@@ -271,7 +271,7 @@ inductive Even : Nat → Prop where
 ## Technical Terminology
 :::
 
-## 専門用語
+## 専門用語（Technical Terminology）
 
 :::comment
 {deftech}_Technical terminology_ refers to terms used in a very specific sense when writing technical material, such as this reference.
@@ -284,7 +284,7 @@ Uses of {tech}[technical terminology] are frequently hyperlinked to their defini
 ## Constant, Syntax, and Tactic References
 :::
 
-## 定数・構文・タクティクの参照
+## 定数・構文・タクティクの参照（Constant, Syntax, and Tactic References）
 
 :::comment
 Definitions, inductive types, syntax formers, and tactics have specific descriptions.
diff --git a/Manual/Language.lean b/Manual/Language.lean
index a51ea8c..d9f01e7 100644
--- a/Manual/Language.lean
+++ b/Manual/Language.lean
@@ -44,7 +44,7 @@ Only well-typed terms have a meaning.
 
 :::
 
-{deftech}_項_ （term）は {deftech}_式_ （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは {tech}[エラボレータ] によってユーザが書いた構文から生成されます。Lean の型システムは項をその _型_ （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論のルールに従った型を持つ項は {deftech}_well-typed_ と言います。well-typed である項のみが意味を持ちます。
+{deftech}_項_ （term）は {deftech}_式_ （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは {tech}[エラボレータ] によってユーザが書いた構文から生成されます。Lean の型システムは項をその _型_ （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論の規則に従った型を持つ項は {deftech}_well-typed_ と言います。well-typed である項のみが意味を持ちます。
 
 :::comment
 Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and `let`-bindings.
diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean
index 2ab1895..e3214dd 100644
--- a/Manual/Language/Files.lean
+++ b/Manual/Language/Files.lean
@@ -218,7 +218,7 @@ These keywords must also be quoted with guillemets to be used as identifier comp
 Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier]
 :::
 
-識別子要素として予約キーワードを使うことがあるかもしれません。予約キーワードの特定のあつまりは、アクティブな構文拡張のあつまりに依存し、またそれらはインポートされたモジュールと現在開いている名前空間のあつまりに依存するかもしれません；Lean はこれを列挙することができません。これらのキーワードはほとんどの構文で識別子の構成要素として使用するために、ギュメでクォートする必要があります。帰納的データ型のコンストラクタ名など、キーワードをギュメなしで識別子として使用できるコンテキストは {deftech}_生識別子_ （raw identifier）コンテキストです。 {index (subterm:="raw")}[identifier]
+識別子要素として予約キーワードを使うことがあるかもしれません。予約キーワードの特定のセットは、アクティブな構文拡張のセットに依存し、またそれらはインポートされたモジュールと現在開いている名前空間のセットに依存するかもしれません；Lean はこれを列挙することができません。これらのキーワードはほとんどの構文で識別子の構成要素として使用するために、ギュメでクォートする必要があります。帰納的データ型のコンストラクタ名など、キーワードをギュメなしで識別子として使用できるコンテキストは {deftech}_生識別子_ （raw identifier）コンテキストです。 {index (subterm:="raw")}[identifier]
 
 :::comment
 Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers].
@@ -308,7 +308,7 @@ Modules do not necessarily correspond to namespaces.
 Modules may add names to any namespace, and importing a module has no effect on the set of currently open namespaces.
 :::
 
-モジュールは必ずしも名前空間に対応するとは限りません。モジュールはどの名前空間にも名前を追加することができ、モジュールをインポートしても現在開いている名前空間のあつまりには影響しません。
+モジュールは必ずしも名前空間に対応するとは限りません。モジュールはどの名前空間にも名前を追加することができ、モジュールをインポートしても現在開いている名前空間のセットには影響しません。
 
 :::comment
 The imported module name is translated to a filename by replacing dots (`'.'`) in its name with directory separators.
diff --git a/Manual/Simp.lean b/Manual/Simp.lean
index bc2784f..79e6ba4 100644
--- a/Manual/Simp.lean
+++ b/Manual/Simp.lean
@@ -16,57 +16,131 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "The Simplifier" =>
+-/
+#doc (Manual) "単純化器（The Simplifier）" =>
 %%%
 tag := "the-simplifier"
 %%%
 
+:::comment
 The simplifier is one of the most-used features of Lean.
 It performs inside-out rewriting of terms based on a database of simplification rules.
 The simplifier is highly configurable, and a number of tactics use it in different ways.
 
+:::
+
+単純化器は Lean で最もよく使われる機能の1つです。これは単純化規則のデータベースに基づいて、項を隅から隅まで書き換えます。単純化器は高度に設定可能であり、多くのタクティクが様々な方法で単純化器を使用しています。
+
+:::comment
 # Invoking the Simplifier
 
+:::
+
+# 単純化器の呼び出し（Invoking the Simplifier）
+
+:::comment
 Lean's simplifier can be invoked in a variety of ways.
 The most common patterns are captured in a set of tactics.
 The {ref "simp-tactics"}[tactic reference] contains a complete list of simplification tactics.
 
+:::
+
+Lean の単純化器はさまざまな方法で呼び出すことができます。最も一般的なパターンはタクティクのセットに含まれています。 {ref "simp-tactics"}[タクティクのリファレンス] には、単純化タクティクの完全なリストが含まれています。
+
+:::comment
 Simplification tactics all contain `simp` in their name.
 Aside from that, they are named according to a system of prefixes and suffixes that describe their functionality:
 
+:::
+
+単純化器のタクティクはすべて名前に `simp` を含んでいます。それはともかく、それらはその機能を表す接頭辞と接尾辞のシステムに従って命名されます：
+
+:::comment
 : `-!` suffix
 
   Sets the {name Lean.Meta.Simp.Config.autoUnfold}`autoUnfold` configuration option to `true`, causing the simplifier unfold all definitions
 
+:::
+
+: `-!` 接尾辞
+
+  {name Lean.Meta.Simp.Config.autoUnfold}`autoUnfold` 設定オプションを `true` にし、これにより単純化器はすべての定義を展開します
+
+:::comment
 : `-?` suffix
 
   Causes the simplifier to keep track of which rules it employed during simplification and suggest a minimal {tech}[simp set] as an edit to the tactic script
 
+:::
+
+: `-?` 接尾辞
+
+  単純化スクリプトが単純化中にどの規則を採用したかを追跡し、単純化スクリプトを記述する上で最小の {tech}[simp セット] を提案するようにします
+
+:::comment
 : `-_arith` suffix
 
   Enables the use of linear arithmetic simplification rules
 
+:::
+
+: `-_arith` 接尾辞
+
+  線形算術の単純化規則の使用を可能にします
+
+:::comment
 : `d-` prefix
 
   Causes the simplifier to simplify only with rewrites that hold definitionally
 
+:::
+
+: `d-` 接頭辞
+
+  定義上成立する書き換えのみを単純化します
+
+:::comment
 : `-_all` suffix
 
   Causes the simplifier to repeatedly simplify all assumptions and the conclusion of the goal, taking as many hypotheses into account as possible, until no further simplification is possible
 
+:::
+
+: `-_all` 接尾辞
+
+  これ以上の単純化が不可能になるまで、可能な限り多くの仮定を考慮に入れながら単純化器にすべての仮定とゴールの結論を繰り返し単純化させます
+
+:::comment
 There are two further simplification tactics, {tactic}`simpa` and {tactic}`simpa!`, which are used to simultaneously simplify a goal and either a proof term or an assumption before discharging the goal.
 This simultaneous simplification makes proofs more robust to changes in the {tech}[simp set].
 
+:::
+
+これらに加えて2つの単純化タクティク {tactic}`simpa` と {tactic}`simpa!` があります。これらはゴールを終了する前に、ゴールと証明項・仮定を同時に単純化するために用いられます。この同時単純化により、 {tech}[simp セット] の変更に対して証明がより頑強になります。
+
+:::comment
 ## Parameters
 
+:::
+
+## パラメータ（Parameters）
+
+:::comment
 The simplification tactics have the following grammar:
 
+:::
+
+単純化タクティクは以下のような文法を持ちます：
+
 :::syntax tactic
 ```grammar
 simp $[(config := $cfg)]? $[only]? $[ [ $[$e],* ] ]? $[at $[$h]*]?
 ```
 :::
 
+:::comment
 In other words, an invocation of a simplification tactic takes the following modifiers, in order, all of which are optional:
  * A configuration specifier, which should be an instance of {name}`Lean.Meta.Simp.Config` or {name}`Lean.Meta.DSimp.Config`, depending on whether the simplifier being invoked is a version of {tactic}`simp` or a version of {tactic}`dsimp`.
  * The {keywordOf Lean.Parser.Tactic.simp}`only` modifier excludes the default simp set, instead beginning with an empty{margin}[Technically, the simp set always includes {name}`eq_self` and {name}`iff_self` in order to discharge reflexive cases.] simp set.
@@ -79,20 +153,54 @@ In other words, an invocation of a simplification tactic takes the following mod
       * A mandatory lemma, which can be a simp set name, a lemma name, or a term. Terms are treated as if they were named lemmas with fresh names.
  * A location specifier, preceded by {keywordOf Lean.Parser.Tactic.simp}`at`, which consists of a sequence of locations. Locations may be:
 
+:::
+
+言い換えれば、単純化タクティクの呼び出しは以下の修飾子を順番に取ります。またこれらはすべて任意です：
+ * 呼び出される単純化器が {tactic}`simp` のバージョンか {tactic}`dsimp` のバージョンであるかに応じて、 {name}`Lean.Meta.Simp.Config` か {name}`Lean.Meta.DSimp.Config` のインスタンスでなければなりません。
+ * {keywordOf Lean.Parser.Tactic.simp}`only` 修飾子はデフォルトの simp セットを除外し、代わりに空の {margin}[厳密には、再帰的なケースを除外するために、simp セットは常に {name}`eq_self` と {name}`iff_self` を含みます。] simp セットから開始します。
+ * 補題リストは simp セットに補題を追加したり削除したりします。補題リストで補題を指定する方法は3つあります：
+   * `*`、これは証明状態にあるすべての仮定を simp セットに追加します
+   * `-` に続く補題はその simp セットから取り除かれます
+   * 補題指定子、これは以下の順番で構成されます：
+     * 任意の `↓` または `↑` はそれぞれ部分項を入力する前後に補題を適用します（`↑` がデフォルト）。単純化された引数はより多くの規則を適用できることが多いため、単純化器は通常、親の項を単純化する前に部分項を単純化します；`↓` によって親の項が部分項の単純化よりも優先的に単純化されます。
+     * 任意の `←` は等式の補題を左から右へではなく、右から左へ使うようにします。
+     * 必須の補題で、simp セット名・補題名・項のいずれでも良いです。項はあたかも新しい名前の補題であるかのように扱われます。
+ * {keywordOf Lean.Parser.Tactic.simp}`at` で始まる位置指定子で、これは位置の列から構成されます。位置は次のいずれかになります：
+
+:::comment
    - The name of an assumption, indicating that its type should be simplified
    - An asterisk `*`, indicating that all assumptions and the conclusion should be simplified
    - A turnstile `⊢`, indicating that the conclusion should be simplified
 
+:::
+
+   - 仮定の名前、これはその型が単純化されるべきであることを示します
+   - アスタリスク `*`、すべての仮定と結論が単純化されることを示します
+   - ターンスタイル `⊢`、結論を単純化する必要があることを示します
+
+:::comment
   By default, only the conclusion is simplified.
 
-::::example "Location specifiers for {tactic}`simp`"
-:::tacticExample
+:::
+
+  デフォルトでは結論だけが単純化されます。
+
+:::comment
+::example "Location specifiers for {tactic}`simp`"
+:::
+:::::example "{tactic}`simp` のための位置指定子"
+::::tacticExample
 {goal show:=false}`∀ (p : Nat → Prop) (x : Nat) (h : p (x + 5 + 2)) (h' : p (3 + x + 9)), p (6 + x + 1)`
 ```setup
 intro p x h h'
 ```
 
+:::comment
 In this proof state,
+:::
+
+この証明状態において、
+
 ```pre
 p : Nat → Prop
 x : Nat
@@ -101,8 +209,13 @@ h' : p (3 + x + 9)
 ⊢ p (6 + x + 1)
 ```
 
+:::comment
 the tactic {tacticStep}`simp_arith` simplifies only the goal:
 
+:::
+
+タクティク {tacticStep}`simp_arith` はゴールのみを単純化します：
+
 ```post
 p : Nat → Prop
 x : Nat
@@ -110,9 +223,9 @@ h : p (x + 5 + 2)
 h' : p (3 + x + 9)
 ⊢ p (x + 7)
 ```
-:::
+::::
 
-:::tacticExample
+::::tacticExample
 {goal show:=false}`∀ (p : Nat → Prop) (x : Nat) (h : p (x + 5 + 2)) (h' : p (3 + x + 9)), p (6 + x + 1)`
 ```setup
 intro p x h h'
@@ -125,8 +238,13 @@ h' : p (3 + x + 9)
 ⊢ p (6 + x + 1)
 ```
 
+:::comment
 Invoking {tacticStep}`simp_arith at h` yields a goal in which the hypothesis `h` has been simplified:
 
+:::
+
+{tacticStep}`simp_arith at h` の呼び出しは仮定 `h` が単純化されたゴールを生成します：
+
 ```post
 p : Nat → Prop
 x : Nat
@@ -134,9 +252,9 @@ h' : p (3 + x + 9)
 h : p (x + 7)
 ⊢ p (6 + x + 1)
 ```
-:::
+::::
 
-:::tacticExample
+::::tacticExample
 {goal show:=false}`∀ (p : Nat → Prop) (x : Nat) (h : p (x + 5 + 2)) (h' : p (3 + x + 9)), p (6 + x + 1)`
 ```setup
 intro p x h h'
@@ -149,8 +267,13 @@ h' : p (3 + x + 9)
 ⊢ p (6 + x + 1)
 ```
 
+:::comment
 The conclusion can be additionally simplified by adding `⊢`, that is, {tacticStep}`simp_arith at h ⊢`:
 
+:::
+
+さらに結論を単純化するには `⊢` を追加して {tacticStep}`simp_arith at h ⊢` とすることで可能です：
+
 ```post
 p : Nat → Prop
 x : Nat
@@ -158,9 +281,9 @@ h' : p (3 + x + 9)
 h : p (x + 7)
 ⊢ p (x + 7)
 ```
-:::
+::::
 
-:::tacticExample
+::::tacticExample
 {goal show:=false}`∀ (p : Nat → Prop) (x : Nat) (h : p (x + 5 + 2)) (h' : p (3 + x + 9)), p (6 + x + 1)`
 ```setup
 intro p x h h'
@@ -173,8 +296,13 @@ h' : p (3 + x + 9)
 ⊢ p (6 + x + 1)
 ```
 
+:::comment
 Using {tacticStep}`simp_arith at *` simplifies all assumptions together with the conclusion:
 
+:::
+
+{tacticStep}`simp_arith at *` を使うことで結論を含めすべての仮定が単純化されます：
+
 ```post
 p : Nat → Prop
 x : Nat
@@ -182,26 +310,57 @@ h : p (x + 7)
 h' : p (x + 12)
 ⊢ p (x + 7)
 ```
-:::
 ::::
+:::::
 
 
+:::comment
 # Rewrite Rules
 
+:::
+
+# 書き換え規則（Rewrite Rules）
+
+:::comment
 The simplifier has three kinds of rewrite rules:
 
+:::
+
+単純化器には3種類の書き換え規則があります：
+
+:::comment
 : Declarations to unfold
 
   The simplifier will only unfold {tech}[reducible] definitions by default. However, a rewrite rule can be added for any {tech}[semireducible] or {tech}[irreducible] definition that causes the simplifier to unfold it as well. When the simplifier is running in definitional mode ({tactic}`dsimp` and its variants), definition unfolding only replaces the defined name with its value; otherwise, it also uses the equational lemmas produced by the equation compiler.
 
+:::
+
+: 定義の展開
+
+  単純化器はデフォルトで {tech}[reducible] な定義のみを展開します。しかし、任意の {tech}[semireducible] または {tech}[irreducible] な定義用に書き換え規則を追加して、単純化器が同様にそれらを展開するようにできます。単純化器が定義上モード（ {tactic}`dsimp` とその亜種）で動作している場合、定義の展開は定義された名前をその値で置き換えるだけです；それ以外では、等式のコンパイラから提供された等式の補題も使用します。
+
+:::comment
 : Equational lemmas
 
   The simplifier can treat equality proofs as rewrite rules, in which case the left side of the equality will be replaced with the right. These equational lemmas may have any number of parameters. The simplifier instantiates parameters to make the left side of the equality match the goal, and it performs a proof search to instantiate any additional parameters.
 
+:::
+
+: 等式の補題
+
+  単純化器は等式の証明を書き換え規則として扱うことができ、この場合等式の左辺は右辺に置き換えられます。これらの等式の補題は任意の数のパラメータを持つことができます。単純化器は等式の左辺がゴールに一致するようにパラメータをインスタンス化し、追加のパラメータをインスタンス化するために証明探索を実行します。
+
+:::comment
 : Simplification procedures
 
   The simplifier supports simplification procedures, known as {deftech}_simprocs_, that use Lean metaprogramming to perform rewrites that can't be efficiently specified using equations. Lean includes simprocs for the most important operations on built-in types.
 
+:::
+
+: 単純化手続き
+
+  単純化器は {deftech}_simprocs_ として知られている単純化手続きをサポートしており、Lean メタプログラミングを使用して、等式では効率的に指定できない書き換えを実行します。Lean には組み込み型に対する最も重要な操作のための simproc が含まれています。
+
 :::keepEnv
 ```lean (show := false)
 -- Validate the above description of reducibility
@@ -269,12 +428,20 @@ example : foo'' (x, y) = (y, x) := by
 ```
 :::
 
+:::comment
 Due to {tech}[propositional extensionality], equational lemmas can rewrite propositions to simpler, logically equivalent propositions.
 When the simplifier rewrites a proof goal to {lean}`True`, it automatically closes it.
 As a special case of equational lemmas, propositions other than equality can be tagged as rewrite rules
 They are preprocessed into rules that rewrite the proposition to {lean}`True`.
 
-:::::example "Rewriting Propositions"
+:::
+
+{tech}[propositional extensionality] により、等式の補題は命題をより単純で論理的に等価な補題に書き換えることができます。単純化器が証明のゴールを {lean}`True` に書き換えると、ゴールが自動的に閉じられます。等式の補題の特別なケースとして、等式以外の命題を書き換え規則としてタグ付けすることができます。それらは命題を {lean}`True` に書き換える規則へと前処理されます。
+
+:::comment
+::example "Rewriting Propositions"
+:::
+:::::example "書き換えの命題"
 ::::tacticExample
 
 {goal show:=false}`∀(α β : Type) (w y : α) (x z : β), (w, x) = (y, z)`
@@ -282,7 +449,12 @@ They are preprocessed into rules that rewrite the proposition to {lean}`True`.
 intro α β w y x z
 ```
 
+:::comment
 When asked to simplify an equality of pairs:
+:::
+
+ペアについての等式を単純化することが求められている場合：
+
 ```pre
 α β : Type
 w y : α
@@ -290,8 +462,13 @@ x z : β
 ⊢ (w, x) = (y, z)
 ```
 
+:::comment
 {tacticStep}`simp` yields a conjunction of equalities:
 
+:::
+
+{tacticStep}`simp` は連言の等式を生成します：
+
 ```post
 α β : Type
 w y : α
@@ -299,8 +476,13 @@ x z : β
 ⊢ w = y ∧ x = z
 ```
 
+:::comment
 The default simp set contains {lean}`Prod.mk.injEq`, which shows the equivalence of the two statements:
 
+:::
+
+デフォルトの simp セットには {lean}`Prod.mk.injEq` が含まれており、2つの文の同値性を示しています：
+
 ```signature
 Prod.mk.injEq.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) :
   ∀ (fst_1 : α) (snd_1 : β),
@@ -309,11 +491,22 @@ Prod.mk.injEq.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) :
 ::::
 :::::
 
+:::comment
 In addition to rewrite rules, {tactic}`simp` has a number of built-in reduction rules, {ref "simp-config"}[controlled by the `config` parameter].
 Even when the simp set is empty, {tactic}`simp` can replace `let`-bound variables with their values, reduce {keywordOf Lean.Parser.Term.match}`match` expressions whose scrutinees are constructor applications, reduce structure projections applied to constructors, or apply lambdas to their arguments.
 
+:::
+
+書き換え規則に加え、 {tactic}`simp` は {ref "simp-config"}[`config` パラメータによって制御される] いくつかの組み込みの簡約規則を持っています。simp セットが空の場合でも、 {tactic}`simp` は `let` 束縛変数のその値へに置き換え・場合分け対象がコンストラクタ適用である {keywordOf Lean.Parser.Term.match}`match` 式の簡約・コンストラクタに適用される構造体の射影の簡約・ラムダ式の引数への適用などを行うことができます。
+
+:::comment
 # Simp sets
 
+:::
+
+# simp セット（Simp sets）
+
+:::comment
 A collection of rules used by the simplifier is called a {deftech}_simp set_.
 A simp set is specified in terms of modifications from a _default simp set_.
 These modifications can include adding rules, removing rules, or adding a set of rules.
@@ -321,10 +514,19 @@ The `only` modifier to the {tactic}`simp` tactic causes it to start with an empt
 Rules are added to the default simp set using the {attr}`simp` attribute.
 
 
-:::syntax attr alias := Lean.Meta.simpExtension label:="attribute"
+:::
+
+単純化器が使用する規則のセットを {deftech}_simp セット_ （simp set）と呼びます。simp セットは、_デフォルト simp セット_ （default simp set）への修正の観点において指定が行われます。これらの修正には規則の追加・削除・セットの追加が含まれます。 {tactic}`simp` タクティクに `only` 修飾子を付けると、デフォルト simp セットではなく、空の simp セットから開始します。規則は {attr}`simp` 属性を使ってデフォルト simp セットに追加されます。
+
+::::syntax attr alias := Lean.Meta.simpExtension label:="attribute"
+:::comment
 The {attr}`simp` attribute adds a declaration to the default simp set.
 If the declaration is a definition, the definition is marked for unfolding; if it is a theorem, then the theorem is registered as a rewrite rule.
 
+:::
+
+{attr}`simp` 属性はデフォルト simp セットに宣言を追加します。宣言が定義である場合、その定義は展開用としてマークされます；宣言が定理である場合、その定理は書き換え規則として登録されます。
+
 ```grammar
 simp
 ```
@@ -348,56 +550,114 @@ simp $p:prio
 #guard_msgs in
 #eval eval_prio default
 ```
-:::
+::::
 
-Custom simp sets are created with {name Lean.Meta.registerSimpAttr}`registerSimpAttr`, which must be run during {tech}[初期化]initialization by placing it in an {keywordOf Lean.Parser.Command.initialize}`initialize` block.
+:::comment
+Custom simp sets are created with {name Lean.Meta.registerSimpAttr}`registerSimpAttr`, which must be run during {tech}[initialization] by placing it in an {keywordOf Lean.Parser.Command.initialize}`initialize` block.
 As a side effect, it creates a new attribute with the same interface as {attr}`simp` that adds rules to the custom simp set.
 The returned value is a {name Lean.Meta.SimpExtension}`SimpExtension`, which can be used to programmatically access the contents of the custom simp set.
 The {tactic}`simp` tactics can be instructed to use the new simp set by including its attribute name in the rule list.
 
+:::
+
+カスタム simp セットは {name Lean.Meta.registerSimpAttr}`registerSimpAttr` で作成します。これは {tech}[初期化] 中における {keywordOf Lean.Parser.Command.initialize}`initialize` ブロック内でのみ実行可能です。副次効果として、カスタム simp セットに規則を追加する {attr}`simp` と同じインタフェースを持つ新しい属性を作成します。戻り値は {name Lean.Meta.SimpExtension}`SimpExtension` で、プログラムにてカスタム simp セットの内容にアクセスするために使用できます。 {tactic}`simp` タクティクは規則のリストにその属性名を含めることで新しい simp セットを使用するとうに指示できます。
+
 {docstring Lean.Meta.registerSimpAttr}
 
 {docstring Lean.Meta.SimpExtension}
 
 
 
+:::comment
 # Simp Normal Forms
 
+:::
+
+# simp 正規形（Simp Normal Forms）
+
+:::comment
 The default {tech}[simp set] contains all the theorems and simplification procedures marked with the {attr}`simp` attribute.
 The {deftech}_simp normal form_ of an expression is the result of applying the default simp set via the {tactic}`simp` tactic until no more rules can be applied.
 When an expression is in simp normal form, it is as reduced as possible according to the default simp set, often making it easier to work with in proofs.
 
+:::
+
+デフォルト {tech}[simp セット] には {attr}`simp` でマークされたすべての定理と単純化手続きが含まれます。式の {deftech}_simp 正規形_ （simp normal form）は、 {tactic}`simp` タクティクによってデフォルトの simp セットを適用できる規則がなくなるまで適用した結果です。式が simp 正規形であると、デフォルト simp セットに従って可能な限り簡約されているため、多くの場合証明で作業しやすくなります。
+
+:::comment
 The {tactic}`simp` tactic *does not guarantee confluence*, which means that the simp normal form of an expression may depend on the order in which the elements of the default simp set are applied.
 The order in which the rules are applied can be changed by assigning priorities when setting the {attr}`simp` attribute.
 
+:::
+
+{tactic}`simp` タクティクは *合流性を保証しません* 。つまり式の simp 正規形はデフォルト simp セットの要素が適用される順番に依存する可能性があります。 {attr}`simp` 属性を設定する際に優先度を割り当てることで規則の適用順序を変更することができます。
+
+:::comment
 When designing a Lean library, it's important to think about what the appropriate simp normal form for the various combinations of the library's operators is.
 This can serve as a guide when selecting which rules the library should add to the default simp set.
 In particular, the right-hand side of simp lemmas should be in simp normal form; this helps ensure that simplification terminates.
 Additionally, each concept in the library should be expressed through one simp normal form, even if there are multiple equivalent ways to state it.
 If a concept is stated in two different ways in different simp lemmas, then some desired simplifications may not occur because the simplifier does not connect them.
 
+:::
+
+Lean ライブラリを設計する際には、ライブラリの演算子の様々な組み合わせに対して適切な simp 正規形とは何かを考えることが重要です。これはライブラリがデフォルト simp セットに追加するべき規則を選択する際の指針になります。特に、simp の補題の右辺は simp 正規形であるべきです；これによって単純化が停止することの保証が促進されます。さらに、ライブラリの各概念はたとえ等価な表現方法が複数あったとしても、1つの simp 正規形を通して表現されるべきです。ある概念が異なる simp の補題で2つの異なる方法で記述されている場合、単純化器がそれらを結び付けずに望ましい単純化が行われないことがあります。
+
+:::comment
 Even though simplification doesn't need to be confluent, striving for confluence is helpful because it makes the library more predictable and tends to reveal missing or poorly chosen simp lemmas.
 The default simp set is as much a part of a library's interface as the type signatures of the constants that it exports.
 
+:::
+
+単純化では必ずしも合流性を満たす必要はありませんが、合流性に近づけようとすることはライブラリをより予測しやすくし、simp の補題の欠落や不適切な選択を明らかにする傾向があるため有益です。デフォルト simp セットはライブラリがエクスポートする定数の型シグネチャと同様に、ライブラリのインタフェースの一部です。
+
+:::comment
 Libraries should not add rules to the default simp set that don't mention at least one constant defined in the library.
 Otherwise, importing a library could change the behavior of {tactic}`simp` for some unrelated library.
 If a library relies on additional simplification rules for definitions or declarations from other libraries, please create a custom simp set and either instruct users to use it or provide a dedicated tactic.
 
 
+:::
+
+ライブラリは、そのライブラリで定義されている少なくとも1つの定数に言及しない規則をデフォルト simp セットに追加すべきではありません。そうでなければ、ライブラリをインポートすることで無関係なライブラリの {tactic}`simp` の挙動が変わってしまう可能性があります。ライブラリが他のライブラリからの定義や宣言に対する追加の単純化規則に依存している場合、カスタム simp セットを作成し、それを使用するようにユーザに指示するか、専用のタクティクを提供してください。
+
+:::comment
 # Terminal vs Non-Terminal Positions
 
+:::
+
+# 終端・非終端位置（Terminal vs Non-Terminal Positions）
+
+:::comment
 To write maintainable proofs, avoid using {tactic}`simp` without {keywordOf Lean.Parser.Tactic.simp}`only` unless it closes the goal.
 Such uses of {tactic}`simp` that do not close a goal are referred to as {deftech}_non-terminal simps_.
 This is because additions to the default simp set may make {tactic}`simp` more powerful or just cause it to select a different sequence of rewrites and arrive at a different simp normal form.
 When {keywordOf Lean.Parser.Tactic.simp}`only` is specified, additional lemmas will not affect that invocation of the tactic.
 In practice, terminal uses of {tactic}`simp` are not nearly as likely to be broken by the addition of new simp lemmas, and when they are, it's easier to understand the issue and fix it.
 
+:::
+
+メンテナンス可能な証明を書くためには、 {keywordOf Lean.Parser.Tactic.simp}`only` を伴わない {tactic}`simp` の使用はゴールを閉じない限り避けてください。ゴールを閉じない {tactic}`simp` のこのような使用は {deftech}_非終端 simp_ （non-terminal simp）と呼ばれます。これはデフォルト simp セットに追加することで、 {tactic}`simp` がより強力になったり、単に異なる書き換えシーケンスを選択し、異なる simp 正規形に到達する可能性があるからです。 {keywordOf Lean.Parser.Tactic.simp}`only` が指定されている場合、追加の補題はタクティクのその呼び出しに影響しません。実際には {tactic}`simp` の終端位置での使用は、新しい simp の補題の追加によって壊れる可能性はほとんどなく、壊れた場合も問題の理解と修正は容易です。
+
+:::comment
 When working in non-terminal positions, {tactic}`simp?` (or one of the other simplification tactics with `?` in their names) can be used to generate an appropriate invocation with{keywordOf Lean.Parser.Tactic.simp}`only`.
 Just as {tactic}`apply?` or {tactic}`rw?` suggest the use of relevant lemmas, {tactic}`simp?` suggests an invocation of {tactic}`simp` with a minimal simp set that was used to reach the normal form.
 
-:::example "Using {tactic}`simp?`"
+:::
+
+非終端位置で作業する場合、 {tactic}`simp?` （または名前に `?` を持つ他の単純化タクティクのいずれか）を使用して、 {keywordOf Lean.Parser.Tactic.simp}`only` で適切な呼び出しを生成することができます。ちょうど {tactic}`apply?` や {tactic}`rw?` が関連する補題の使用を提案するように、 {tactic}`simp?` は正規形に到達するために使用された最小の simp セットでの {tactic}`simp` の呼び出しを提案します。
 
+:::comment
+::example "Using {tactic}`simp?`"
+:::
+::::example "{tactic}`simp?` の使用"
+
+:::comment
 The non-terminal {tactic}`simp?` in this proof suggests a smaller {tactic}`simp` with {keywordOf Lean.Parser.Tactic.simp}`only`:
+:::
+
+この証明における非終端位置での {tactic}`simp?` は {keywordOf Lean.Parser.Tactic.simp}`only` を伴ったより小さい {tactic}`simp` を示唆します：
+
 ```lean (name:=simpHuhDemo)
 example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by
   intros
@@ -405,11 +665,21 @@ example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by
   simp?
   assumption
 ```
+:::comment
 The suggested rewrite is:
+:::
+
+
+
 ```leanOutput simpHuhDemo
 Try this: simp only [Array.size_toArray, List.length_cons, List.length_singleton, Nat.reduceAdd]
 ```
+:::comment
 which results in the more maintainable proof:
+:::
+
+これはよりメンテナンス可能な証明になります：
+
 ```lean
 example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by
   intros
@@ -418,26 +688,46 @@ example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by
   assumption
 ```
 
-:::
+::::
 
 
+:::comment
 # Configuring Simplification
+:::
+
+# 単純化の設定（Configuring Simplification）
+
 %%%
 tag := "simp-config"
 %%%
 
+:::comment
 {tactic}`simp` is primarily configured via a configuration parameter, passed as a named argument called `config`.
 
+:::
+
+{tactic}`simp` は主に `config` という名前対の引数として渡される設定パラメータによって設定されます。
+
 {docstring Lean.Meta.Simp.Config}
 
 {docstring Lean.Meta.Simp.neutralConfig}
 
 {docstring Lean.Meta.DSimp.Config}
 
+:::comment
 ## Options
 
+:::
+
+## オプション（Options）
+
+:::comment
 Some global options affect {tactic}`simp`:
 
+:::
+
+いくつかのグローバルオプションが {tactic}`simp` に影響します：
+
 {optionDocs simprocs}
 
 {optionDocs tactic.simp.trace}
@@ -448,8 +738,14 @@ Some global options affect {tactic}`simp`:
 
 {optionDocs trace.Meta.Tactic.simp.discharge}
 
+:::comment
 # Simplification vs Rewriting
 
+:::
+
+# 単純化と書き換え（Simplification vs Rewriting）
+
+:::comment
 Both {tactic}`simp` and {tactic}`rw`/{tactic}`rewrite` use equational lemmas to replace parts of terms with equivalent alternatives.
 Their intended uses and their rewriting strategies differ, however.
 Tactics in the {tactic}`simp` family are primarily used to reformulate a problem in a standardized way, making it more amenable to both human understanding and further automation.
@@ -457,7 +753,15 @@ In particular, simplification should never render an otherwise-provable goal imp
 Tactics in the {tactic}`rw` family are primarily used to apply hand-selected transformations that do not always preserve provability nor place terms in standardized forms.
 These different emphases are reflected in the differences of behavior between the two families of tactics.
 
+:::
+
+{tactic}`simp` と {tactic}`rw` ・ {tactic}`rewrite` はどちらも等式の補題を使用して、項の一部を同値な代替の項に置き換えます。しかし、それらの意図された用途と書き換え戦略は異なります。 {tactic}`simp` の族のタクティクは、主に標準化された方法で問題を再定式化するために使用され、人間の理解とさらなる自動化の両方に供します。特に、単純化することで、他に証明可能なゴールが不可能になるようなことがあってはなりません。 {tactic}`rw` の族のタクティクは主に手作業で選択された変換を適用するために使用されます。これは証明可能性を常に保持したり、項を標準化された形式に配置したりしません。これらの異なる強調点は、2つのタクティクの族の動作の違いに反映されています。
+
+:::comment
 The {tactic}`simp` tactics primarily rewrite from the inside out.
 The smallest possible expressions are simplified first so that they can unlock further simplification opportunities for the surrounding expressions.
 The {tactic}`rw` tactics select the leftmost outermost subterm that matches the pattern, rewriting it a single time.
 Both tactics allow their strategy to be overridden: when adding a lemma to a simp set, the `↓` modifier causes it to be applied prior to the simplification of subterms, and the {name Lean.Meta.Rewrite.Config.occs}`occs` field of {tactic}`rw`'s configuration parameter allows a different occurrence to be selected, either via a whitelist or a blacklist.
+:::
+
+{tactic}`simp` タクティクは主に内側から外側へ書き換えます。可能な限り小さい式が最初に単純化され、周囲の式のさらなる単純化の機会を解放します。 {tactic}`rw` タクティクは、パターンにマッチする最も左の外側の部分項を選択し、それを1回だけ書き換えます。どちらのタクティクもその戦略を上書きすることができます：simp セットに補題を追加するとき、`↓` 修飾子は部分項の単純化の前に適用されるようにし、 {tactic}`rw` の設定パラメータの {name Lean.Meta.Rewrite.Config.occs}`occs` フィールドは複数の出現に対してホワイトリストかブラックリストのいずれかの選択を可能にします。
diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean
index b3a0511..8108f58 100644
--- a/Manual/Tactics/Reference.lean
+++ b/Manual/Tactics/Reference.lean
@@ -431,7 +431,7 @@ Try this: exact Nat.lt_trans h1 h2
 
 :::
 
-# 決定処理（Decision Procedures）
+# 決定手続き（Decision Procedures）
 
 :::tactic Lean.Parser.Tactic.decide show:="decide"
 :::