CS430/530 Assignment 4
Last modified: October 8, 2013.
Solution posted: October 25, 2013.
Due: Monday, October 21, 2013
SF Prop
(Please directly modify the abridged Prop.v file;
full version at Prop.v):
- gorgeous_sum
- beautiful__gorgeous
- ev_ev__ev
- palindromes
SF MoreProp
(Please directly modify the abridged MoreProp.v file;
full version at MoreProp.v):
- R_provability: including proofs of provable propositions
- R_fact
- combine_odd_even
SF Logic
(Please directly modify the abridged Logic.v file;
full version at Logic.v):
- contrapositive
- Extra credits, required for graduate students: classical_axioms; to undergrads: don't spend too much time on it.
- dist_not_exists
- not_exists_dist
- dist_exists_or
- leibniz_equality
SF Imp
(Please directly modify the abridged Imp.v file;
full version at Imp.v):
- optimize_0plus_b
- bevalR
- pup_to_n
- loop_never_stops
- stack_compiler
- stack_compiler_correct
SF Hoare
(Please directly modify the abridged Hoare.v file;
full version at Hoare.v):
- valid_triples
- hoare_asgn_wrong
- hoare_asgn_example4
- swap_exercise
- if_minus_plus
- if1_hoare
Both Imp.v and
Hoare.v require
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
Sample solutions are on the Zoo machine
/c/cs430/as/as4/{Prop,MoreProp,Logic,Imp,Hoare}-sol.v.