跳到主要内容

Lean 战术系统

Lean是一个交互式定理证明器，它允许用户通过编写代码来构建数学证明。Lean的战术系统是其核心功能之一，它提供了一系列工具和方法，帮助用户逐步构建证明。本文将详细介绍Lean的战术系统，并通过示例展示其使用方法。

什么是Lean战术系统？​

Lean的战术系统是一组用于构建证明的工具和方法。这些战术可以帮助用户自动化部分或全部证明过程，从而简化复杂的数学证明。战术系统允许用户通过逐步应用战术来构建证明，而不是手动编写每一步的逻辑。

基本战术​

intro​

intro 战术用于引入假设。当你需要证明一个形如 ∀ x, P x 的命题时，可以使用 intro 来引入变量 x。

lean
example : ∀ (n : ℕ), n = n :=
begin
  intro n,
  refl
end

在这个例子中，intro n 引入了变量 n，然后 refl 用于证明 n = n。

apply​

apply 战术用于应用一个已知的定理或引理。假设你有一个定理 H : P → Q，并且你需要证明 Q，你可以使用 apply H 来应用这个定理。

lean
example (P Q : Prop) (H : P → Q) (p : P) : Q :=
begin
  apply H,
  exact p
end

在这个例子中，apply H 应用了定理 H，然后 exact p 用于提供 P 的证明。

exact​

exact 战术用于提供一个精确的证明项。当你已经有一个证明项时，可以使用 exact 来完成证明。

lean
example (P : Prop) (p : P) : P :=
begin
  exact p
end

在这个例子中，exact p 直接提供了 P 的证明。

组合战术​

战术可以组合使用，以构建更复杂的证明。例如，你可以使用 intro 和 apply 来逐步构建一个证明。

lean
example (P Q R : Prop) (H1 : P → Q) (H2 : Q → R) (p : P) : R :=
begin
  apply H2,
  apply H1,
  exact p
end

在这个例子中，apply H2 应用了 H2，然后 apply H1 应用了 H1，最后 exact p 提供了 P 的证明。

实际案例​

假设我们需要证明一个简单的命题：如果 n 是偶数，那么 n + 2 也是偶数。我们可以使用Lean的战术系统来构建这个证明。

lean
import tactic

def even (n : ℕ) : Prop := ∃ k, n = 2 * k

example (n : ℕ) (H : even n) : even (n + 2) :=
begin
  cases H with k Hk,
  use k + 1,
  rw Hk,
  ring
end

在这个例子中，cases H with k Hk 解构了 even n 的假设，use k + 1 提供了一个新的变量 k + 1，rw Hk 重写了等式，最后 ring 完成了证明。

总结​

Lean的战术系统提供了一系列强大的工具，帮助用户逐步构建和自动化证明。通过组合使用不同的战术，用户可以有效地处理复杂的数学证明。本文介绍了几个基本的战术，并通过实际案例展示了它们的使用方法。

附加资源​

练习​

  1. 使用 intro 和 apply 战术证明以下命题：

    lean
    example (P Q : Prop) (H : P → Q) (p : P) : Q :=
    begin
      -- 你的证明
    end

  2. 使用 cases 和 use 战术证明以下命题：

    lean
    example (n : ℕ) (H : even n) : even (n + 4) :=
    begin
      -- 你的证明
    end

通过这些练习，你可以进一步熟悉Lean的战术系统，并掌握如何在实际证明中应用它们。