License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.29
URN: urn:nbn:de:0030-drops-110841
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11084/
Go to the corresponding LIPIcs Volume Portal

Tassi, Enrico

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

pdf-format:
LIPIcs-ITP-2019-29.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{tassi:LIPIcs:2019:11084,
  author =	{Enrico Tassi},
  title =	{{Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11084},
  URN =		{urn:nbn:de:0030-drops-110841},
  doi =		{10.4230/LIPIcs.ITP.2019.29},
  annote =	{Keywords: Coq, Containers, Induction, Equality test, Parametricity translation}
}

Keywords: Coq, Containers, Induction, Equality test, Parametricity translation
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: Source code of the Coq package: https://github.com/LPCIC/coq-elpi

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI