跳到主要内容

Lean 战术编写

介绍​

Lean是一个交互式定理证明器，它允许用户通过编写代码来构造数学证明。在Lean中，**战术（Tactics）**是用于自动化证明过程的工具。它们可以帮助你分解目标、应用定理、简化表达式等。掌握战术编写是Lean元编程的核心技能之一。

本文将逐步介绍如何在Lean中编写战术，并通过实际案例展示其应用场景。

什么是战术？​

战术是Lean中用于操作证明状态的小程序。它们可以看作是对当前证明目标的指令，告诉Lean如何将目标分解为更简单的子目标，或者如何应用已知的定理来解决问题。

基本战术​

在Lean中，有一些内置的基本战术，例如：

  • intro：用于引入假设。
  • apply：用于应用定理。
  • exact：用于直接完成目标。
  • simp：用于简化表达式。

这些战术可以组合使用，以构建复杂的证明。

编写自定义战术​

除了使用内置战术外，你还可以编写自定义战术。自定义战术允许你封装常用的证明步骤，以便在多个证明中重复使用。

示例：编写一个简单的战术​

假设我们经常需要证明某个特定的逻辑命题，例如 A → A。我们可以编写一个自定义战术来自动完成这个证明。

lean
meta def my_tactic : tactic unit :=
do tactic.intro `h,
   tactic.exact (expr.var 0)

在这个例子中，my_tactic 是一个自定义战术，它首先使用 intro 引入假设 h，然后使用 exact 完成证明。

使用自定义战术​

编写完自定义战术后，你可以在证明中使用它：

lean
example : A → A :=
begin
  my_tactic
end

这个例子展示了如何使用自定义战术 my_tactic 来证明 A → A。

实际案例​

案例1：自动化逻辑证明​

假设我们需要证明一个逻辑命题 (A → B) → (B → C) → (A → C)。我们可以编写一个战术来自动完成这个证明。

lean
meta def logic_tactic : tactic unit :=
do tactic.intro `h1,
   tactic.intro `h2,
   tactic.intro `h3,
   tactic.apply (expr.var 1),
   tactic.apply (expr.var 2),
   tactic.exact (expr.var 0)

然后，我们可以使用这个战术来证明命题：

lean
example : (A → B) → (B → C) → (A → C) :=
begin
  logic_tactic
end

案例2：简化表达式​

假设我们需要简化一个复杂的表达式，例如 (a + b) + (c + d)。我们可以编写一个战术来自动完成这个任务。

lean
meta def simplify_tactic : tactic unit :=
do tactic.simp

然后，我们可以使用这个战术来简化表达式：

lean
example : (a + b) + (c + d) = a + b + c + d :=
begin
  simplify_tactic
end

总结​

通过本文，我们学习了如何在Lean中编写战术。战术是Lean中自动化证明过程的重要工具，掌握战术编写可以帮助你更高效地完成复杂的证明任务。

附加资源​

练习​

  1. 编写一个自定义战术，用于证明 A → (B → A)。
  2. 编写一个自定义战术，用于简化表达式 (a * b) * (c * d)。

通过练习，你将更深入地理解战术编写，并能够在实际证明中灵活运用。