Proof Repair across Quotient Type Equivalences

TL;DR

This paper extends an algorithm and tool for automatically repairing proofs in Rocq to handle quotient type equivalences, using setoid machinery to address changes in representations and implementations, with validation through case studies and formal proofs.

Contribution

It introduces novel extensions to proof repair algorithms and tools to support quotient type equivalences via setoid machinery in Rocq, enabling automated handling of behavioral changes.

Findings

Extended proof repair algorithm to support quotient type equivalences.

Automated proof repair tool now handles setoid-based changes.

Validated extensions through case studies and formal proofs in Cubical Agda.

Abstract

Proofs in proof assistants like Rocq can be brittle, breaking easily in response to changes. To address this, recent work introduced an algorithm and tool in Rocq 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 \emph{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 \emph{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 implementations of data structures. We extend this algorithm and tool to support quotient type equivalences in Rocq. Notably, since Rocq lacks quotient types entirely, our extensions use Rocq's setoid machinery in place of quotients. Specifically, (1) our extension to the algorithm supports new changes corresponding to setoids, and (2) our extension to the tool supports this new class of changes and further automates away some of the new proof obligations. We demonstrate our extensions on proof repair case studies for previously unsupported changes. We also perform manual proof repair in Cubical Agda, a language with a univalent metatheory, which allows us to construct the first ever internal proofs of correctness for proof repair.