Functions and their specification
Scripts from the book
Exercises
Exercises 9.1 page 253 and 9.2 page 254 Witness Extraction
Exercise 9.3 page 254 A simple version of sig_rec
Exercise 9.4 page 254 Equality on nat is decideable
Exercise 9.5 page 256 More on permutations
Exercise 9.6 page 270 A three step induction proof
Exercise 9.7 page 270 A two step induction proof
Exercise 9.8 page 270 The fibonacci sequence
Exercise 9.9 page 270 A four-step induction principle
Exercise 9.10 page 271 Reasoning on the fibonacci sequence
Exercise 9.11 page 271 Proofs using specific induction principles
Exercise 9.12 page 270 Euclidean division by 2
Exercise 9.13 page 276 Another addition function
Exercise 9.14 page 276 Associativity of the tail recursively defined addition
Exercise 9.15 page 276 A tail recursive Fibonacci function
Exercise 9.16 page 284 Computing square roots
Exercise 9.17 page 284 An efficient Fibonacci function on binary numbers
Errata
- page 252 (last paragraph of 9.1.1) and page 254 (last paragraph
of 9.1.2). The old-fashioned syntax of abstraction : "[x:A]E"
must be replaced by "fun x:A => E "
Going home
Pierre Castéran