11. 转换策略模式🔗

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

作为第一个例子，让我们证明 (a b c : Nat) : a * (b * c) = a * (c * b)（本段中的例子有些刻意设计，因为其他策略可以立即完成它们）。首次简单的尝试是进入策略模式并尝试 rw [Nat.mul_comm]。但这将目标转化为 b * c * a = a * (c * b)，因为它作用于项中出现的第一个乘法。有几种方法可以解决这个问题，其中一个方法是使用更精确的工具：转换模式。下面的代码块显示了每行之后的当前目标。

                #guard_msgs (drop all) in
example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b)
  rw [Nat.mul_comm]a:Natb:Natc:Nat⊢ b * c * a = a * (c * b)

example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b)
  conv =>a:Natb:Natc:Nat| a * (b * c) = a * (c * b)
    lhsa:Natb:Natc:Nat| a * (b * c)
    congraa:Natb:Natc:Nat| aaa:Natb:Natc:Nat| b * c
    rflaa:Natb:Natc:Nat| b * c
    rw [Nat.mul_comm]aa:Natb:Natc:Nat| c * b

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

lhs 导航到关系（此处是等式）左边。同理 rhs 导航到右边。
congr 创建与当前头函数的（非依赖的和显式的）参数数量一样多的目标（此处的头函数是乘法）。
rfl 使用自反性关闭目标。

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

使用转换模式的第二个主要原因是在约束器下重写。假设我们想证明 (fun x : Nat => 0 + x) = (fun x => x)。首次简单的尝试是进入策略模式并尝试 rw [Nat.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

解决方案为：

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

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

example : (fun x : Nat => 0 + x) = (fun x => x) := by⊢ (fun x => 0 + x) = fun x => x
  funext xhx:Nat⊢ 0 + x = x; rw [Nat.zero_add]All goals completed! 🐙

或者这样：

example : (fun x : Nat => 0 + x) = (fun x => x) := by⊢ (fun x => 0 + x) = fun x => x
  simpAll goals completed! 🐙

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

11.2. 模式匹配🔗

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

example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b)
  conv in b * c =>a:Natb:Natc:Nat| b * c
    rw [Nat.mul_comm]a:Natb:Natc:Nat| c * b

这是下面代码的语法糖：

example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b)
  conv =>a:Natb:Natc:Nat| a * (b * c) = a * (c * b)
    pattern b * ca:Natb:Natc:Nat| b * c
    rw [Nat.mul_comm]a:Natb:Natc:Nat| c * b

当然也可以用通配符：

example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b)
  conv in _ * c =>a:Natb:Natc:Nat| b * c rw [Nat.mul_comm]a:Natb:Natc:Nat| c * b

11.3. 结构化转换策略🔗

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

example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ (0 + a) * (b * c) = a * (c * b)
  conv =>a:Natb:Natc:Nat| (0 + a) * (b * c) = a * (c * b)
    lhsa:Natb:Natc:Nat| (0 + a) * (b * c)
    congraa:Natb:Natc:Nat| 0 + aaa:Natb:Natc:Nat| b * c
    . rw [Nat.zero_add]aa:Natb:Natc:Nat| a
    . rw [Nat.mul_comm]aa:Natb:Natc:Nat| c * b

11.4. 转换模式中的其他策略🔗

arg i 进入一个应用的第 i 个非依赖显式参数。

example (a b c : Nat) : a * (b * c) = a * (c * b) := bya:Natb:Natc:Nat⊢ a * (b * c) = a * (c * b) conv =>a:Natb:Natc:Nat| a * (b * c) = a * (c * b) lhsa:Natb:Natc:Nat| a * (b * c) arg 2a:Natb:Natc:Nat| b * c rw [Nat.mul_comm]a:Natb:Natc:Nat| c * b

args 是 congr 的替代名称。

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

def f (x : Nat) := if x > 0 then x + 1 else x + 2example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := byx:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0⊢ g x = f x conv =>x:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| g x = f x rhsx:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| f x simp [f, h₂]x:Natg:Nat → Nath₁:g x = x + 1h₂:x > 0| x + 1 exact h₁All goals completed! 🐙

enter [1, x, 2, y] 使用给定参数迭代 arg 和 intro。

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

trace_state 显示当前策略状态。

whnf 将项置于弱首范式（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 := byx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ g x x + x = 1 + x conv =>x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x = 1 + x lhsx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x arg 1x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x rw [h₁]x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 . skipx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1 . tactic =>ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 exact h₂All goals completed! 🐙

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 := byx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ g x x + x = 1 + x conv =>x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x = 1 + x lhsx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x + x arg 1x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| g x x rw [h₁]x:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1ax:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0⊢ x ≠ 0 . skipx:Natg:Nat → Nat → Nath₁:∀ (x : Nat), x ≠ 0 → g x x = 1h₂:x ≠ 0| 1 . apply h₂All goals completed! 🐙

Lean 4 定理证明

11. 转换策略模式🔗

11.1. 基本导航和重写🔗

11.2. 模式匹配🔗

11.3. 结构化转换策略🔗

11.4. 转换模式中的其他策略🔗