转换策略模式

在策略块中，可以使用关键字conv进入转换模式(conversion mode)。这种模式允许在假设和目标内部，甚至在函数抽象和依赖箭头内部移动，以应用重写或简化步骤。

基本导航和重写

作为第一个例子，让我们证明(a b c : Nat) : a * (b * c) = a * (c * b)（本段中的例子有些刻意设计，因为其他策略可以立即完成它们）。首次简单的尝试是尝试rw [Nat.mul_comm]，但这将目标转化为b * c * a = a * (c * b)，因为它作用于项中出现的第一个乘法。有几种方法可以解决这个问题，其中一个方法是

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
    rw [Nat.mul_comm b c]

不过本节介绍一个更精确的工具：转换模式。下面的代码块显示了每行之后的当前目标。

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
  conv =>
    -- ⊢ a * (b * c) = a * (c * b)
    lhs
    -- ⊢ a * (b * c)
    congr
    -- 2 goals: ⊢ a, ⊢ b * c
    rfl
    -- ⊢ b * c
    rw [Nat.mul_comm]

上面这段涉及三个导航指令：

• lhs（left hand side）导航到关系（此处是等式）左边。同理rhs导航到右边。
• congr创建与当前头函数的(非依赖的和显式的)参数数量一样多的目标（此处的头函数是乘法）。
• skip走到下一个目标。

一旦到达相关目标，我们就可以像在普通策略模式中一样使用rw。

使用转换模式的第二个主要原因是在约束器下重写。假设我们想证明(fun x : Nat => 0 + x) = (fun x => x)。首次简单的尝试rw [zero_add]是失败的。报错：

error: tactic 'rewrite' failed, did not find instance of the pattern
       in the target expression
  0 + ?n
⊢ (fun x => 0 + x) = fun x => x

（错误：'rewrite'策略失败了，没有找到目标表达式中的模式0 + ?n）

解决方案为：

example : (fun x : Nat => 0 + x) = (fun x => x) := by
  conv =>
    lhs
    intro x
    rw [Nat.zero_add]

其中intro x是导航命令，它进入了fun约束器。这个例子有点刻意，你也可以这样做：

example : (fun x : Nat => 0 + x) = (fun x => x) := by
  funext x; rw [Nat.zero_add]

或者这样：

example : (fun x : Nat => 0 + x) = (fun x => x) := by
  simp

所有这些也可以用conv at h从局部上下文重写一个假设h。

模式匹配

使用上面的命令进行导航可能很无聊。使用下面的模式匹配来简化它：

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
  conv in b * c => rw [Nat.mul_comm]

这是下面代码的语法糖：

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
  conv =>
    pattern b * c
    rw [Nat.mul_comm]

当然也可以用通配符：

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
  conv in _ * c => rw [Nat.mul_comm]

结构化转换策略

大括号和.也可以在conv模式下用于结构化策略。

example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by
  conv =>
    lhs
    congr
    . rw [Nat.zero_add]
    . rw [Nat.mul_comm]

转换模式中的其他策略

• arg i进入一个应用的第i个非独立显式参数。

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
  conv =>
    -- ⊢ a * (b * c) = a * (c * b)
    lhs
    -- ⊢ a * (b * c)
    arg 2
    -- ⊢ b * c
    rw [Nat.mul_comm]

• args是congr的替代品。

• simp将简化器应用于当前目标。它支持常规策略模式中的相同选项。

def f (x : Nat) :=
  if x > 0 then x + 1 else x + 2

example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by
  conv =>
    rhs
    simp [f, h₂]
  exact h₁

• enter [1, x, 2, y]是arg和intro使用给定参数的宏。

syntax enterArg := ident <|> group("@"? num)
syntax "enter " "[" (colGt enterArg),+ "]": conv
macro_rules
  | `(conv| enter [$i:num]) => `(conv| arg $i)
  | `(conv| enter [@$i:num]) => `(conv| arg @$i)
  | `(conv| enter [$id:ident]) => `(conv| ext $id)
  | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))

• done会失败如果有未解决的目标。

• traceState显示当前策略状态。

• whnf put term in weak head normal form.

• tactic => <tactic sequence>回到常规策略模式。这对于退出conv模式不支持的目标，以及应用自定义的一致性和扩展性引理很有用。

example (g : Nat → Nat → Nat)
        (h₁ : ∀ x, x ≠ 0 → g x x = 1)
        (h₂ : x ≠ 0)
        : g x x + x = 1 + x := by
  conv =>
    lhs
    -- ⊢ g x x + x
    arg 1
    -- ⊢ g x x
    rw [h₁]
    -- 2 goals: ⊢ 1, ⊢ x ≠ 0
    . skip
    . tactic => exact h₂

• apply <term>是tactic => apply <term>的语法糖。

example (g : Nat → Nat → Nat)
        (h₁ : ∀ x, x ≠ 0 → g x x = 1)
        (h₂ : x ≠ 0)
        : g x x + x = 1 + x := by
  conv =>
    lhs
    arg 1
    rw [h₁]
    . skip
    . apply h₂