交互式定理证明器中的策略

交互式定理证明器（如 Coq、Isabelle、Agda）允许用户通过形式化证明来验证数学定理或程序正确性。其核心功能依赖于策略——一种指导证明过程的指令。下面从基础概念到高级应用逐步展开。

1. 策略的基本角色

在交互式证明器中，证明通常以目标状态管理：

• 初始目标：待证明的命题（如 ∀n:ℕ, n+0=n）。
• 策略应用：用户输入策略（如 induction n），系统将目标分解为子目标。
• 证明完成：所有子目标被解决后，证明成立。

例如，在 Coq 中，策略 simpl 可简化表达式（将 n+0 化为 n），而 reflexivity 可验证等式两边相同。

2. 策略的分类与常见形式

策略按功能可分为以下几类：

（1）基本推理策略

• intros：引入假设（将前提移至上下文）。

  Goal ∀P Q, P→Q→P.  
  intros P Q H1 H2.  (* 上下文：P, Q, H1:P, H2:Q *)  
  

• apply：应用已知定理或假设到当前目标。

（2）等式与化简策略

• rewrite：使用等式替换目标中的子项。
• simpl/compute：执行计算化简（如β规约、算术运算）。

（3）自动化策略

• auto：根据预设规则库尝试自动证明。
• omega：解决线性算术问题。

3. 策略的组合与控制

复杂证明需组合策略并控制执行流程：

• 分号 ;：顺序执行策略（如 induction n; simpl; auto）。
• 括号 []：为不同子目标指定不同策略。

  induction n as [|n' IH];  
    [ simpl; reflexivity.   (* 基础情况 *)  
    | simpl; rewrite IH; reflexivity. ]. (* 归纳情况 *)  
  

• 失败处理：try T 在策略 T 失败时静默跳过；repeat T 重复执行直到失败。

4. 自定义策略与元编程

证明器允许用户扩展策略语言：

• Ltac（Coq）：过程式元编程语言。

  Ltac solve_eq := repeat (simpl; rewrite <- plus_n_Sm); reflexivity.  
  

• Isar（Isabelle）：声明式语言，支持结构化证明脚本。
  自定义策略能封装重复模式，提升证明效率。

5. 策略的可靠性与局限性

• 可靠性：策略生成的底层证明需经核验器检查，避免逻辑错误。
• 完备性：自动化策略（如 firstorder）可能因搜索空间不足而失败，需人工引导。
• 交互性：策略开发需平衡自动化与可控性，如使用 debug auto 查看推理步骤。

6. 高级应用：策略与数学库的协同

大型形式化项目（如 CompCert 编译器、四色定理证明）依赖策略管理复杂性：

• 模块化策略：针对特定理论（如群论、拓扑）设计领域专用策略。
• 策略组合子：通过函数式编程组合基础策略（如 t1 THEN t2）。

此词条展示了策略如何桥接人类直觉与机器可检证证明，是形式化方法的核心工具。