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 2n
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

  1. Exercise 6.32 page 174
    The correct statement is here
  2. Section 5.1.3, paragraph 4 p 141,
    read "; apply T_ind2" instead of "; apply T_ind"

Going home
Pierre Castéran