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

- 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]`" must be replaced by "*E*`fun x:A =>`"*E* - 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}}

instead offorall 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 + BThe function

Going home

Pierre Castéran