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
Errata
p. 358, lines 19 and 29: 'list A' should be 'LList A'
Going home
Pierre Castéran