Why Rocq is better than Lean for program verification

为什么在程序验证领域，Rocq 比 Lean 更好

Especially now, with AI’s well-publicized success in mathematics, I get asked why I still use Rocq instead of giving in to the hype and switching to Lean. Most of this post started life as a provocatively titled slide in a recent LangSec keynote: “Why Rocq is better than Lean for program verification.” I am not trying to start a flame war here. If you are a more mature person than I am, feel free to mentally replace “better” with “a better fit for my work today” everywhere below. One more caveat before I start: this post is about program verification, not formalizing mathematics, where I will happily admit Lean has real momentum.

尤其是现在，随着人工智能在数学领域广为人知的成功，人们经常问我为什么仍然使用 Rocq，而不是屈服于炒作并转向 Lean。这篇文章的大部分内容最初源于我最近在 LangSec 主题演讲中一张标题颇具挑衅性的幻灯片：“为什么 Rocq 在程序验证方面比 Lean 更好”。我并不是想引发一场口水战。如果你比我更成熟，请随意在下文中将“更好”替换为“更适合我当前的工作”。在开始之前还有一个免责声明：本文讨论的是程序验证，而不是数学形式化——我乐于承认 Lean 在数学形式化方面确实势头强劲。

Language-level issues: Coinductive types and cofixpoints

语言层面的问题：共归纳类型与共定点

Wojciech Różowski and Joachim Breitner of Lean FRO developed support for coinductive predicates in Lean. Their feature made it into Lean 4.25 as the coinductive command (implementation). It is useful for bisimulations and other coinductive proofs, but it does not provide executable cofixpoints or programs that can be extracted. I also want codata in Type that I can actually run. Rocq gives me that directly with CoInductive and CoFixpoint. Lean has no corresponding declarations in Type; its alternatives use ordinary functions and structures or library encodings.

Lean FRO 的 Wojciech Różowski 和 Joachim Breitner 开发了对 Lean 中共归纳谓词的支持。他们的功能已作为 coinductive 命令（实现）进入 Lean 4.25。它对于双模拟（bisimulations）和其他共归纳证明很有用，但它不提供可执行的共定点（cofixpoints）或可提取的程序。我还需要可以在 Type 中实际运行的共数据（codata）。Rocq 通过 CoInductive 和 CoFixpoint 直接为我提供了这一点。Lean 在 Type 中没有相应的声明；其替代方案使用的是普通函数、结构体或库编码。

The closest Lean experiment I found to a Rocq-style codata declaration is Alex Keizer’s QPFTypes, a proof-of-concept package for generic codata. Its codata command turns a specification into a library encoding and generates destructor, corecursor, and bisimulation principles. Unlike Rocq’s CoInductive, it is not a kernel declaration. The examples use QPFTypes’ pinned Lean 4.25.0 toolchain (latest supported at the time of the post).

我发现最接近 Rocq 风格共数据声明的 Lean 实验是 Alex Keizer 的 QPFTypes，这是一个用于通用共数据的概念验证包。它的 codata 命令将规范转换为库编码，并生成析构器、共递归器和双模拟原理。与 Rocq 的 CoInductive 不同，它不是内核声明。这些示例使用了 QPFTypes 锁定的 Lean 4.25.0 工具链（本文撰写时支持的最新版本）。

Declaring codata

声明共数据

I do not mean this as a dunk on QPFTypes: it says “proof of concept” right there in the readme. But the rough edges show up quickly in examples that are completely ordinary in Rocq. For instance, Rocq accepts this parameterless coinductive type directly:

我并不是要贬低 QPFTypes：它的自述文件中明确写着“概念验证”。但在 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 -/

This one can be written off as an implementation bug but the next two are structural. Mutually coinductive declarations are routine in Rocq but not supported by QPFTypes:

这可以归咎于实现错误，但接下来的两个是结构性的。相互共归纳声明在 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 -/

Indexed coinductive families are also part of Rocq’s ordinary coinductive fragment but outside the QPF encoding. In this example, the index is a clock that advances at each step; the same pattern occurs with protocols, phases, sizes, and state machines:

索引共归纳族也是 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 -/

Under the hood, QPFTypes generates Cofix machinery. The codata command hides most of it for simple, non-mutual, non-indexed cases, but once I leave that fragment I am either calling the low-level MvQPF.Cofix.corec and bisim API myself or I am out of luck. In Rocq, the examples above are just declarations. Rocq’s direct support is not painless; anyone who has argued with its guardedness checker knows that. On the proof side, Rocq users also have mature tools such as Paco and Damien Pous’s coinduction library. They help with coinductive predicates and relations, but they do not replace CoFixpoint for programs.

在底层，QPFTypes 生成了 Cofix 机制。对于简单的、非相互的、非索引的情况，codata 命令隐藏了大部分细节，但一旦超出这个范围，我就必须自己调用底层的 MvQPF.Cofix.corec 和 bisim API，否则就无能为力了。在 Rocq 中，上述示例仅仅是声明。Rocq 的直接支持并非没有痛苦；任何与它的守卫检查器（guardedness checker）打过交道的人都知道这一点。在证明方面，Rocq 用户还有 Paco 和 Damien Pous 的共归纳库等成熟工具。它们有助于处理共归纳谓词和关系，但不能替代程序中的 CoFixpoint。

Extracting cofixpoints

提取共定点

A native Rocq cofixpoint extracts to an actual lazy OCaml value. For example, in the game tree library I worked on, the Rocq unfold_cotree function extracts to:

原生的 Rocq 共定点可以提取为实际的惰性 OCaml 值。例如，在我参与的游戏树库中，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))))

With QPFTypes, construction and observation instead go through the generic MvQPF.Cofix.corec and MvQPF.Cofix.dest operations. The program keeps the generic Cofix representation rather than becoming the direct lazy tree above. That is fine as mathematics, but it is not the program I would write by hand.

使用 QPFTypes，构造和观察必须通过通用的 MvQPF.Cofix.corec 和 MvQPF.Cofix.dest 操作。程序保留了通用的 Cofix 表示，而不是变成上面那种直接的惰性树。作为数学这没问题，但这不是我会手写的程序。

Current Lean alternatives

当前的 Lean 替代方案

At this point, a Lean programmer may be shouting at the screen: nobody reaches for QPFTypes just to write a stream. Fair enough. QPFTypes is here because it comes closest to a Rocq-style codata declaration. Day-to-day Lean uses several other tricks. For streams, mathlib’s Stream' is the obvious answer. It is just Nat → α: ask for position n and get an element back. It runs, and mathlib supplies corecursors along with extensionality, bisimulation, and coinduction lemmas, so it is pleasant to prove things about. But it is not a lazy constructor whose tail is another stream.

此时，一位 Lean 程序员可能会对着屏幕大喊：没人会为了写一个流而去用 QPFTypes。说得对。之所以提到 QPFTypes，是因为它最接近 Rocq 风格的共数据声明。日常的 Lean 开发使用其他几种技巧。对于流，mathlib 的 Stream' 是显而易见的答案。它只是 Nat → α：询问位置 n 并返回一个元素。它可以运行，并且 mathlib 提供了共递归器以及外延性、双模拟和共归纳引理，因此证明起来很方便。但它不是一个尾部是另一个流的惰性构造器。