## CS430/530 Assignment 1

Last modified: September 5, 2013.

Solution posted: September 20, 2013.
**Due: Monday, September 16, 2013**

- Reynolds, Exercise A.2.

- Reynolds, Exercise A.3(b).

- Reynolds, Exercise A.5, except for the part corresponding to question A.4(b)4.

- Reynolds, Exercise A.6(b).

- Reynolds, Exercise A.7.

- Reynolds, Exercise 1.2.

- 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.