The Hitchhiker’s Guide to Logical Verification

• 语言: 英语
• 格式: .pdf
• 来源: cs.brown.edu

摘要

The document provides an introduction to using the Lean theorem prover for interactive theorem proving. It covers fundamental concepts, tactics, and techniques for verifying logical statements and systems. The guide explains how to use Lean for proving properties about functional and imperative programming languages, mathematics, and other domains. It emphasizes the importance of hands-on practice and understanding the underlying logic of proof assistants. The document also introduces key Lean tactics such as `apply`, `exact`, `assumption`, and `cc`, and discusses the use of Hoare logic for specifying and verifying program correctness. The guide is designed to help readers develop practical skills in formal verification and prepare them for applying these techniques in academic or industrial settings.

AI总结

《 Hitchhiker’s Guide to Logical Verification》 是一本 companion 书，配合 Vrije Universiteit Amsterdam 的逻辑验证（LoVe）课程使用，旨在教授交互式定理证明（Interactive Theorem Proving, ITP）的基础理论和技巧。Lean 是该课程的主要工具，但其目标不是将 Lean 作为最终目标，而是通过 Lean 教授 ITP 的核心概念和方法。

### 核心目标
1. **学习交互式定理证明的基础理论和技巧**：包括如何使用逻辑语言建模系统和陈述系统属性。
2. **熟悉成功应用领域**：如函数编程、命令式编程语言的语义、数学等。
3. **培养实际技能**：能够应用于更大项目（如研究或工业界）。
4. **掌握 Lean 后，能够迁移到其他证明助手**：如 Agda、Coq、HOL4 或 Isabelle/HOL。
5. **具备阅读相关科学论文的能力**：如 Certified Programs and Proofs (CPP) 和 Interactive Theorem Proving (ITP) 会议的论文。

### 重要特性
- **实用导向**：书中包含 Lean 的配套文件，包括演示文件、练习题和作业题。
- **理论与实践结合**：强调通过实践掌握 ITP，而非仅依赖理论讲解。
- **模块化和可扩展性**：书中内容结构清晰，便于逐步学习和深入探索。

### 关键概念
1. **Lean 的基本自动化功能**：Lean 的核心库提供了许多现代证明助手的自动化功能，简化了定理证明过程。
2. **逻辑验证的核心思想**：通过 Hoare 逻辑和操作语义来验证程序的正确性。
3. **定理证明工具的使用**：书中介绍了 Lean 的一些关键 tactic（如 `apply`、`exact`、`intro` 和 `cc`）及其应用场景。

### 成功案例
- **编译器验证**：如 Leroy 的 formally verified compiler back-end。
- **操作系统内核验证**：如 seL4 操作系统内核的 formal verification。
- **数学定理验证**：如 Hales 等人对 Kepler 猜想的 formal proof。

### 总结
《 Hitchhiker’s Guide to Logical Verification》 是一本适合学习交互式定理证明的入门指南，强调通过实践掌握 Lean 的核心概念和技巧。书中结合理论和案例，展示了定理证明在函数编程、命令式编程语言语义、数学和系统验证等领域的广泛应用。对于希望掌握现代证明助手并应用于实际问题的研究者和开发者来说，这是一本非常实用的参考书。