## CS430/530 Assignment 2

Last modified: September 17, 2013.

Solution posted: September 29, 2013.
**Due: Wednesday, September 25, 2013**

- Reynolds, Exercise 2.2.

- Reynolds, Exercise 2.3.

- Reynolds, Exercise 2.4.

- Reynolds, Exercise 2.9.

- 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

- 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

Or download the file here or copy
/c/cs430/as/as2/Basics.vo
(both available three days after assignment 1 due).
### 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.