Proof repair across type equivalences
Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman
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 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.
Topics & Concepts
Mathematical proofProof assistantAxiomTerm (time)Structural proof theoryProof theoryMathematicsType theoryDirect proofProgramming languageTransformation (genetics)Type (biology)Proof complexityComputer scienceAlgebra over a fieldCalculus (dental)Automated proof checkingNatural deductionDiscrete mathematicsFormal proofAutomated theorem provingDependent typeProof of conceptTheoretical computer scienceCombinatorial proofGas meter proverAlgorithmMathematical logicConstructive proofSecurity and Verification in ComputingLogic, programming, and type systemsFormal Methods in Verification