Proof repair across type equivalences
Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman · 2021
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 suggested 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.