Functions and their specification

Scripts from the book

Exercises

Exercises 9.1 page 253 and 9.2 page 254 Witness Extraction

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.10 page 271 Reasoning on the fibonacci sequence
Formal specification of a parity test
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

  1. 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 "