15.2. 重写规则🔗

简化器有三类重写规则：

要展开的声明

默认情况下，简化器只展开可约定义。 不过，可以为任意半可约或不可约定义添加重写规则，使简化器也展开该定义。 当简化器以定义模式（dsimp 及其变体）运行时，定义展开只会用定义的值替换定义名称；否则，它还会使用等式编译器产生的等式引理。

等式引理

简化器可以将相等性证明视为重写规则，此时等式左侧会被右侧替换。这些等式引理可以有任意数量的参数。简化器会实例化参数，使等式左侧与目标匹配，并通过证明搜索实例化任何额外参数。

简化过程

简化器支持称为 simproc 的简化过程。它们利用 Lean 元编程执行无法用等式高效指定的重写。Lean 为内置类型上最重要的操作提供了简化过程。

借助命题外延性，等式引理可以把命题重写为逻辑等价且更简单的命题。 当简化器把证明目标重写为 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 表达式、归约应用于构造器的结构投影，或把匿名函数应用于其参数。