×

Circular coinduction in Coq using bisimulation-up-to techniques. (English) Zbl 1317.68209

Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 354-369 (2013).
Summary: We investigate methods for proving equality of infinite objects using circular coinduction, a combination of coinduction with term rewriting, in the Coq proof assistant. In order to ensure productivity, Coq requires the corecursive construction of infinite objects to be guarded. However, guardedness forms a severe confinement for defining infinite objects, and this includes coinductive proof terms. In particular, circular coinduction is troublesome in Coq, since rewriting usually obstructs guardedness. Typically, applications of transitivity are in between the guard and the coinduction hypothesis. Other problems concern the use of lemmas, and rewriting under causal contexts. We show that the method of bisimulation-up-to allows for an elegant rendering of circular coinduction, and we use this to overcome the troubles with guardedness.
For the entire collection see [Zbl 1268.68006].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Paco; Coq
PDFBibTeX XMLCite
Full Text: DOI