Document Open Access Logo

Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq

Author Enrico Tassi



PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.29.pdf
  • Filesize: 395 kB
  • 18 pages

Document Identifiers

Author Details

Enrico Tassi
  • Université côte d'Azur - Inria, France

Cite AsGet BibTex

Enrico Tassi. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 29:1-29:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.29

Abstract

We describe a procedure to derive equality tests and their correctness proofs from inductive type declarations in Coq. 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 [Dunchev et al., 2015] extension language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
Keywords
  • Coq
  • Containers
  • Induction
  • Equality test
  • Parametricity translation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail