15.2. 重写规则🔗

简化器具有三种重写规则：

待展开的宣言

默认情况下，简化器只会展开 reducible 定义。 但是，可以为任何 半可约 或 不可约 定义添加重写规则，这也会导致简化器展开它。 当简化器在定义模式（dsimp 及其变体）下运行时，定义展开仅用其值替换定义的名称；否则，它还使用方程编译器生成的方程引理。

方程引理

简化器可以将等式证明视为重写规则，在这种情况下等式的左侧将被右侧替换。这些等式引理可以具有任意数量的参数。简化器实例化参数以使等式的左侧与目标匹配，并执行证明搜索以实例化任何其他参数。

简化程序

该简化器支持称为 simprocs 的简化过程，该过程使用 Lean 元编程来执行无法使用方程有效指定的重写。 Lean 包括用于内置类型上最重要操作的 simprocs。

由于 命题外延性，等式引理可以将命题重写为更简单、逻辑上等价的命题。 当简化器将证明目标重写为 True 时，它会自动关闭它。 作为等式引理的特例，等式以外的命题可以被标记为重写规则 它们被预处理成规则，将命题重写为 True。

除了重写规则之外，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 表达式，减少应用于构造函数的结构投影，或将 lambda 应用于其参数。