Proof Repair across Quotient Type Equivalences
arxiv(2023)
摘要
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_ω (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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要