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}}
    
    instead of
    forall a b:Z, 0 <= b -> {q:Z &{r:Z | a=q*b + r /\ 0 <= r < b}}
    
  • Page 254. This paragraph omits to present the sum type:
    Inductive sum (A B : Type) : Type :=  inl : A -> A + B | inr : B -> A + B
    
    The function div2_gen uses sum and not sumbool, since (div2_of_even _ _) returns a term of sort Set (hence Type) and not a proposition.

    Going home
    Pierre Castéran