Treffer: Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
Title:
Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
Authors:
Contributors:
Mathematical, Reasoning and Software (MARELLE), Centre Inria d'Université Côte d'Azur, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP)
Source:
ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩
Publisher Information:
CCSD, 2019.
Publication Year:
2019
Collection:
collection:INRIA
collection:INRIA-SOPHIA
collection:INRIASO
collection:INRIA_TEST
collection:TESTALAIN1
collection:INRIA2
collection:UNIV-COTEDAZUR
collection:INRIA-SOPHIA
collection:INRIASO
collection:INRIA_TEST
collection:TESTALAIN1
collection:INRIA2
collection:UNIV-COTEDAZUR
Subject Terms:
Subject Geographic:
Original Identifier:
HAL: hal-01897468
Document Type:
Konferenz
conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.4230/LIPIcs.CVIT.2016.23
DOI:
10.4230/LIPIcs.CVIT.2016.23
Access URL:
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.01897468v2
Database:
HAL
Weitere Informationen
We describe a procedure to derive equality tests and their correctness proofs from inductive type declarations. Programs and proofs are derived compositionally, reusing code and proofs derived previously. The key steps are two. First, we design appropriate induction principles for data types defined using parametric containers. Second, we develop a technique to work around the modularity limitations imposed by the purely syntactic termination check Coq performs on recursive proofs. The unary parametricity translation of inductive data types turns out to be the key to both steps. Last but not least, we provide an implementation of the procedure for the Coq proof assistant based on the Elpi [3] extension language.