编辑“︁Lean战术编写”︁

= Lean战术编写 =

'''Lean战术编写'''是Lean元编程中的核心概念，它允许用户通过编写自动化策略（tactics）来辅助或完全自动化数学证明和程序验证过程。战术本质上是元程序，它们操作Lean的证明状态（proof state），逐步将目标分解为更简单的子目标，直到所有目标都被解决。本教程将详细介绍Lean战术的基本结构、使用方法以及实际应用案例。

== 介绍 ==

在Lean中，证明通常是通过应用一系列战术来构建的。战术可以视为一种高级指令，它们能够分析当前的证明状态并执行逻辑推理步骤。例如，`intro`用于引入假设，`apply`用于应用定理，而`rw`（rewrite）用于重写表达式。通过组合这些基础战术，用户可以构建复杂的自动化证明策略。

=== 证明状态 ===
Lean的证明状态是一个包含以下部分的数据结构：
* '''目标（Goals）'''：需要证明的命题集合。
* '''上下文（Context）'''：当前可用的假设和变量。
* '''元数据（Metavariables）'''：未解决的约束或占位符。

战术的作用就是逐步转换这个状态，直到没有剩余目标为止。

== 基础战术 ==

以下是Lean中最常用的基础战术及其用法示例：

=== `intro` ===
`intro`用于引入一个假设。例如，若要证明`P → Q`，可以使用`intro h`将`h : P`加入上下文。

<syntaxhighlight lang="lean">
example : P → Q := by
  intro h
  -- 现在上下文中有 h : P，目标是 Q
</syntaxhighlight>

=== `apply` ===
`apply`用于应用一个定理或引理。如果目标匹配定理的结论，Lean会将目标替换为定理的前提。

<syntaxhighlight lang="lean">
example (h : P → Q) (p : P) : Q := by
  apply h
  exact p
</syntaxhighlight>

=== `rw`（重写） ===
`rw`用于根据等式重写目标或假设。

<syntaxhighlight lang="lean">
example (h : x = y) : f x = f y := by
  rw [h]
  -- 目标变为 f y = f y，可通过 reflexivity 解决
</syntaxhighlight>

== 组合战术 ==

战术可以通过组合来实现更复杂的行为。Lean提供了多种组合方式：

=== 分号 `;` ===
分号用于依次应用多个战术。

<syntaxhighlight lang="lean">
example : P ∧ Q → Q ∧ P := by
  intro h
  cases h with | intro hp hq =>
    apply And.intro
    exact hq
    exact hp
</syntaxhighlight>

=== `<|>`（或操作符） ===
`<|>`表示尝试第一个战术，如果失败则尝试第二个。

<syntaxhighlight lang="lean">
example (h : P ∨ Q) : Q ∨ P := by
  cases h with
  | inl hp => apply Or.inr; exact hp
  | inr hq => apply Or.inl; exact hq
</syntaxhighlight>

== 自定义战术 ==

用户可以通过`macro_rules`或`elab`指令定义自定义战术。以下是一个简单的自定义战术示例：

<syntaxhighlight lang="lean">
macro "triv" : tactic => `(tactic| exact True.intro)

example : True := by
  triv
</syntaxhighlight>

== 实际案例 ==

以下是一个实际案例，展示如何使用战术自动化证明一个简单的逻辑命题：

=== 案例：交换合取命题 ===
证明`P ∧ Q → Q ∧ P`：

<syntaxhighlight lang="lean">
example : P ∧ Q → Q ∧ P := by
  intro h
  cases h with | intro hp hq =>
    apply And.intro
    exact hq
    exact hp
</syntaxhighlight>

=== 案例：自然数加法交换律 ===
使用归纳法和重写证明`n + m = m + n`：

<syntaxhighlight lang="lean">
theorem add_comm (n m : Nat) : n + m = m + n := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Nat.add_succ, Nat.succ_add, ih]
</syntaxhighlight>

== 高级主题 ==

对于高级用户，Lean还支持以下功能：

=== 元战术（Meta-tactics） ===
元战术允许在战术中嵌入更复杂的逻辑，例如条件分支或循环。

<syntaxhighlight lang="lean">
example (n : Nat) : n = n := by
  match n with
  | 0 => rfl
  | _ + 1 => rfl
</syntaxhighlight>

=== 交互式战术开发 ===
Lean的交互式模式允许用户逐步构建战术并实时查看证明状态的变化。

== 总结 ==

Lean战术编写是Lean元编程的核心技术之一，它通过提供一系列基础战术和组合方式，使用户能够高效地构建和自动化证明。从简单的逻辑命题到复杂的数学定理，战术编写都能显著提升证明的效率和可读性。通过本教程的学习，读者应能掌握基础战术的使用方法，并逐步探索更高级的元编程技巧。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean元编程]]