Proof Repair across Type Equivalences

TL;DR

This paper introduces PUMPKIN Pi, a novel proof repair method for Coq that automatically adapts proofs to type changes using proof term transformations and a decompiler, improving proof maintenance and interoperability.

Contribution

It presents a new approach combining proof term transformation and decompiler techniques for proof repair across type equivalences in Coq, implemented in the PUMPKIN Pi tool.

Findings

Successfully repaired proofs in eight diverse case studies.

Enhanced proof development with dependent types and type porting.

Facilitated interoperability between Coq and other verification tools.

Abstract

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.