# Inductive Data Structures

Sources of examples from the book
## Exercises

### Types without recursion

Exercise 6.1 page 139 On seasons

Exercise 6.3 page 140 Using `bool_ind`

Exercise 6.4 page 144 On seasons (continued)

Exercise 6.6 page 144 Computing on booleans

Exercise 6.8 page 146 Manhattan distance

Exercise 6.9 page 148 Functions defined by cases without `match`
### Case based reasoning

Exercise 6.10 page 153 Applying `mont_rect`

Exercise 6.11 page 153 A manual proof of discrimination

Exercise 6.13 page 156 About the danger of axioms

New! On partial functions
### Recursive types

Exercise 6.15 page 166 Definition by cases

Exercise 6.16 page 166 Another definition of addition

Exercise 6.17 page 166 Computing *f(0)+f(1)+...f(n)*

Exercise 6.18 page 166 Computing 2^{n}

Exercise 6.19 page 169 Representation of positive numbers

Exercise 6.20 page 169 On even positive numbers

Exercise 6.21 page 169 Division by 4

Exercise 6.23 page 169 Propositional formulae

Exercise 6.24 page 169 On fractions

Exercise 6.25 page 169 Looking for a value in a tree

Exercise 6.26 page 170 Logarithm and power

Exercise 6.27 page 171 Representing trees with functions

Exercise 6.28 page 172 Finding 0 in an infinitely branching tree

Exercise 6.29 page 173 A simple proof by elimination

Exercise 6.30 page 173 Representing trees with functions (continued)

Exercise 6.31 page 174 A simple proof by induction

Exercises 6.32 and 6.33 page 174 On the sum of the *n* first natural numbers
### Polymorphic types

Exercise 6.34 and 6.35 page 177 A simple polymorphic function on lists

Exercise 6.38 page 177 On the list `1::2:: ... `*n*::nil.

Exercise 6.40 page 178 On (too) short lists

Exercise 6.41 page 179 Finding the first element satisfying a boolean predicate in a list

Exercise 6.42 page 179 Splitting and combining lists

Exercise 6.43 page 179 Monomorphic binary trees and polymorphic trees

Exercise 6.45 page 179 Computing prime numbers
### Dependent inductive types

Exercise 6.46 page 183 Manual injection on variably dependent types

Exercise 6.47 page 183 Trees with fixed height

Exercise 6.48 page 183 Binary words

Exercise 6.49 page 183Bit-wise or on binary words

Exercise 6.50 page 183 A function returning a value in a dependent type
### Empty types

Exercise 6.51 page 183 On the empty set
### New !

On vectors

## Errata

- p. 164, line -13: 't' and 'e' should be 'T' and 'expr'
- p. 165, line 20, 't' should be 'T'
- Exercise 6.32 page 174

The correct statement is here
- Section 6.1.3, paragraph 4 p 141,

read "; apply T_ind2" instead of "; apply T_ind"

Going home

Pierre Castéran