CS430/530 Assignment 4
Last modified: October 8, 2013.
Solution posted: October 25, 2013.
Due: Monday, October 21, 2013
(Please directly modify the abridged Prop.v file;
full version at Prop.v):
(Please directly modify the abridged MoreProp.v file;
full version at MoreProp.v):
- R_provability: including proofs of provable propositions
(Please directly modify the abridged Logic.v file;
full version at Logic.v):
- Extra credits, required for graduate students: classical_axioms; to undergrads: don't spend too much time on it.
(Please directly modify the abridged Imp.v file;
full version at Imp.v):
(Please directly modify the abridged Hoare.v file;
full version at Hoare.v):
Both Imp.v and
SfLib. Please download the coq file
here and compile
it with coqc SfLib.v under the same folder
where you place your other coq files.
Sample solutions are on the Zoo machine