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):
- boolean functions
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.