8.2. 書き換え規則（Rewrite Rules）
単純化器には3種類の書き換え規則があります：
- 定義の展開
単純化器はデフォルトで reducible な定義のみを展開します。しかし、任意の semi-reducible または irreducible な定義用に書き換え規則を追加して、単純化器が同様にそれらを展開するようにできます。単純化器が定義上モード（
dsimpとその亜種）で動作している場合、定義の展開は定義された名前をその値で置き換えるだけです；それ以外では、等式のコンパイラから提供された等式の補題も使用します。
- 等式の補題
単純化器は等式の証明を書き換え規則として扱うことができ、この場合等式の左辺は右辺に置き換えられます。これらの等式の補題は任意の数のパラメータを持つことができます。単純化器は等式の左辺がゴールに一致するようにパラメータをインスタンス化し、追加のパラメータをインスタンス化するために証明探索を実行します。
- 単純化手続き
単純化器は simprocs として知られている単純化手続きをサポートしており、Lean メタプログラミングを使用して、等式では効率的に指定できない書き換えを実行します。Lean には組み込み型に対する最も重要な操作のための simproc が含まれています。
propositional extensionality により、等式の補題は命題をより単純で論理的に等価な補題に書き換えることができます。単純化器が証明のゴールを True に書き換えると、ゴールが自動的に閉じられます。等式の補題の特別なケースとして、等式以外の命題を書き換え規則としてタグ付けすることができます。それらは命題を True に書き換える規則へと前処理されます。
書き換えの命題
ペアについての等式を単純化することが求められている場合：
α:Typeβ:Typew:αy:αx:βz:β⊢ w = y ∧ x = z は連言の等式を生成します：
デフォルトの simp セットには Prod.mk.injEq が含まれており、2つの文の同値性を示しています：
Prod.mk.injEq.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) :
∀ (fst_1 : α) (snd_1 : β),
((fst, snd) = (fst_1, snd_1)) = (fst = fst_1 ∧ snd = snd_1)
書き換え規則に加え、 simp は config パラメータによって制御される いくつかの組み込みの簡約規則を持っています。simp セットが空の場合でも、 simp は let 束縛変数のその値へに置き換え・場合分け対象がコンストラクタ適用である Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 式の簡約・コンストラクタに適用される構造体の射影の簡約・ラムダ式の引数への適用などを行うことができます。