形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载本指南以仓库文档 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模块中的单子 APImonadic API辅助函数与高层操作定义在Tacmach与Tacticals模块中而面向最终用户的战术则主要定义在Tactics模块中。新引擎的三大支柱evar、evar_map 与目标状态部分证明项与 evar新引擎的根基是把证明表示为可以包含带类型洞的部分项。这些洞被称为evarexistential variable 的缩写存在变量。一个 evar 本质由它的上下文和返回类型确定记为?e : [Γ ⊢ _ : A]其中Γ是上下文A是类型。?e必须作用于一个类型为Γ的替换σ即一个项列表才能产出一个类型为A的项。这一步通过EConstr.mkEvar完成结果记为?e{σ}。需要说明的是?e{σ}这种应用替换的表达方式是整个引擎运转的基础战术生成的洞最终都要以这种方式被填充而填充的产物依然是一个合法的项从而保证了证明项的可构造性。evar_map单子中的全局状态证明引擎单子带有一份被称为evar_map的全局状态定义在Evd模块engine/evd.mli中。它是逐步细化incremental refinementevar的结构每生成一个新 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 按层次分布在如下模块中模块定位仓库路径Proofview引擎核心proofview 状态、a tactic单子类型、Goal 模块、聚焦与回溯原语engine/proofview.mliRefine底层 refine 原语用部分项填充目标洞proofs/refine.mliEvd低层evar_map结构操作不建议直接使用engine/evd.mliEvarutil生成与操纵 evar 的高层抽象原语engine/evarutil.mliEConstr带 evar 的项evar-contextualized terms表示engine/econstr.mliTacmach旧引擎风格的辅助函数如pf_ids_set_of_hypsproofs/tacmach.mliTacticals高层战术组合子Ltac 各原语的 ML 对应物tactics/tacticals.mliTactics面向最终用户的战术tactics/目录单子的三种基础运算在 engine/proofview.mli 中单子的基础运算被明确为Proofview.tclUNIT单子的return把值提升为战术Proofview.tclBIND单子的bindProofview.tclTHEN绑定在返回unit的战术上的特化形式即 Ltac 中分号;的语义。此外战术还支持完整回溯full backtracking一个战术可以有多个成功success若在返回第一个成功后遇到失败战术可回溯并使用第二个成功状态随之回退到先前的值。失败通过Proofview.tclZERO抛出tclOR/tclORELSE则用于引入回溯点与异常处理分支engine/proofview.mli。用 Refine.refine 编写底层战术签名与语义一个典型的底层战术通过把部分项塞进目标洞来实现使用的正是Refine模块的Refine.refine原语。其完整签名含文档注释如下proofs/refine.mlival 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的实际步骤取出当前目标的sigmaevar_map、env环境与concl结论通过Proofview.Unsafe.tclEVARS把当前状态切换到传入的 evar_map然后执行用户函数f生成部分项若typecheck为true则用typecheck_evar逐个检查新引入 evar 的假设与结论可类型化并用Typing.check env sigma c concl验证细化项c的类型确实匹配目标结论concl用Evarutil.occur_evar_upto检查目标本身没有出现在细化项中自引用检测否则报occur_check错误恢复 future goals 状态用Evd.define self c sigma把当前目标self定义为c用mark_as_goals把新洞标记为目标并通过tclSETGOALS设置新的聚焦目标列表。异常处理上refine内部通过Proofview.wrap_exceptionsengine/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分别取得目标的上下文Γ与结论ATacmach.pf_ids_set_of_hyps gl取目标上下文中所有假设的标识符集合该辅助函数定义于 proofs/tacmach.mli用于生成不与现有假设冲突的新名字Namegen.next_name_away Anonymous hyps在假设名集合之外生成一个新鲜标识符engine/namegen.mlimkArrowR 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_evarEvarutil.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其中值得关注的可选参数~srcevar 的来源供Evar_kinds记录与调试使用~candidates候选解列表evar 的解被限制在候选之中~namingevar 被自动化求解时引入的命名模式默认IntroAnonymous~typeclass_candidate标记该 evar 是否可作为类型类搜索的候选目标~relevanceevar 的 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 中确认存在组合子语义对应 LtactclIDTAC恒等战术什么都不做idtactclTHEN t1 t2顺序执行先t1再t2t1; t2tclTHENS t tl执行t后对产生的子目标逐个分派tlt; [t1 | ... | tn]tclTHENLIST tl依序执行列表中的战术t1; t2; ...tclMAP f l对列表l逐元素构造战术—tclTRY t尝试t失败则跳过不报错try ttclFIRST tl依次尝试直到第一个成功first [t1 | ...]tclORELSE t1 t2t1失败则执行t2t1 || t2tclIFTHENELSE c t e条件战术if c then t else etclDO n t把t重复执行n次do n ttclREPEAT t反复执行t直到失败repeat ttclSOLVE tl依次尝试直到有一个彻底解决当前目标solve [t1 | ...]tclPROGRESS t仅当t使目标发生实质变化时才算成功progress ttclFAIL msg以msg失败fail与 Proofview 原子组合子的差异需要特别区分Tacticals中的组合子与Proofview中同名但更原子的组合子语义并不完全相同tactics/tacticals.mli。例如Tacticals.tclORELSE把无进展lack of progress也视为失败而Proofview.tclORELSEengine/proofview.mli不会Tacticals中所有能捕获失败的组合子tclOR、tclORELSE、tclTRY、tclREPEAT等都会在每个目标上独立运行——失败与回溯被局部化到单个目标而不是影响整个目标列表。因此在编写跨目标行为时选择哪一层的组合子至关重要。新旧引擎对比为什么 Tacmach.refine 不可靠为完整起见文档对比了旧引擎旧引擎依赖Tacmach.refine提供类似功能但它是基于**无类型的 metauntyped 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.mlgeneric_refine全流程、engine/evarutil.mlievar 生成原语与 tactics/tacticals.mli组合子语义四个文件入手配合本文的cut示例自行实践。赞分享形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载相关推荐Chaos Mesh Workflow 内部设计深度解析基于 Kubernetes 声明式 API 的混沌实验编排引擎Chaos Mesh Workflow 内部设计深度解析基于 Kubernetes 声明式 API 的混沌实验编排引擎 本文是 Chaos Mesh 仓库内云原生运维测试可观测性Nixpkgs 中的 Rocq原 Coq打包与使用完全指南rocq-core、rocqPackages 与 mkRocqDerivationNixpkgs 中的 Rocq原 Coq打包与使用完全指南 rocq core 、 rocqPackages 与 mkRocqDerivation 导读包管理器操作系统Flowable DMN引擎API深度解析与实战指南Flowable DMN引擎API深度解析与实战指南 一、DMN引擎API概述 Flowable DMN引擎提供了一套完整的API体系用于管理和执行决策模型。后端工作流自动化流程编排上一篇Ray Data 核心概念全解Dataset、Block 与两阶段执行规划机制下一篇2025实测突破CSP限制的js-cookie安全存储终极方案创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考