Infinite Objects and Proofs

Potentially infinite lists

The chapter on co-inductive types of our book is mainly illustrated with the theory of finite or infinite ("lazy") lists. This file contains the complete development of this theory. Please notice that most of exercises proposed in the book are solved in this file , presented as a complete Coq development.
Here are some more exercises on this topic.
Exercise 13.1 page 350 Mapping finite lists to lazy lists
Exercise 13.5 page 357 Mapping a function on a stream
Erratum 6th line (on the book) : read "such that LMapcan ..." instead of "such that LMap ..."
Exercise 13.13 page 366 A boggy definition of Infinity
Exercise 13.16 page 367 Finiteness, infinity and classical logic
Exercise 13.17 page 368 Another definition of infinite lists
Exercise 13.29 page 373 Using finiteness hypotheses

Lazy binary trees

All the technology illustrated by linear lists apply to tree structures. The following thread of exercises is devoted to binary trees which may have infinite branches.
Exercise 13.2 page 351 Potentially infinite trees
Exercise 13.3 page 355 Building some complex trees
Exercise 13.4 page 355 Grafting trees
Exercise 13.9 page 361 Unfold lemmas for graft
Exercise 13.14 page 366 Trees with [in]finite branches
Exercise 13.23 page 370 Tree bisimilarity
Exercise 13.26 page 371 A theorem on graft


Going home
Pierre Castéran