CS430/530 Assignment 2

Due: Wednesday, September 25, 2013

1. Reynolds, Exercise 2.2.
2. Reynolds, Exercise 2.3.
3. Reynolds, Exercise 2.4.
4. Reynolds, Exercise 2.9.
5. SF Induction (Please directly modify the abridged Induction.v file; full version at Induction.v):
   • basic_induction
   • plus_comm
   • mult_comm
   • evenb_n__oddb_Sn
   • binary_commute
   • binary_inverse
6. SF Lists (Please directly modify the abridged Lists.v file; full version at Lists.v):
   • bag_functions
   • bag_theorem
   • list_exercises -- except nonzeros_app (removed in the abridged version)
   • list_design
   • bag_count_sum
   • rev_injective

For any tool to accept Induction.v and Lists.v in question 5 and 6, you have to compile the Basics.v you finished in assignment 1 to Basics.vo using

• coqc Basics.v.

Sample Solutions

For the writing part, sample solutions can be downloaded here. For the coq part, sample solutions are on the Zoo machine /c/cs430/as/as2/{Induction,Lists}-sol.v.