Lean 战术组合

在Lean中，战术组合（Tactical Composition）是一种将多个战术（tactics）组合在一起的技术，用于简化证明过程并提升代码的可读性。通过战术组合，你可以将多个步骤合并为一个更简洁的表达式，从而减少代码冗余并提高效率。

什么是战术组合？

战术组合的核心思想是将多个战术串联或并联在一起，形成一个更强大的战术。Lean提供了多种方式来组合战术，例如：

顺序组合：使用 ; 将多个战术按顺序执行。
选择组合：使用 <|> 尝试多个战术，直到其中一个成功。
条件组合：使用 try 或 repeat 等战术来控制执行流程。

这些组合方式可以帮助你更灵活地构建证明，并避免重复代码。

顺序组合

顺序组合是最常见的战术组合方式。通过使用 ;，你可以将多个战术按顺序执行。例如：

lean
example : ∀ (n : Nat), n + 0 = n := by
  intro n
  rw [Nat.add_zero]

在这个例子中，intro n 和 rw [Nat.add_zero] 是两个独立的战术。我们可以使用 ; 将它们组合在一起：

lean
example : ∀ (n : Nat), n + 0 = n := by
  intro n; rw [Nat.add_zero]

这种组合方式不仅减少了代码行数，还使证明过程更加紧凑。

选择组合

选择组合允许你尝试多个战术，直到其中一个成功。使用 <|> 可以实现这一点。例如：

lean
example : ∀ (n : Nat), n + 0 = n := by
  intro n
  apply Nat.add_zero <|> rw [Nat.add_zero]

在这个例子中，Lean会首先尝试 apply Nat.add_zero，如果失败，则会尝试 rw [Nat.add_zero]。这种组合方式非常适合处理可能存在多种证明路径的情况。

条件组合

条件组合允许你根据特定条件执行战术。例如，try 战术会尝试执行一个战术，如果失败则不会报错：

lean
example : ∀ (n : Nat), n + 0 = n := by
  intro n
  try rw [Nat.add_zero]

另一个常用的战术是 repeat，它会重复执行一个战术，直到无法继续：

lean
example : ∀ (n : Nat), n + 0 = n := by
  intro n
  repeat rw [Nat.add_zero]

这些战术组合方式可以帮助你更灵活地控制证明流程。

实际案例

以下是一个更复杂的例子，展示了如何在实际证明中使用战术组合：

lean
example : ∀ (n m : Nat), n + m = m + n := by
  intros n m
  induction n with
  | zero => rw [Nat.zero_add, Nat.add_zero]
  | succ k ih => rw [Nat.succ_add, Nat.add_succ, ih]

在这个例子中，我们使用了 intros、induction 和 rw 等战术，并通过顺序组合将它们串联在一起。这种组合方式使证明过程更加清晰和高效。

总结

战术组合是Lean中一种强大的技术，可以帮助你简化证明过程并提升代码的可读性。通过顺序组合、选择组合和条件组合，你可以更灵活地构建证明，并减少代码冗余。

提示

尝试将常用的战术组合封装成自定义战术，以便在多个证明中复用。
使用 ; 和 <|> 时，注意战术的执行顺序和逻辑关系。

附加资源与练习

练习

尝试将以下证明改写为使用战术组合的形式：

lean
example : ∀ (n : Nat), n * 1 = n := by
  intro n
  rw [Nat.mul_one]

使用 <|> 组合多个战术，尝试证明以下命题：

lean
example : ∀ (n : Nat), n + 0 = n := by
  intro n
  apply Nat.add_zero <|> rw [Nat.add_zero]

资源

Lean官方文档
《Theorem Proving in Lean》——一本适合初学者的Lean教程

通过不断练习和探索，你将能够熟练掌握战术组合，并在Lean中编写出更高效的证明代码！

什么是战术组合？​

顺序组合​

选择组合​

条件组合​

实际案例​

总结​

附加资源与练习​

练习​

资源​