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.
Install Coq. Download the starter code from CMS. Do all the
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.
remove_does_not_increase_count is recommended for additional
practice, but it is advanced and therefore optional.
The starter code in CMS includes the original, unsolved versions of
Lists.v depends upon. When we
Lists.v submission, we will substitute the staff solutions
Induction.v. So, if there are any custom theorems
or definitions you added to Basics or Induction that you want to re-use
in Lists, you will need to copy them over to
Lists.v from your A1
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
appear to be axioms. Be assured that those will not count against you,
because the staff solution will have proved them.
The (advanced) Church numeral exercises at the end of
worth doing just to learn about Church numerals, if you’ve never seen
them before. You might find these resources helpful in understanding
them: , [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.
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.
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.
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
The classical logic exercises can be a bit mind boggling. They are all advanced, hence optional; skipping them is fine.
le_exercises might take a couple hours, but
are well worth the time.
There are many optional exercises at the end of
Imp that are fun:
adding short-circuit 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.
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 hyper-automate any proofs.
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
specialize v to “specialize” it to just
x replaced by
That can save you from having to do an extra
assert (plus proof)
to accomplish the same task.
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.
Nothing to say.
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
Nothing to say.
This one could be challenging. Have fun!