Proofs in proof assistants like Coq can be brittle, breaking easily in response to changes in the terms and types those proofs depend on. To address this, recent work introduced an algorithm and tool in Coq to automatically repair broken proofs in response to changes that correspond to type equivalences. However, many changes remained out of the scope of this algorithm and tool -- especially changes in underlying behavior. We extend this proof repair algorithm so that it can express certain changes in behavior that were previously out of scope. We focus in particular on equivalences between quotient types -- types equipped with a relation that describes what it means for any two elements of that type to be equal. Quotient type equivalences can be used to express interesting changes in representations of mathematical structures, as well as changes in the underlying implementations of data structures -- two use cases highlighted by our case studies. We extend this algorithm to support quotient type equivalences in two different ways: (1) internally to cubical type theory (applied to Cubical Agda), and (2) externally to CIC$_{\omega}$ (applied to Coq). While our approach in Coq comes equipped with prototype automation, it suffers notably from Coq's lack of quotient types -- something we circumvent using Coq's setoid machinery and an extension to the proof repair algorithm to support the corresponding new proof obligations. In contrast, while our approach in Cubical Agda is completely manual, it takes advantage of cubical type theory's internal quotient types, which makes the algorithm straightforward. Furthermore, it includes the first internal proofs of correctness of repaired proofs, something not possible in general in Coq. We report on the tradeoffs between these two approaches, and demonstrate these tradeoffs on proof repair case studies for previously unsupported changes.

翻译：像Coq这样的证明助手中的证明往往具有脆弱性，当其所依赖的项和类型发生变化时容易失效。为此，近期研究提出了一种基于类型等价的Coq算法和工具，可自动修复因变化而损坏的证明。然而，许多变化——尤其是底层行为的变化——仍超出了该算法和工具的处理范围。本文扩展了这一证明修复算法，使其能够表达先前无法处理的特定行为变化。我们特别关注商类型之间的等价关系——商类型是配备了一种关系的类型，该关系定义了该类型中任意两个元素相等的含义。商类型等价可用于表达数学结构表示形式的有趣变化，以及数据结构底层实现的变化——这两类用例均在我们的案例研究中得到凸显。我们以两种不同方式扩展该算法以支持商类型等价：（1）在立体类型理论内部（应用于立体Agda）；（2）在CIC$_{\omega}$外部（应用于Coq）。虽然我们在Coq中的方法配备了原型自动化工具，但其显著受限于Coq缺乏商类型的问题——我们通过使用Coq的setoid机制和扩展证明修复算法以支持相应新增证明义务的方式规避了这一问题。相比之下，虽然我们在立体Agda中的方法完全依赖手动操作，但该方案充分利用了立体类型理论内置的商类型特性，使算法实现更为直接。此外，该方法还首次实现了修复后证明的内部正确性验证，这在Coq中通常难以实现。我们报告了这两种方法之间的权衡，并通过针对先前不支持变化的证明修复案例研究来展示这些权衡。