论文标题
跨类型等价修理
Proof Repair across Type Equivalences
论文作者
论文摘要
我们描述了一种新方法，可以自动修复COQ证明助手中的破损证明，以应对类型的变化。我们的方法将可配置的证明术语转换与从证明术语到战术脚本的反编译器结合在一起。证明术语转换以删除对更改类型的旧版本的引用的方式实现了跨等价的传输，并且不依赖于这些COQ假设以外的公理。 我们已经在南瓜PI中实现了这种方法，这是南瓜补丁Coq插件套件的扩展，以进行证明维修。我们证明了南瓜Pi对八个案例研究的灵活性，包括支持用户研究的基准，以依赖类型，移植功能和一单二进制数字之间的证明，并支持工业证明工程师在COQ和其他验证工具之间进行互操作。
We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes. We have implemented this approach in PUMPKIN Pi, an extension to the PUMPKIN PATCH Coq plugin suite for proof repair. We demonstrate PUMPKIN Pi's flexibility on eight case studies, including supporting a benchmark from a user study, easing development with dependent types, porting functions and proofs between unary and binary numbers, and supporting an industrial proof engineer to interoperate between Coq and other verification tools more easily.
