SF-lean4 软件基础

Appearance

重塑经典：用现代 Lean 4 重构《软件基础》全三卷与交互式文档 ​

项目主页：https://ghost-silver.github.io/SF-lean4/
开源仓库：https://github.com/Ghost-Silver/SF-lean4
作者：Ghost-Silver · SF-lean4 社区
状态：三卷 57 章全量形式化实现与审计已 100% 完成，文档网站正式上线。

0. 引言：形式化圣经与新时代的定理证明器 ​

在计算机科学与程序语言理论（Programming Language Theory, PLT）的世界里，有一部被全球学术界与工业界奉为圭臬的传世之作——宾夕法尼亚大学 Benjamin C. Pierce 教授团队开创的**《软件基础》（Software Foundations，简称 SF）**。

自问世以来，这套教材以其革命性的“文学化形式化编程（Literate Formal Programming）”范式，影响了数以万计的逻辑学家、编译器作者与软件工程师。它打破了传统纸笔证明“直觉跳步、细微漏洞百出”的弊病，将每一个数学定义、每一条操作语义规则、每一个核心定理的推导，都原原本本地交给证明助手（Proof Assistant）进行机器级检查。

然而，经典的《软件基础》始终基于 Coq（现改名为 Rocq）构建。不可否认，Coq 作为开拓者立下了汗马功劳，但在数十年的演进中，其略显陈旧的 Ltac 战术系统、割裂的脚本/模块编译机制以及不够现代的通用编程人体工学，往往令新一代学习者望而却步。

与此同时，由 Leonardo de Moura 主导的现代纯函数式定理证明系统与依值类型编程语言 Lean 4 正在以势如破竹的姿态重构整个领域。从菲尔兹奖得主陶哲轩对数学定理库的重磅投入，到顶级高校与工业界关键软件的系统性验证，Lean 4 凭借其：

  • 极其优雅简洁的现代语法与模式匹配方程编译器；
  • 基于宏（Macro）与单子（Monad）的高度可扩展元编程体系；
  • 原生多平台 AOT 高性能代码生成；
  • 卓越的 LSP 现代编辑器交互体验（VS Code / Neovim 零延迟即时目标视图），

毫无疑问成为了二十一世纪形式化验证领域最具生命力的明珠。

今天，我们非常自豪地向开源社区宣布：SF-lean4 项目正式完工并全量上线！ 我们完成了《软件基础》全三卷、57 个核心章节、27,000+ 行 Lean 4 纯正代码、800+ 道实战习题的全面形式化重构与汉化精校，并构建了配套的极速交互式在线文档系统。

1. 全卷全景一览：三卷合一的宏大理论图景 ​

在本次重构中，我们不仅忠实还原了原版经典逻辑脉络，更针对 Lean 4 依赖类型论进行了地道的 Idiomatic 现代重写。整套体系包含三大核心支柱：

                       ┌──────────────────────────────────────┐
                       │         SF-Lean 4 现代重制版         │
                       └──────────────────────────────────────┘
                                           │
             ┌─────────────────────────────┴─────────────────────────────┐
             ▼                             ▼                             ▼
┌────────────────────────┐    ┌────────────────────────┐    ┌────────────────────────┐
│ 卷一：逻辑基础 (LF)    │    │ 卷二：语言基础 (PLF)   │    │ 卷三：算法验证 (VFA)   │
│ 19 章 · 200+ 习题      │    │ 21 章 · 300+ 习题      │    │ 17 章 · 300+ 习题      │
├────────────────────────┤    ├────────────────────────┤    ├────────────────────────┤
│ - 纯函数式编程与多态   │    │ - 程序等价性与同余性   │    │ - 排序算法全规约验证   │
│ - 结构化归纳证明反演   │    │ - 霍尔逻辑与 VCGen     │    │ - 多重集计数置换模型   │
│ - 柯里-霍华德证明对象  │    │ - 小步操作语义与闭包   │    │ - Okasaki 红黑树平衡   │
│ - 构造性命题逻辑代数   │    │ - STLC 类型安全体系    │    │ - 二进制 Trie 查找表   │
│ - Imp 语言大步操作语义 │    │ - 子类型化与包容法则   │    │ - 优先队列与二项堆     │
│ - 自动化证明策略搜索   │    │ - 可变引用与强规范化   │    │ - Kempe 图着色验证     │
└────────────────────────┘    └────────────────────────┘    └────────────────────────┘

卷一：逻辑基础 (Logical Foundations, 19 章) ​

作为整个体系的基石，卷一带领读者从最纯粹的布尔枚举类型与归纳数据类型出发，逐步跨越到现代类型论的核心：

  • 柯里-霍华德同构（Curry-Howard Isomorphism）：深刻揭示“命题即类型（Propositions-as-Types），证明即程序（Proofs-as-Programs）”的本质，学习者将亲手用 Lean 4 构造证明项（Proof Objects）；
  • 归纳命题与关系：置换（Permutation）、正则表达式泵引理（Pumping Lemma）与布尔可判定性反射（Reflection）；
  • Imp 简单命令式语言：定义语法树、大步操作语义与抽象状态映射，并实现词法语法解析器与自动化求解策略。

卷二：编程语言基础 (Programming Language Foundations, 21 章) ​

深入计算机程序语言的内在机理，探索编译优化与形式语义的核心边界：

  • 程序等价性（Behavioral Equivalence）：形式化证明编译器常量折叠优化的可靠性，探讨非确定性语法扩展；
  • 霍尔逻辑（Hoare Logic）：严密构建三元组推导系统，证明验证条件生成器（VCGen）的健全性与相对完备性，掌握循环不变量的设计艺术；
  • 简单类型 Lambda 演算（STLC）：完整形式化操作语义、代换引理，严密确立类型系统的进益定理（Progress）与保型定理（Preservation）（即类型安全性）；
  • 前沿类型理论：子类型化（Subtyping）、记录类型系统、可变状态堆内存引用（References），以及全卷巅峰之作——基于 Tait 逻辑关系（Logical Relations）的 STLC 强规范化（Strong Normalization）停机性证明。

卷三：函数式算法验证 (Verified Functional Algorithms, 17 章) ​

将定理证明应用于计算机科学最经典的数据结构与算法，展示全规约形式化验证的威力：

  • 排序算法正确性：插入排序、选择排序与归并排序的“有序性（Sortedness）”与“多重集置换保持（Permutation Preservation）”；
  • 表示不变量与数据抽象：二叉搜索树（BST）与抽象模型的仿真对应；
  • 高级数据结构：Okasaki 红黑树平衡旋转不变量与对数高度界限证明、二进制前缀树（Trie）与正整数算术双射、二项堆（Binomial Heap）的进位链与可合并优先队列；
  • 工业编译器后端应用：Kempe-Chaitin 寄存器分配图着色算法的完备规约与健全性检验。

2. 核心技术突破：从 Coq 到 Lean 4 的现代蜕变 ​

从 Coq 迁移到 Lean 4 绝非机械的“关键字替换”，而是一场深刻的现代范式重塑：

2.1 告别繁琐战术，拥抱递归方程编译器 ​

在传统 Coq 中，定义递归函数往往需要小心翼翼地遵循构造子嵌套，证明中充斥着冗长的 inversion 与 destruct 展开。

而在 Lean 4 中，其强大的**方程编译器（Equation Compiler）与模式匹配（Pattern Matching）**让定义与证明融为一体。例如在处理列表多态映射或二叉树重平衡时，Lean 4 能够直接识别深层解构与良基递归（Well-founded Recursion），大大压缩了机械样板代码。

2.2 现代求解器加持：Presburger 算术决策过程 ​

在 Coq 中，读者需要经常在 omega、lia、nia 之间权衡。而在现代 Lean 4 中，官方内建的 omega 决策过程基于最新的 Presburger 算术整数线性规划算法，能够一键秒杀包括自然数字段截断减法、商余关系、不等式传递闭包等所有线性算术目标：

lean
-- 在 VFA/Perm.lean 中，复杂的数值比较推导在 Lean 4 中一气呵成：
theorem le_trans (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  omega

2.3 宏体系的魔力：所见即所得的嵌入式领域语言 (DSL) ​

在卷二霍尔逻辑与 Imp 语言的设计中，我们充分发挥了 Lean 4 先进的卫生宏系统（Hygienic Macros）。我们无需依赖复杂的外部解析插件，直接在 Lean 4 内部扩展了 Imp 命令语法与霍尔三元组表示：

lean
-- 读者可以在代码中直接书写如同教科书般的 Imp 语法：
syntax "<{" term "}>" : term
syntax "{{" term "}}" term:max "{{" term "}}" : term

-- 验证赋值规则的直观性：
theorem hoare_asgn : ∀ (Q : Assertion) (X : String) (a : aexp),
  {{ Q [ X ↦ a ] }} (X ::= a) {{ Q }}

语法高亮、自动补全、语法报错与上下文推导完全天然无缝地内嵌于编辑器中！

3. 文档工程创新：单源真理 (Single Source of Truth) ​

为了达到“无限好看、极致易用”的目标，我们在工程基建上投入了大量心血：

3.1 拒绝代码与文档割裂 ​

许多形式化开源项目最终陷入“代码更新了，文档还是旧的；或者文档写得很漂亮，代码却无法编译”的恶性循环。

在 SF-lean4 中，我们确立了**代码即唯一真理（Single Source of Truth）**原则：

  • 所有 57 个章节的纯正形式化代码全部存放在 SFLean4/ 源码目录中；
  • 教学散文采用 /-! ... -/ 文学化注释与代码紧密相连；
  • 自研自动化管道 [scripts/build_docs.py](file:///Users/ghostface/LuoJin/SF-lean4/scripts/build_docs.py)，实时将 Lean 源码抽离、过滤纯符号边框、将习题规范化转换为带星级 Badge 的精美卡片，并自动生成结构化导航树。

3.2 毫秒级极速交互与顶级排版体验 ​

依托 VitePress 现代响应式静态站点生成器，我们实现了：

  1. 零延迟全文检索：内置 MiniSearch 客户端毫秒级搜索引擎，中英文混合分词，无论是搜索“柯里-霍华德”、“红黑树平衡”，还是直接检索定理名称 hoare_consequence，都能瞬间跳转；
  2. 矢量数学公式排版：全面集成 MathJax 3，所有逻辑推导式、大步语义关系 st =[ c ]=> st' 与归约规则均以矢量高清晰呈现，针对移动端特别优化了横向溢出滚动；
  3. 分卷分级清晰标识：360+ 道习题全部配备了颜色自适应的星级 Badge（1 星青绿、2 星蓝紫、3 星琥珀、4~5 星挑战赤红），做题路径清晰明了；
  4. GitHub Actions 持续交付：配置了全自动化部署流水线，每当源码有新提交，静态站点自动完成重构、静态化并发布至 GitHub Pages。

4. 5 分钟上手体验：开启你的形式化探索 ​

不论你是想在网页上随心阅读，还是想在本地编辑器中一步步填补 sorry 攻克难题，环境都已完全开箱即用：

选项 A：在线阅读（免安装） ​

直接访问网页端，随时在手机、平板或 PC 上阅读全书 57 章与所有练习题解析：
👉 SF-lean4 官方在线文档

选项 B：本地交互式沉浸证明（推荐！） ​

  1. 安装 Lean 4 版本管理器 elan：

    bash
    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

  2. 克隆仓库并一键构建：

    bash
    git clone https://github.com/Ghost-Silver/SF-lean4.git
cd SF-lean4
lake build

  3. 进入沉浸式证明探索：

    • 打开 VS Code（安装官方扩展 Lean 4）或 Neovim（搭配 lean.nvim）；
    • 打开任何 .lean 源码（例如 SFLean4/LF/Basics.lean）；
    • 将光标移至任何标有 sorry 的习题中，右侧的 Infoview 即刻动态刷新待证目标上下文（Context & Goal）；
    • 替换 sorry，一步步享受绿灯通过、形式化消除所有不确定性的极致理智愉悦！

5. 结语与致谢：迈向形式化新时代 ​

数学与软件的本质是同一的——正如柯里-霍华德同构所揭示的那样，一段优雅严密的程序就是一个深邃命题的构造性证明。

我们谨向《Software Foundations》的原始创作者 Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Brent Yorgey 等学者致以最崇高的敬意；同时也对 Lean 4 社区与开源世界的先驱们表示由衷感谢。

SF-lean4 不仅是一个重制版项目，更是我们送给中文计算机科学社区与形式化验证爱好者的一份长久礼物。前路漫漫，形式化验证的黄金时代才刚刚拉开序幕。

欢迎在 GitHub 上为我们点亮一颗 ⭐️ Star，提交 Issue、提出改进建议，或者与我们一同踏上这场探索逻辑与真理的形式化远征！

“Proof is the idol before whom the pure mathematician tortures himself.”
—— 愿你在这片形式化世界中，找到探索真理的纯粹与宁静。

基于 MIT 与 Software Foundations 原版教育许可协议开源

Copyright © 2024-2026 Ghost-Silver · Software Foundations Authors