转换策略模式

在策略块中,可以使用关键字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]
  • argscongr的替代品。

  • 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]argintro使用给定参数的宏。
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₂