11.1. 基本导航与重写11.1. Basic navigation and rewriting🔗

作为第一个例子，让我们证明示例 (a b c : Nat) : a * (b * c) = a * (c * b) （此文件中的示例有些人为设计，因为 其他策略可以立即完成它们）。最直接 的首次尝试是进入策略模式并尝试 rw [Nat.mul_comm]。但这会将目标变换为 b * c * a = a * (c * b)，在交换了项中出现的 第一个乘法之后。有多种 方法可以解决此问题，其中一种方法是使用更精确的工具： 转换模式。以下代码块显示了每一行之后的当前目标。As a first example, let us prove example (a b c : Nat) : a * (b * c) = a * (c * b) (examples in this file are somewhat artificial since other tactics could finish them immediately). The naive first attempt is to enter tactic mode and try rw [Nat.mul_comm]. But this transforms the goal into b * c * a = a * (c * b), after commuting the very first multiplication appearing in the term. There are several ways to fix this issue, and one way is to use a more precise tool: the conversion mode. The following code block shows the current target after each line.

以上代码片段展示了三个导航命令：The above snippet shows three navigation commands:

• lhs 导航到关系（此处为等式）的左侧。 还有 rhs 用于导航到右侧。lhs navigates to the left-hand side of a relation (equality, in this case). There is also a rhs to navigate to the right-hand side.

• congr 为当前头部函数创建与（非依值和显式）参数数量相同的目标 （此处头部函数是乘法）。congr creates as many targets as there are (nondependent and explicit) arguments to the current head function (here the head function is multiplication).

• rfl 使用自反性（reflexivity）关闭目标。rfl closes target using reflexivity.

一旦到达相关目标，我们可以像在普通策略模式中一样使用 rw。Once arrived at the relevant target, we can use rw as in normal tactic mode.

使用转换模式的第二个主要原因是重写绑定器（binder）内部。假设我们想要证明示例 (fun x : Nat => 0 + x) = (fun x => x)。 最直接的首次尝试是进入策略模式并尝试 rw [Nat.zero_add]。但这会失败，并出现令人沮丧的The second main reason to use conversion mode is to rewrite under binders. Suppose we want to prove example (fun x : Nat => 0 + x) = (fun x => x). The naive first attempt is to enter tactic mode and try rw [Nat.zero_add]. But this fails with a frustrating

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

解决方案是：The solution is:

其中 intro x 是进入 fun 绑定器内部的导航命令。 请注意，此示例有些人为设计，我们也可以这样做：where intro x is the navigation command entering inside the fun binder. Note that this example is somewhat artificial, one could also do:

或者简单地or just

conv 也可以使用 conv at h 重写来自局部上下文（local context）的假设（hypothesis）h。conv can also rewrite a hypothesis h from the local context, using conv at h.

11.2. 模式匹配11.2. Pattern matching🔗

使用上述命令进行导航可能很繁琐。可以通过模式匹配来简化，如下所示：Navigation using the above commands can be tedious. One can shortcut it using pattern matching as follows:

这只是以下内容的语法糖which is just syntax sugar for

当然，允许使用通配符（wildcard）：Of course, wildcards are allowed:

11.3. 结构化转换策略11.3. Structuring conversion tactics🔗

花括号（curly bracket）和 . 也可以在 conv 模式中用于结构化策略：Curly brackets and . can also be used in conv mode to structure tactics:

11.4. 转换模式中的其他策略11.4. Other tactics inside conversion mode🔗

• arg i 进入某个应用的第 i 个非依值显式参数。arg i enter the i-th nondependent explicit argument of an application.

  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 的替代名称。args is an alternative name for congr.

• simp 将化简器（simplifier）应用于当前目标。它支持与普通策略模式中相同的选项。simp applies the simplifier to the current goal. It supports the same options available in regular tactic mode.

  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 := 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。enter [1, x, 2, y] iterate arg and intro with the given arguments.

• done 在存在未解决的目标时失败。done fail if there are unsolved goals.

• trace_state 显示当前策略状态。trace_state display the current tactic state.

• whnf 将项置于弱头正规形式（weak head normal form）。whnf put term in weak head normal form.

• tactic => <tactic sequence> 返回常规策略模式。这 对于处理 conv 模式不支持的目标，以及 应用自定义的同余（congruence）和外延性（extensionality）引理非常有用。tactic => <tactic sequence> go back to regular tactic mode. This is useful for discharging goals not supported by conv mode, and applying custom congruence and extensionality lemmas.

  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> 的语法糖。apply <term> is syntax sugar for 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! 🐙