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)