CS430/530 Assignment 1

Due: Monday, September 16, 2013

1. Reynolds, Exercise A.2.
2. Reynolds, Exercise A.3(b).
3. Reynolds, Exercise A.5, except for the part corresponding to question A.4(b)4.
4. Reynolds, Exercise A.6(b).
5. Reynolds, Exercise A.7.
6. Reynolds, Exercise 1.2.
7. SF Basics (Please directly modify the abridged Basics.v file; full version at Basics.v):
   • factorial
   • plus_id_exercise
   • zero_nbeq_plus_1
   • boolean functions
   • andb_eq_orb
   • binary
   • decreasing

Sample solutions

For the writing part, sample solutions can be downloaded here. For the coq part, sample solutions are on the Zoo machine /c/cs430/as/as1/Basics-sol.v.

Sample solutions of the writing part in Coq

Credit to Antonis Stampoulis. Main file. This depends on some definitions and auxiliary lemmas and tactics; if you want to trace through the proofs in ProofGeneral or CoqIDE, make sure to first compile these two files using coqc.