`conv => ...` 允许用户聚焦特定子表达式，从而对目标或假设执行定向重写。更多详情请参阅 https://lean-lang.org/theorem_proving_in_lean4/conv.html 。 基本形式： * `conv => cs` 使用 `conv` 策略 `cs` 重写目标。 * `conv at h => cs` 重写假设 `h`。 * `conv in pat => cs` 重写第一个匹配 `pat` 的子表达式（参见 `pattern`）。
14.6. 使用 conv 定向重写
conv（即转换）策略允许在目标内进行定向重写。
conv 的参数以一种与主策略语言互操作的独立语言编写；它既提供在目标内导航到特定子项的命令，也提供重写这些子项的命令。
当重写只应应用于目标的一部分（例如只应用于等式的一侧）而非全局应用时，或者重写应在某个绑定器之下进行、因而 rw 等策略无法访问该项时，conv 很有用。
转换策略语言与主策略语言非常相似：二者使用相同的证明状态；策略主要作用于主目标，并且可能失败，也可能成功并产生一系列新目标；宏展开与策略执行交错进行。
主策略语言中的策略旨在最终解决目标；与之不同，conv 策略用于改变目标，使其适合由主策略语言进一步处理。
准备使用 conv 重写的目标会以竖线而非推导符显示。
使用 conv 导航并重写
在此示例中，加法出现了多次，而 rw 默认会重写它遇到的第一个实例。
先使用 conv 导航到特定子项再进行重写，rw 就只能重写正确的项。
example (x y z : Nat) : x + (y + z) = (x + z) + y := x:Naty:Natz:Nat⊢ x + (y + z) = x + z + y
x:Naty:Natz:Nat| x + (y + z) = x + z + y
x:Naty:Natz:Nat| x + (y + z)
x:Naty:Natz:Nat| y + z
x:Naty:Natz:Nat| z + y
All goals completed! 🐙
使用 conv 在绑定器下重写
在此示例中，加法位于绑定器之下，因此不能使用 rw。
不过，在使用 conv 导航到函数体之后，重写便会成功。
嵌套使用 conv 会在对当前项的某个子项执行进一步转换之后，让控制返回该项中的当前位置。
由于重写后的目标是自反等式，conv 会自动将其关闭。
example :
(fun (x y z : Nat) =>
x + (y + z))
=
(fun x y z =>
(z + x) + y)
:= ⊢ (fun x y z => x + (y + z)) = fun x y z => z + x + y
| (fun x y z => x + (y + z)) = fun x y z => z + x + y
| fun x y z => x + (y + z)
x:Naty:Natz:Nat| x + (y + z)
conv =>
x:Naty:Natz:Nat| y + z
x:Naty:Natz:Nat| z + y
x:Naty:Natz:Nat| x + z + y
x:Naty:Natz:Nat| x + z
x:Naty:Natz:Nat| z + x
14.6.1. 控制结构
14.6.2. 目标选择
conv 策略
case ... => ...
`case tag => tac` 聚焦于分支名为 `tag` 的目标，并使用 `tac` 求解它，否则失败。`case tag x₁ ... xₙ => tac` 还会把最近的 `n` 个具有不可访问名称的假设重命名为给定名称。`case tag₁ | tag₂ => tac` 等价于 `( case tag₁ => tac ) ; ( case tag₂ => tac )`。
conv 策略
case' ... => ...
`case'` 与 `case tag => tac` 策略类似，但它既不确保应用 `tac` 后目标已经解决，也不会在 `tac` 失败时承认该目标。回想一下，当 `tac` 失败时，`case` 会使用 `sorry` 关闭目标，并且不会中断策略执行。
conv 策略
next ... => ...
`next => tac` 聚焦下一个目标并使用 `tac` 解决它，否则失败。 `next x₁ ... xₙ => tac` 还会使用给定名称，重命名最近引入的 `n` 个具有不可访问名称的假设。
14.6.3. 导航
conv 策略
arg [@]i
`arg i` 遍历进入目标的第 `i` 个实参。例如，若目标为 `f a b c d`，则 `arg 1` 遍历进入 `a`，而 `arg 3` 遍历进入 `c`。 索引可以为负数；`arg - 1` 遍历进入最后一个实参，`arg - 2` 遍历进入倒数第二个实参，依此类推。 `arg @ i` 与 `arg i` 相同，但它对所有实参计数，而非只对显式实参计数。 `arg 0` 遍历进入函数。若目标为 `f a b c d`，则 `arg 0` 遍历进入 `f`。
语法
enter 的参数`enterArg ::= ... | num enterArg ::= ... | @ num enterArg ::= ... | `binderIdent`` 匹配一个 `ident` 或 `_`。它用于绑定位置中的标识符，其中 `_` 表示该值应保持匿名且不可访问。`ident`
conv 策略
enter
`enter [ arg , ... ]` 是描述通向子项的路径的紧凑方式。它是其他 `conv` 策略的如下简写： * `enter [ i ]` 等价于 `arg i`。 * `enter [ @ i ]` 等价于 `arg @ i`。 * `enter [ x ]`（其中 `x` 是标识符）等价于 `ext x`。 * `enter [ in e ]`（其中 `e` 是项）等价于 `pattern e`。 可以用 `enter [ in ( occs := ... ) e ]` 指定出现位置。例如，给定目标式 `f ( g a ( fun x => x b ) )`，`enter [ 1 , 2 , x , 1 ]` 会遍历至子项 `b`。
conv 策略
pattern
`pattern pat` 遍历到目标中第一个与 `pat` 匹配的子项。`pattern ( occs := * ) pat` 遍历到目标中每个与 `pat` 匹配且不包含在另一个 `pat` 匹配中的子项。它为每个匹配的子项生成一个子目标。 `pattern ( occs := 1 2 4 ) pat` 匹配 `pat` 的第 `1`、`2`、`4` 次出现，并产生三个子目标。出现位置按从左到右、由外向内的顺序编号。 请注意，跳过 `pat` 的某次出现后，会继续遍历该子表达式内部；这意味着可能找到更多匹配，并影响后续模式匹配的编号。 例如，在 `f ( f a ) = f b` 中搜索 `f _` 时： - `occs := 1 2`（以及 `occs := *`）返回 `| f ( f a )` 和 `| f b`； - `occs := 2` 返回 `| f a`； - `occs := 2 3` 返回 `| f a` 和 `| f b`； - `occs := 1 3` 会报错，因为跳过 `f b` 后不存在第三个匹配。
14.6.4. 改变目标
14.6.4.1. 归约
conv 策略
cbv
`cbv` 执行与按值求值非常相似的化简。它通过使用定义方程展开定义并应用匹配器方程来归约目标项。展开是命题式的，因此 `cbv` 也适用于通过良基递归或部分不动点定义的函数。 `cbv` 生成的证明只使用三个标准公理。特别是，它们无需信任代码生成器的正确性。
cbv 策略
conv 策略
whnf
把目标式约简为弱头范式。它会约简处于“头部位置”的定义，直到暴露出构造器。例如，`List.map f [ a , b , c ]` 的弱头规范化结果是 `f a :: List.map f [ b , c ]`。
conv 策略
delta
`delta id1 id2 ...` 展开目标式中 `id1`、`id2` 等的所有出现位置。与 `delta` 策略一样，它忽略任何定义方程，改用原始 delta 约简，这可能泄露实现细节。用户应优先使用 `unfold` 来展开定义。
conv 策略
unfold
`unfold id` 展开目标式中定义 `id` 的所有出现位置。`unfold id1 id2 ...` 等价于 `unfold id1 ; unfold id2 ; ...`。定义既可以是全局定义，也可以是局部定义。 对于非递归全局定义，此策略与 `delta` 相同。对于递归全局定义，它使用为每个递归定义生成的“展开引理”`id.eq_def`，按照用户给出的递归定义进行展开。它只执行一层展开；与之相对，`simp only [ id ]` 会递归地展开定义 `id`。 这是 `unfold` 策略的 `conv` 版本。
14.6.4.2. 化简
conv 策略
dsimp
`dsimp` 是 `conv` 模式中的定义化简器。它与 `simp` 的区别是只应用通过自反性成立的定理。 示例： example ( a : Nat ) : ( 0 + 0 ) = a - a := by a : Nat ⊢ 0 + 0 = a - a conv => a : Nat | 0 + 0 = a - a lhs a : Nat | 0 + 0 dsimp a : Nat | 0 rw [ ← Nat.sub_self a ] a : Nat | a - a
conv 策略
simp_match
`simp_match` 化简 `match` 表达式。例如，`match [ a , b ] with | [ ] => 0 | hd :: tl => hd` 化简为 `a`。
14.6.4.3. 重写
conv 策略
erw
`erw [ rules ]` 是 `rw ( transparency := .default ) [ rules ]` 的简写。它进行重写时可展开普通定义；相比之下，普通 `rw` 只展开带有 `@[ reducible ]` 标记的定义。
conv 策略
apply
`conv` 策略 `apply thm` 与普通策略 `apply thm` 相同。对 `thm` 没有限制，但如果无法合理地把 `thm` 解释为从一系列其他等式证明一个等式，可能会产生奇怪的结果。
14.6.5. 嵌套策略
策略
conv'执行给定的 `conv` 块，但不把普通目标转换为 `conv` 目标。
策略
conv'执行给定的 `conv` 块，但不把普通目标转换为 `conv` 目标。