CS430/530 Assignment 2
Last modified: January 29, 2025.
Due: Thursday, February 6, 2025
- 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
- even_S
- mul_comm
- binary_commute
- nat_bin_nat
- double_bin
- bin_nat_bin
- SF Lists
(Please directly modify the abridged Lists.v file;
full version at Lists.v):
- bag_functions
- add_inc_count
- list_exercises --
except nonzeros_app
(removed in the abridged version)
- bag_count_sum
- rev_injective
Before working on Induction.v and
Lists.v in question 5 and 6, you have
to place the Basics.v file you finished in
assignment 1 in the same directory as the two files,
and compile it to Basics.vo using
Before working on Lists.v you also
have to execute
- coqc -Q . LF Induction.v.
Alternatively, you may download the file Basics.vo
and copy it to same directory as the two files. (Available 3 days after AS1 is due)
Sample Solutions
For the writing part, sample solutions can be downloaded
here. For the coq part, sample solutions
can be downloaded here and here.
Solutions to the writing part were provided by Antonis Stampoulis.
Solutions to the coq part were prepared by Longfei Qiu.