文章基本信息

标题：Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq
本地全文：下载
作者：Enrico Tassi
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：141
页码：1-18
DOI：10.4230/LIPIcs.ITP.2019.29
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Coq; Containers; Induction; Equality test; Parametricity translation