The Hitchhiker’s Guide to Logical Verification

这篇文档《The Hitchhiker’s Guide to Logical Verification》主要介绍了在使用Lean系统进行逻辑验证时的结构化证明方法和相关构造。以下是核心内容的总结： ### 主要内容概述 1. **结构化证明的核心命令**： - `fix`：用于固定变量。 - `assume`：用于假设命题。 - `have`：用于定义辅助命题或引入新的证明步骤。 - `show`：用于展示最终结论。 2. **结构化证明的格式**： - 典型的结构化证明遵循 `fix–assume–have–show` 的模式。例如： ```lean4 lemma l : ∀(c1 : σ1) ...(cl : σl), P1 → · · · → Pm → R := fix (c1 : σ1) ...(cl : σl), assume h1 : P1, ...assume hm : Pm, have k1 : Q1 := ..., ...have kn : Qn := ..., show R, from ... ``` - 通过这种模式，可以清晰地组织证明步骤，提高可读性。 3. **有用的构造**： - `have` 命令可以定义辅助命题，例如 `have hb : b := hab ha`，其中 `hb` 是证明 `b` 的一个辅助命题名称。 - 在复杂证明中，可以通过有序的 `have` 和 `show` 命令逐步推导出最终结论。 4. **Lemma和假设的使用**： - Lemma 或假设的名称可以直接作为证明的一部分使用。例如，已证明的 `lemma two_add_two_eq_four : 2 + 2 = 4` 可以在后续证明中直接引用其名称作为证明。 5. **其他内容**： - 文档还涉及了关于 Lean 系统中新构造的总结、有理数与实数的相关内容，以及一些逻辑符号和命题的证明方法。 ### 核心观点 文档的核心在于系统地介绍了 Lean 系统中结构化证明的方法和技巧，通过 `fix–assume–have–show` 模式，帮助用户更高效地组织和管理复杂的证明步骤，从而提高证明的可读性和可维护性。同时，文档还强调了定义辅助命题和复用已有证明的重要性。