Assignments
General instructions:

Use the Coq sources available from CMS, not from the public Software Foundations website. Changes are being made to exercises that are specific to CS 4160 Spring 2019.

Assignments are due at noon on Tuesday each week, with late submissions accepted until noon on Thursday.

All assignments are to be done as individuals, not with partners nor with teams. You are welcome to talk about assignments at a high level, as well as Coq in general, with other students. But your solution code must be written entirely on your own. Do not share solution code, including Coq programs or proof scripts, with any other students. Do not develop them together. If you do collaborate with other students, you need to acknowledge them at the top of your solution file.

Optional means optional. Any exercises marked “optional” are not required: you are free to skip or complete them, at your choice, with no effect on your score.

Advanced also means optional. You are welcome to dig deeper into the material with these, but they will have no effect on your score.
Any exceptions or clarifications for individual assignments will be posted below.
A1
Install Coq. Download the starter code from CMS. Do all the
exercises in Basics.v
and Induction.v
, except those marked as
optional or advanced. (The optional more_exercises
exercise in
Induction.v
is nonetheless recommended for additional practice with
understanding the tactics being studied.) Submit your solutions in CMS.
That’s all!
A2
Exercise remove_does_not_increase_count
is recommended for additional
practice, but it is advanced and therefore optional.
Important:
The starter code in CMS includes the original, unsolved versions of
Basics.v
and Induction.v
, which Lists.v
depends upon. When we
grade your Lists.v
submission, we will substitute the staff solutions
to Basics.v
and Induction.v
. So, if there are any custom theorems
or definitions you added to Basics or Induction that you want to reuse
in Lists, you will need to copy them over to Lists.v
from your A1
solution.
Unfortunately this also complicates running make ListsTest.vo
to check
whether your solution to Lists.v
relies on any axioms, because all
the unproved theorems in the original Basics.v
and Induction.v
will
appear to be axioms. Be assured that those will not count against you,
because the staff solution will have proved them.
A3
The (advanced) Church numeral exercises at the end of Poly.v
are
worth doing just to learn about Church numerals, if you’ve never seen
them before. You might find these resources helpful in understanding
them: [1], [2, §1.4]. If you understand
the encoding, you can probably invent the implementation of addition
and multiplication by yourself. Inventing the implementation of
exponentiation is quite tricky; don’t be afraid to look it up in one
of those resources.
Advanced exercise forall_exists_challenge
in Tactics.v
is
recommended for additional practice. Hint: although it’s tempting to
prove De Morgan’s Laws on bool
as helper lemmas, you don’t actually
need to do that.
A4
The 2 and 3 star exercises will now routinely require case analysis and/or induction, sometimes nested. Don’t be afraid to wade into such proofs, but always try to have a strategy in mind before you start.
Exercise tr_rev_correct
is 4 stars not because it requires a long
proof, but because it requires ingenuity in inventing a good helper
lemma. Start by trying to prove lemma tr_rev_correct
; note where you
get stuck, then try to invent a helper lemma that is sufficiently
general. The staff solution uses just a single induction
and no
destruct
.
The classical logic exercises can be a bit mind boggling. They are all advanced, hence optional; skipping them is fine.
A5
The optional le_exercises
might take a couple hours, but
are well worth the time.
A6
There are many optional exercises at the end of Imp
that are fun:
adding shortcircuit evaluation, or break statements, or for loops.
If we hadn’t just had a prelim, one or more of those would have been
required instead of optional. You might enjoy solving them nonetheless.
A7
The Hoare logic exercises are a good place to experiment with automation,
tacticals, and the e
variants of tactics. Of course, you are not
required to hyperautomate any proofs.
The specialize
tactic hasn’t been covered in SF, but is useful in
one or two places—though never necessary. If you have a
hypothesis of the form forall x, P
in the context, then you can
do specialize v
to “specialize” it to just P
with x
replaced by v
.
That can save you from having to do an extra assert
(plus proof)
to accomplish the same task.
A8
We are placing more emphasis on Hoare logic in 4160 that SF does. Make doubly sure you grab the assignment source from CMS, because a number of exercises have been modified.
A9
Nothing to say.
A10
The second half of SearchTree.v
is marked as optional. That means the
exercises are optional, but you still need to read them and understand
what they are asking you to prove. The concepts will be used in later
assignments.
A11
Nothing to say.
A12
This one could be challenging. Have fun!