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.14
URN: urn:nbn:de:0030-drops-110690
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11069/
Go to the corresponding LIPIcs Volume Portal

Czajka, Lukasz

First-Order Guarded Coinduction in Coq

pdf-format:
LIPIcs-ITP-2019-14.pdf (0.5 MB)

Abstract

We introduce two coinduction principles and two proof translations which, under certain conditions, map coinductive proofs that use our principles to guarded Coq proofs. The first principle provides an "operational" description of a proof by coinduction, which is easy to reason with informally. The second principle extends the first one to allow for direct proofs by coinduction of statements with existential quantifiers and multiple coinductive predicates in the conclusion. The principles automatically enforce the correct use of the coinductive hypothesis. We implemented the principles and the proof translations in a Coq plugin.

BibTeX - Entry

@InProceedings{czajka:LIPIcs:2019:11069,
  author =	{Lukasz Czajka},
  title =	{{First-Order Guarded Coinduction in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{14:1--14: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/11069},
  URN =		{urn:nbn:de:0030-drops-110690},
  doi =		{10.4230/LIPIcs.ITP.2019.14},
  annote =	{Keywords: coinduction, Coq, guardedness, corecursion}
}

Keywords: coinduction, Coq, guardedness, corecursion
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The Coq plugin is available at https://github.com/lukaszcz/coinduction.

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