企业官网建设流程全解析

• 形式化验证
• 编程语言

本指南以仓库文档 dev/doc/proof-engine.md 为骨架，系统讲解 Rocq Prover（原 Coq）自 8.5 版本起引入的全新证明引擎：它如何以Proofview单子 API 取代旧 meta 引擎，如何用evar（存在变量）表示含类型洞的部分证明项，以及如何通过Refine.refine与Tacticals组合子编写可靠、可组合的 ML 战术。读完本文，你将掌握新引擎的底层概念、cut战术的完整实现范式，以及旧引擎Tacmach.refine为何被取代的深层原因。

为什么需要新证明引擎：旧 meta 引擎的困境

从 Coq 8.5 开始，Rocq 引入了一套全新的证明引擎，替代旧的基于 meta 的引擎。旧引擎在表达力与健全性两方面都有诸多缺陷，其中最主要的一条是：战术的类型是透明的（the type of tactics was transparent）。这一点被广泛滥用，使得几乎不可能在不破坏外部战术的情况下调整引擎的底层实现——引擎的任何内部改动都可能因为战术直接依赖其具体结构而失效。

正因如此，旧引擎被标记为已弃用（deprecated），并正在从源码中逐步移除。新引擎的核心是一个定义在Proofview模块中的单子 API（monadic API）；辅助函数与高层操作定义在Tacmach与Tacticals模块中，而面向最终用户的战术则主要定义在Tactics模块中。

新引擎的三大支柱：evar、evar_map 与目标状态

部分证明项与 evar

新引擎的根基，是把证明表示为可以包含带类型洞的部分项。这些洞被称为evar（existential variable 的缩写，存在变量）。一个 evar 本质由它的上下文和返回类型确定，记为：

?e : [Γ ⊢ _ : A]

其中Γ是上下文，A是类型。?e必须作用于一个类型为Γ的替换σ（即一个项列表），才能产出一个类型为A的项。这一步通过EConstr.mkEvar完成，结果记为?e{σ}。

需要说明的是，?e{σ}这种"应用替换"的表达方式是整个引擎运转的基础：战术生成的洞最终都要以这种方式被"填充"，而填充的产物依然是一个合法的项，从而保证了证明项的可构造性。

evar_map：单子中的全局状态

证明引擎单子带有一份被称为evar_map的全局状态，定义在Evd模块（engine/evd.mli）中。它是逐步细化（incremental refinement）evar的结构：每生成一个新 evar、每给一个 evar 定义解，都会反映在evar_map的更新中。

Evd是一个底层 API，官方不鼓励直接使用，而推荐使用Evarutil模块（engine/evarutil.mli）提供的更抽象的原语——这一点在编写战术时尤为重要，因为它避免了直接操作evar_map的内部表示。

目标状态：洞的有序列表

除了evar_map，单子还携带一份目标状态（goal state）：一个待填充洞的有序列表。在足够高的抽象层次上，这些洞被称为"目标（goals）"，但本质上它们不过就是 evar。处理这些洞的 API 位于Proofview.Goal模块中。

由于战术天然地同时作用于多个目标，通常的做法是使用Proofview.Goal.enter及其变体，把战术分派（dispatch）到当前聚焦的每一个目标上。这正是enter的核心语义——在 engine/proofview.mli 中，enter t会在每个目标上独立地应用目标相关战术t，且把当前目标作为参数传入。

模块地图：从 Proofview 到 Tactics

新引擎的 API 按层次分布在如下模块中：

单子的三种基础运算

在 engine/proofview.mli 中，单子的基础运算被明确为：

• Proofview.tclUNIT：单子的"return"，把值提升为战术；
• Proofview.tclBIND：单子的"bind"；
• Proofview.tclTHEN：绑定在返回unit的战术上的特化形式，即 Ltac 中分号;的语义。

此外，战术还支持完整回溯（full backtracking）：一个战术可以有多个成功（success），若在返回第一个成功后遇到失败，战术可回溯并使用第二个成功；状态随之回退到先前的值。失败通过Proofview.tclZERO抛出，tclOR/tclORELSE则用于引入回溯点与异常处理分支（engine/proofview.mli）。

用 Refine.refine 编写底层战术

签名与语义

一个典型的底层战术，通过把部分项"塞进"目标洞来实现，使用的正是Refine模块的Refine.refine原语。其完整签名（含文档注释）如下（proofs/refine.mli）：

val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic (** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)

refine的执行流程是：先在当前证明状态下求值参数t，再把得到的项作为当前聚焦目标的填充物。所有由这个 thunk 调用新创建的 evar，会按创建顺序被转化为新的目标，追加到目标状态中。因此refine是一种目标相关（goal-dependent）战术：它只能作用于当前聚焦的目标。

底层实现剖析

从源码 proofs/refine.ml 可以看出generic_refine的实际步骤：

1. 取出当前目标的sigma（evar_map）、env（环境）与concl（结论）；
2. 通过Proofview.Unsafe.tclEVARS把当前状态切换到传入的 evar_map，然后执行用户函数f生成部分项；
3. 若typecheck为true，则用typecheck_evar逐个检查新引入 evar 的假设与结论可类型化，并用Typing.check env sigma c concl验证细化项c的类型确实匹配目标结论concl；
4. 用Evarutil.occur_evar_upto检查目标本身没有出现在细化项中（自引用检测），否则报occur_check错误；
5. 恢复 future goals 状态，用Evd.define self c sigma把当前目标self定义为c；
6. 用mark_as_goals把新洞标记为目标，并通过tclSETGOALS设置新的聚焦目标列表。

异常处理上，refine内部通过Proofview.wrap_exceptions（engine/proofview.mli）捕获求值期间抛出的异常并转化为战术失败，这保证了战术失败与 OCaml 异常的语义隔离。注意Proofview.Goal.sigma、Proofview.Goal.env、Proofview.Goal.concl等访问器定义于 engine/proofview.mli。

实战：用 refine 实现 cut 战术

下面以cut战术为理想化示例，完整演示Proofview.Goal.enter与Refine.refine的组合用法（代码逐行取自 dev/doc/proof-engine.md）。

假设X是一个类型，cut X会把当前目标[Γ ⊢ _ : A]填充为如下项：

let x : X := ?e2{Γ} in ?e1{Γ} x

其中x是新变量，?e1 : [Γ ⊢ _ : X -> A]、?e2 : [Γ ⊢ _ : X]。当前目标由此被解决，两个新洞[e1, e2]按此顺序加入目标状态。

let cut c = Proofview.Goal.enter begin fun gl -> (* In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (* Get the context of the goal, essentially [Γ] *) let concl = Proofview.Goal.concl gl in (* Get the conclusion [A] of the goal *) let hyps = Tacmach.pf_ids_set_of_hyps gl in (* List of hypotheses from the context of the goal *) let id = Namegen.next_name_away Anonymous hyps in (* Generate a fresh identifier *) let t = mkArrowR c (Vars.lift 1 concl) in (* Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) Refine.refine ~typecheck:true begin fun sigma -> (* All evars generated by this block will be added as goals *) let sigma, f = Evarutil.new_evar env sigma t in (* Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. *) let sigma, x = Evarutil.new_evar env sigma c in (* Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Context.annotR (Name id), x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in (* Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) (sigma, r) end end

逐段解读

• Proofview.Goal.enter：进入"每目标一次"的上下文。回调gl代表当前聚焦的一个目标；
• Proofview.Goal.env gl/Proofview.Goal.concl gl：分别取得目标的上下文Γ与结论A；
• Tacmach.pf_ids_set_of_hyps gl：取目标上下文中所有假设的标识符集合（该辅助函数定义于 proofs/tacmach.mli），用于生成不与现有假设冲突的新名字；
• Namegen.next_name_away Anonymous hyps：在假设名集合之外生成一个新鲜标识符（engine/namegen.mli）；
• mkArrowR c (Vars.lift 1 concl)：构造X -> A。注意A位于箭头右侧，因此需要做一次lift 1的变量提升——这是依赖类型下编写项时最常见的坑；
• Evarutil.new_evar env sigma t：生成类型为t的新 evar?e1并返回可直接使用的项f（含恒等替换?e1{Γ}）。文档特别提醒：必须传入正确的env上下文，恒等替换是从env中提取的，若上下文传错，得到的项将无法通过类型检查；
• mkLetIn (Context.annotR (Name id), x, c, mkApp (Vars.lift 1 f, [|mkRel 1|]))：把?e2{Γ}绑定为let id : X := ?e2{Γ} in ?e1{Γ} id，其中f再次lift 1以进入let体，mkRel 1引用刚绑定的变量；
• (sigma, r)：返回更新后的sigma与构造好的部分项，交给Refine.refine完成对当前目标的填充，?e1、?e2依创建顺序成为新子目标。

深入 Evarutil.new_evar

Evarutil.new_evar是战术中生成 evar 的首选方式。它直接返回一个"即用型"项（含恒等替换），无需再调用底层的EConstr.mkEvar原语。其完整签名（engine/evarutil.mli）为：

val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?relevance:ERelevance.t -> ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?parent:Evar.t -> ?typeclass_candidate:bool -> ?rrpat:bool -> env -> evar_map -> types -> evar_map * EConstr.t

其中值得关注的可选参数：

• ~src：evar 的来源（供Evar_kinds记录与调试使用）；
• ~candidates：候选解列表，evar 的解被限制在候选之中；
• ~naming：evar 被自动化求解时引入的命名模式（默认IntroAnonymous）；
• ~typeclass_candidate：标记该 evar 是否可作为类型类搜索的候选目标；
• ~relevance：evar 的 relevance 标记。

若确实需要非恒等替换等特殊场景，才应使用new_pure_evar等更低层的变体（engine/evarutil.mli）。使用new_evar时同样必须小心传对env：它生成的 evar 与项只有在"将被插入的上下文"中才有意义。

高层战术组合：Tacticals

低层 refine 战术可以组合出更强大的抽象。文档明确指出：在旧引擎中，组合低层战术是被迫的做法（因为只能走有限的推导规则集合），而在新引擎中，只要可能且足够容易，就应尽量在 ML 战术中通过 refine 直接生成证明项——这能避免依赖如 unification 这类脆弱的构造。

当然，这并不禁止使用 tacticals 去复刻 Ltac 的写法。每一个 Ltac 原语都有语义简单的 ML 对应物，全部罗列在Tacticals模块中（tactics/tacticals.mli）。它们大多是从旧引擎移植到新引擎的，同名即同义：如果新旧引擎中的 tactical 共享名字，就应当具有相同的语义。

常用组合子一览

以下组合子均已在 tactics/tacticals.mli 中确认存在：

与 Proofview 原子组合子的差异

需要特别区分：Tacticals中的组合子与Proofview中同名（但更原子）的组合子语义并不完全相同（tactics/tacticals.mli）。例如：

• Tacticals.tclORELSE把"无进展（lack of progress）"也视为失败，而Proofview.tclORELSE（engine/proofview.mli）不会；
• Tacticals中所有能捕获失败的组合子（tclOR、tclORELSE、tclTRY、tclREPEAT等）都会在每个目标上独立运行——失败与回溯被局部化到单个目标，而不是影响整个目标列表。

因此在编写跨目标行为时，选择哪一层的组合子至关重要。

新旧引擎对比：为什么 Tacmach.refine 不可靠

为完整起见，文档对比了旧引擎：旧引擎依赖Tacmach.refine提供类似功能，但它是基于**无类型的 meta（untyped metas）**而非 evar 的。因为没有类型信息，旧引擎不得不"篡改"参数项以真正产生要填入洞中的项：

• 为了绕过无类型问题，部分 meta 必须借助cast（强制类型转换）来约束其类型，否则会在运行时出错；
• 这套做法在非常简单的场景下勉强可用，但对其他一切场景都不可靠。

这正是新引擎改用 evar 的根本动因：evar 携带完整的上下文与类型信息，?e : [Γ ⊢ _ : A]本身就是类型正确的部分项，细化过程无需也不应再对项做脆弱的"修补"。源码层面，当前仓库中 proofs/tacmach.mli 仅保留了pf_get_new_id、pf_ids_set_of_hyps这类纯辅助函数，而核心的证明推进逻辑已完全迁移到Refine与Proofview体系。

小结

• 新证明引擎（Coq 8.5 起引入，Rocq 延续使用）以Proofview单子为核心：'a tactic是抽象类型，evar_map是全局状态，目标状态是待填充 evar 的有序列表；
• Refine.refine是底层战术的推荐入口：求值部分项、填入目标、新洞按序成为子目标，并支持可选的预类型检查；
• Evarutil.new_evar是生成 evar 的首选原语，直接返回即用项，只需注意传入正确的env上下文；
• Tacticals提供与 Ltac 一一对应的 ML 组合子，且在与Proofview原子组合子同名时需注意回溯与失败语义的差异；
• 旧 meta 引擎因战术类型透明、meta 无类型而不可靠，已弃用并逐步移除。

对希望深入源码的读者，建议从 engine/proofview.mli（单子与 Goal 模块）、proofs/refine.ml（generic_refine全流程）、engine/evarutil.mli（evar 生成原语）与 tactics/tacticals.mli（组合子语义）四个文件入手，配合本文的cut示例自行实践。

• 形式化验证
• 编程语言