Exercises

Remark

You will able to prove formally your programs are correct soon.
For now, it could be useful to write some tests for each function you define. You may use the command Compute: 
Compute fact 5.
(** expected result : 
 = 120 : Z
*)
Another possibility is to include some lemmas of the following form: 
Example test_fact : fact 5 = 120.
Proof. reflexivity. Qed.


If your function is buggy and does not return the expected result,  the compilation of your file will fail.


 Errata 


    
  
  1.  Page 24: section 2.2.3.1:
    
  In the sentence "In the second example, the function Zplus expects an integer..." the word Zplus should be replaced by Zmult.

  2.  Page 42:
    
The two occurrences of Z_fun_to_nat_fun must be replaced by
nat_fun_to_Z_fun