# 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