为何Rocq在程序验证上优于Lean

# 为什么Rocq在程序验证方面比Lean更好 来源：https://joomy.korkutblech.com/posts/2026-07-28-why-rocq-is-better.html 尤其是在当下，AI在数学领域取得了广为人知的成功，我常被人问起为什么还在用Rocq（https://rocq-prover.org/），而不是屈服于潮流转向Lean（https://lean-lang.org/）。这篇文章的大部分内容最初源于我最近在LangSec（https://langsec.org/spw26/abstracts.html）主题演讲中一张标题颇具挑衅性的幻灯片：“为什么Rocq在程序验证方面比Lean更好”。 我并非想挑起论战。如果你比我更成熟，请随意将下文中的“更好”在脑海中替换为“更适合我当前的工作”。在开始之前还有一个提醒：这篇文章是关于*程序*验证的，而非形式化数学——在数学领域，我欣然承认Lean确实势头正盛。 ## 语言层面问题 ### 余归纳类型与余不动点 Lean FRO的Wojciech Różowski和Joachim Breitner开发了Lean中的余归纳谓词（https://www.youtube.com/watch?v=vEt07N_v-Yo）支持。他们的功能作为`coinductive`命令（实现（https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Coinductive.lean））被纳入Lean 4.25（https://lean-lang.org/doc/reference/latest/releases/v4.25.0/）。这对于互模拟和其他余归纳证明很有用，但它不提供可执行的余不动点或可提取的程序。 我还希望在`Type`中拥有真正可以运行的余数据。Rocq通过`CoInductive`和`CoFixpoint`直接提供这一点。Lean在`Type`中没有对应的声明；它的替代方案使用普通函数和结构体或库编码。 我找到的最接近于Rocq风格余数据声明的Lean实验是Alex Keizer的QPFTypes（https://github.com/alexkeizer/QPFTypes），一个用于通用余数据的概念验证包。它的`codata`命令将规范转化为库编码，并生成析构器、余递归器和互模拟原理。与Rocq的`CoInductive`不同，它不是内核声明。示例使用了QPFTypes固定的Lean 4.25.0工具链（截至本文发布时支持的最新版本）。 #### 声明余数据 我并非在贬低QPFTypes：它的readme里明确写着“概念验证”。但粗糙之处在那些Rocq中完全普通的例子里很快就暴露无遗。例如，Rocq直接接受这个无参数余归纳类型： `` CoInductive co_unit : Type := | co_unit_loop : co_unit. `` `` codata CoUnit where | loop : CoUnit /-- error: Due to a bug, codatatype without any parameters don't quite work yet. Please try adding parameters to your type -/ `` 这个可以归咎于实现bug，但接下来的两个是结构性的。相互递归的余归纳声明在Rocq中是常规操作，但QPFTypes不支持： `` CoInductive tree (a : Type) : Type := | node : a -> forest a -> tree a with forest (a : Type) : Type := | fnil : forest a | fcons : tree a -> forest a -> forest a. `` `` mutual codata Tree α where | node : α → Forest α → Tree α codata Forest α where | fnil : Forest α | fcons : Tree α → Forest α → Forest α end /-- error: invalid mutual block: either all elements of the block must be inductive/structure declarations, or they must all be definitions/ theorems/abbrevs -/ `` 带索引的余归纳族也是Rocq普通余归纳片段的一部分，但不在QPF编码范围内。在这个例子中，索引是一个每一步都会递增的时钟；同样的模式出现在协议、阶段、大小和状态机中： `` CoInductive istream (a : Type) : nat -> Type := | icons : forall n, a -> istream a (S n) -> istream a n. `` `` codata IStream α : Nat → Type where | icons : α → IStream α (n + 1) → IStream α n /-- error: Unexpected type; type will be automatically inferred. Note that inductive families are not supported due to inherent limitations of QPFs -/ `` 在底层，QPFTypes生成`Cofix`机制。对于简单的、非相互递归的、非带索引的情况，`codata`命令隐藏了大部分细节，但一旦离开这个范畴，我就要么自己调用底层的`MvQPF.Cofix.corec`和`bisim`API，要么就没辙了。而在Rocq中，上面的例子仅仅是声明而已。 Rocq的直接支持也并非没有痛苦；任何与它的守卫性检查器争执过的人都明白这一点。在证明方面，Rocq用户还有成熟的工具，如Paco（https://github.com/snu-sf/paco）和Damien Pous的coinduction（https://github.com/damien-pous/coinduction）库。它们有助于处理余归纳谓词和关系，但不能替代程序中的`CoFixpoint`。 一个原生的Rocq余不动点会提取成一个实际的惰性OCaml值。例如，在我参与的对弈树库（https://github.com/bloomberg/game-trees）中，Rocq的`unfold_cotree`函数提取为： `` type 'a cotree = 'a __cotree Lazy.t and 'a __cotree = | Conode of 'a * 'a cotree colist (* other definitions ... *) (** val unfold_cotree : ('a1 -> 'a1 colist) -> 'a1 -> 'a1 cotree **) let rec unfold_cotree next init = lazy (Conode (init, (comap (unfold_cotree next) (next init)))) `` 使用QPFTypes，构造和观察则通过通用的`MvQPF.Cofix.corec`和`MvQPF.Cofix.dest`操作进行。程序保持通用的`Cofix`表示，而不会变成上面那样的直接惰性树。这在数学上没问题，但并非我手写会写出的程序。 如果你想亲自尝试QPFTypes，BadCoinduction.lean（https://joomy.korkutblech.com/assets/why-rocq-is-better/BadCoinduction.lean）包含了本章节背后的完整实验：可用的`Colist`和`Cotree`定义、生成接口的示例，以及针对无参数、相互递归和带索引余数据的检查失败案例。其头部记录了确切的QPFTypes提交和重新运行测试所需的命令。 #### 当前Lean的替代方案 此时，可能有Lean程序员在对屏幕大喊：没人为了写一个流而去用QPFTypes。好吧，有道理。这里提到QPFTypes是因为它最接近Rocq风格的余数据声明。日常的Lean使用其他几种技巧。 对于流，mathlib的`Stream'`（https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Stream/Defs.html）是显而易见的答案。它只是`Nat → α`：询问位置`n`，然后得到一个元素。它可以运行，并且mathlib提供了余递归器以及外延性、互模拟和余归纳引理，因此用它来证明东西很愉快。但它不是一个尾部是另一个流的惰性构造器。它能解决流的问题，但不能解决任意的相互递归或带索引的余数据。 另一种选择是显式的状态机：维持一些状态，编写一个步进函数，并将其用作余递归器。Lean当前的`Iter`接口（https://lean-lang.org/doc/reference/latest/Iterators/）将此模式封装成序列，并按需一步一步计算。一个迭代器可以携带一个`Productive`（https://lean-lang.org/doc/reference/latest/Iterators/Iterator-Definitions/#finite-and-productive-iterators）证明，表明它最终会产生一个值或结束；`Iter.repeat`已经拥有了一个。使用自定义迭代器，我必须自己提供步进接口、其不变式，以及可能的生产性证明。这可行，但现在我正在自己处理状态机和序列之间的连接工作。而Rocq的`CoFixpoint`会检查其递归调用的守卫性，并直接给我余归纳值。 `Thunk`（https://lean-lang.org/doc/reference/latest/Basic-Types/Lazy-Computations/）提供了惰性，但不提供余归纳。编译后的Lean会延迟一个thunk直到被强制求值，然后缓存结果。逻辑层面看到的是一个`Unit → α`，这意味着涉及thunk的全函数定义仍然对证明可用，尽管缓存是不可见的。Thunk既不允许递归，也不检查递归最终是否产生构造器。提取后的Rocq余不动点在其递归通过守卫性检查器之后，才使用类似的运行时惰性。 `partial def`（https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#partial-functions）是粗暴的工具。编译器运行递归体，但逻辑只得到一个不透明的常量。Lean在这里既不检查终止性也不检查生产性；它同时接受一个thunk化的自然数生产者和一个立即无限自调用的生产者。`unsafe def`也可以运行，但定理安全的声明完全不能引用它。Batteries的`MLList`（https://github.com/leanprover-community/batteries/blob/main/Batteries/Data/MLList/Basic.lean）展示了通常的安排：一个私有的unsafe惰性实现，一个不透明的公共接口，以及作为`partial def`编写的生产者（如`fix`和`iterate`）。这些生产者无法像被观察的Rocq余不动点那样在证明中被展开。Lean还有`partial_fixpoint`（https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#partial-fixpoints），它保留了等式，但它不接受这种构造器和thunk的递归。 QPFTypes避免了这种不透明性：它提供了余递归器和互模拟原理。但这样一来，我又回到了它通用的`Cofix`表示以及我之前测试过的声明限制。 为什么我要担心流之外的东西？交互树。Rocq中的interaction trees（https://github.com/DeepSpec/InteractionTrees）库将副作用、可能非终止的程序表示为余归纳树。我可以使用它们编写程序，解释和提取这些程序，并证明关于同一棵树（通常是在弱互模拟意义下）的等式。`Stream'`和`Iter`只给我序列，而不是实现效果所需的分支延续。我可以使用`Thunk`和`partial def`运行一个手写的效果树，但那样递归生产者对证明就是不透明的。要在Lean中获得所有这些，需要一个余数据的库编码。 MIT PLV的lean4-itree（https://github.com/mit-plv/lean4-itree）使用Mathlib的`PFunctor.M`最终余代数实现了这一点用于交互树。较新的PolyFun（https://github.com/Verified-zkEVM/PolyFun）增加了处理器、递归过程、踪迹、强互模拟和弱互模拟，以及单子律和迭代律的证明。我可以在Lean中用这些树进行计算并证明关于它们的性质。不过，它们仍然是库编码的M类型。Lean在这里没有原生的余数据声明，计算保留了通用表示，而不是产生Rocq提取出的那种直接惰性程序。 HITrees（https://arxiv.org/abs/2510.14558）并非解决此问题的途径。作者考虑了ITrees使用的余归纳Delay单子方法，但Lean缺乏原生余归纳类型排除了这种可能性。他们的树反而是归纳的，非终止性变成了一个高阶递归效果。一个递归计算不再是我可以观察和展开的无限树；它的递归只有在处理器解释该效果时才获得意义。单子解释可以运行它，证明可以通过状态机解释进行，但HITree等式理论不提供通常的递归展开等式。它可行。但它也将非终止性从树中移到了解释器里，我觉得这比编写一个受守卫的Rocq余不动点更别扭。 使用Lean，我必须放弃其中一些东西，或者在通用机制之上重建它们。Rocq让我声明余数据，编写受守卫的生产者，通过观察推理它，并提取直接的惰性代码。这就是我从余归纳中想要的东西。 ### 嵌套归纳类型与谓词 Meven Lennon-Bertrand向我指出了这一点（https://lipn.info/@mevenlennonbertrand/116608679656852130），我对下面的例子做了扩展。Lean接受许多嵌套归纳定义，但其检查器拒绝一些Rocq接受的定义。我在撰写我的证明珍珠*A Rose Tree Is Blooming*（https://joomy.korkutblech.com/papers/game-trees-cpp26.pdf）时遇到了这个问题，该文依赖于Rocq的这一部分，如果改用Lean编写会难看得多。玫瑰树例子对于这篇文章来说太大了，所以这里用JSON模式展示同样的问题。 假设你有一个JSON模式语言，想要证明关于验证的常见性质：字段名匹配、从模式中删除字段是安全的、验证前缀可行。如果你在构建一个经过验证的系统，这都是常规工作。在两种语言中定义JSON和模式都没有问题： `` Inductive json : Type := | jnull : json | jstr : string -> json | jnum : nat -> json | jarr : list json -> json | jobj : list (string * json) -> json. Inductive schema : Type := | sany : schema | sstr : schema | snum : schema | sarr : schema -> schema | sobj : list (string * schema) -> schema. `` `` inductive JSON where | null : JSON | str : String → JSON | num : Nat → JSON | arr : List JSON → JSON | obj : List (String × JSON) → JSON inductive Schema where | any : Schema | strS : Schema | numS : Schema | arrS : Schema → Schema | objS : List (String × Schema) → Schema `` 有趣的部分是验证关系。一个对象模式如`\{ "name": string, "age": number \}`应该通过成对检查字段名匹配且每个值针对相应子模式验证，来验证对象`\{ "name": "Alice", "age": 30 \}`。Rocq可以将所有这些存储在一个`Forall2`（https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Lists.List.html#Forall2）推导中： `` Inductive valid : schema -> json -> Prop := | valid_any : forall j, valid sany j | valid_str : forall s, valid sstr (jstr s) | valid_num : forall n, valid snum (jnum n) | valid_arr : forall elem_schema elems, Forall (fun j => valid elem_schema j) elems -> valid (sarr elem_schema) (jarr elems) | valid_obj : forall schema_fields json_fields, Forall2 (fun (sf : string * schema) (jf : string * json) => fst sf = fst jf /\ valid (snd sf) (snd jf)) schema_fields json_fields -> valid (sobj schema_fields) (jobj json_fields). `` 使用投影是刻意的。Rocq 9.0拒绝了围绕递归出现使用等价元组模式lambda的做法，因为它不是严格正值的；它的语法检查器无法看透那个模式匹配。上面基于投影的声明可以编译。 Lean 4.32.1拒绝了对应的对象构造器： `` inductive ValidCombined : Schema → JSON → Prop where | obj : Forall2 (fun (sf : String × Schema) (jf : String × JSON) => sf.1 = jf.1 ∧ ValidCombined sf.2 jf.2) schemaFields jsonFields → ValidCombined (.objS schemaFields) (.obj jsonFields) `` `` error: (kernel) invalid nested inductive datatype 'And', nested inductive datatypes parameters cannot contain local variables. `` Lean接受几种相近的形式：`Forall2 ParRed`、通过`And`和`Exists`的直接递归，以及`Forall2 \(fun sf jf =\> Valid sf\.2 jf\.2\)`。在被拒绝的声明中，递归出现同时通过了`Forall2`和`And`，内核报告了内部的`And`。另一种情况，`Forall2 \(Eval env\)`，在`Forall2`处失败，因为其关系参数捕获了构造器局部的`env`。 Lean可以通过将组合关系拆分为两个`Forall2`推导来保留列表结构： `` inductive Valid : Schema → JSON → Prop where | obj : Forall2 (fun (sf : String × Schema) (jf : String × JSON) => sf.1 = jf.1) schemaFields jsonFields → Forall2 (fun (sf : String × Schema) (jf : String × JSON) => Valid sf.2 jf.2) schemaFields jsonFields → Valid (.objS schemaFields) (.obj jsonFields) `` 不需要索引或单独的长度证明。删除头部仍然是结构性的，尽管Lean必须解构两个推导： `` Lemma Forall2_tail : forall (A B : Type) (R :