CS430/530 Assignment 4
Last modified: February 19, 2025.
Due: Thursday, March 6, 2025
SF Logic
(Please directly modify the abridged Logic.v file;
full version at Logic.v):
- contrapositive
- dist_not_exists
- dist_exists_or
- combine_odd_even
- not_exists_dist
SF IndProp
(Please directly modify the abridged IndProp.v file;
full version at IndProp.v):
- ev_double
- ev_sum
- ev_ev__ev
- ev_plus_plus
- palindromes
(There is an interesting challenge in this chapter, although it is NOT part
of your homework: prove pigeonhole_principle
without using excluded middle. -- Longfei)
SF Imp
(Please directly modify the abridged Imp.v file;
full version at Imp.v):
- optimize_0plus_b_sound
- bevalR
- pup_to_n
- loop_never_stops
- stack_compiler
- execute_app
- 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_ceval
- hoare_if1
Before working on later exercise files, you need to compile the previous
exercise files with coqc -Q . LF \$FILE.
You also have to compile your finished
{Basics,Induction,Lists,Poly,Tactics}.v or compile our sample
solutions (available 3 days after AS3 is due).
Sample Solutions
Sample solutions
can be downloaded
here and
here and
here and
here.
Solutions were prepared by Longfei Qiu.