Deriving proved equality tests in Coq-elpi (Stronger induction principles for containers in Coq)

Enrico Tassi 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01897468
Contributor : Enrico Tassi <>
Submitted on : Wednesday, October 17, 2018 - 11:30:51 AM
Last modification on : Tuesday, April 9, 2019 - 1:21:45 AM
Long-term archiving on : Friday, January 18, 2019 - 1:35:52 PM

File

induction.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01897468, version 1

Citation

Enrico Tassi. Deriving proved equality tests in Coq-elpi (Stronger induction principles for containers in Coq). 2018. ⟨hal-01897468v1⟩

Share

Metrics

Record views

244

Files downloads

128