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`加入上下文。
example : P → Q := by
intro h
-- 现在上下文中有 h : P，目标是 Q
`apply`[编辑 | 编辑源代码]
`apply`用于应用一个定理或引理。如果目标匹配定理的结论，Lean会将目标替换为定理的前提。
example (h : P → Q) (p : P) : Q := by
apply h
exact p
`rw`（重写）[编辑 | 编辑源代码]
`rw`用于根据等式重写目标或假设。
example (h : x = y) : f x = f y := by
rw [h]
-- 目标变为 f y = f y，可通过 reflexivity 解决
组合战术[编辑 | 编辑源代码]
战术可以通过组合来实现更复杂的行为。Lean提供了多种组合方式：
分号 `;`[编辑 | 编辑源代码]
分号用于依次应用多个战术。
example : P ∧ Q → Q ∧ P := by
intro h
cases h with | intro hp hq =>
apply And.intro
exact hq
exact hp
`<|>`（或操作符）[编辑 | 编辑源代码]
`<|>`表示尝试第一个战术，如果失败则尝试第二个。
example (h : P ∨ Q) : Q ∨ P := by
cases h with
| inl hp => apply Or.inr; exact hp
| inr hq => apply Or.inl; exact hq
自定义战术[编辑 | 编辑源代码]
用户可以通过`macro_rules`或`elab`指令定义自定义战术。以下是一个简单的自定义战术示例：
macro "triv" : tactic => `(tactic| exact True.intro)
example : True := by
triv
实际案例[编辑 | 编辑源代码]
以下是一个实际案例，展示如何使用战术自动化证明一个简单的逻辑命题：
案例：交换合取命题[编辑 | 编辑源代码]
证明`P ∧ Q → Q ∧ P`：
example : P ∧ Q → Q ∧ P := by
intro h
cases h with | intro hp hq =>
apply And.intro
exact hq
exact hp
案例：自然数加法交换律[编辑 | 编辑源代码]
使用归纳法和重写证明`n + m = m + n`：
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]
高级主题[编辑 | 编辑源代码]
对于高级用户，Lean还支持以下功能：
元战术（Meta-tactics）[编辑 | 编辑源代码]
元战术允许在战术中嵌入更复杂的逻辑，例如条件分支或循环。
example (n : Nat) : n = n := by
match n with
| 0 => rfl
| _ + 1 => rfl
交互式战术开发[编辑 | 编辑源代码]
Lean的交互式模式允许用户逐步构建战术并实时查看证明状态的变化。
总结[编辑 | 编辑源代码]
Lean战术编写是Lean元编程的核心技术之一，它通过提供一系列基础战术和组合方式，使用户能够高效地构建和自动化证明。从简单的逻辑命题到复杂的数学定理，战术编写都能显著提升证明的效率和可读性。通过本教程的学习，读者应能掌握基础战术的使用方法，并逐步探索更高级的元编程技巧。