Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
In: ITP 2019 - 10th International Conference on Interactive Theorem Proving ; https://inria.hal.science/hal-01897468 ; ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩, 2019
Online
Konferenz
Zugriff:
International audience ; 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.
Titel: |
Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq
|
---|---|
Autor/in / Beteiligte Person: | Tassi, Enrico ; Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; 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) |
Link: | |
Zeitschrift: | ITP 2019 - 10th International Conference on Interactive Theorem Proving ; https://inria.hal.science/hal-01897468 ; ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩, 2019 |
Veröffentlichung: | HAL CCSD, 2019 |
Medientyp: | Konferenz |
DOI: | 10.4230/LIPIcs.CVIT.2016.23 |
Schlagwort: |
|
Sonstiges: |
|