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 re-use 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 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.

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 hyper-automate 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!