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.