# 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

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 "
2. Page 254, the specification of the division function should be
```forall a b:Z, 0 < b -> {q:Z &{r:Z | a=q*b + r /\ 0 <= r < b}}
```
```forall a b:Z, 0 <= b -> {q:Z &{r:Z | a=q*b + r /\ 0 <= r < b}}
```Inductive sum (A B : Type) : Type :=  inl : A -> A + B | inr : B -> A + B