# A5: Prove It!
**Deadline:** Wednesday, 5/9/18, 11:59 pm
**Special late policy:** You may submit up to 48 hours late with no
penalty. After Friday, 5/11/19, 11:59:00 pm, no more submissions will
be accepted; that is the absolute last moment to submit. After that,
we suggest that you move on to completing your project and studying
for the final.
**Partners:** This assignment may be done as an individual or with one
partner. The use of a partner is optional. Sharing of code is
permitted only between you and your partner; sharing among larger
groups is prohibited. *Pro-tip:* do not divide the work; do pair
programming (pair proving?) instead. You will severely handicap your
understanding of the material if you divide it up.
**Table of Contents:**
* [Assignment information](#info)
* [Part 0: Makefile](#makefile)
* [Part 1: Coq](#coq)
* [Part 2: Overview document](#overview)
* [What to turn in](#turnin)
In this assignment, you will use the Coq proof assistant to implement
two queue data structures and verify their correctness. You will also
do some exercises with logic and induction.
## Assignment information
* Formally verify programs using the Coq proof assistant.
* Practice proofs in formal logic.
* Practice proof by induction.
* [Lectures and recitations 19–23][web]
* The 3110 [Coq tactics cheatsheet][cheatsheet]
* [The Coq Survival Kit][survivalkit], an external reference for Coq tactics
* Your solution must implement the functions and correctly prove the theorems
given in `a5.v`.
* You must submit an overview document.
**What we provide.**
In the release code on the course website you will find this file:
* A Coq source file `a5.v` containing the function stubs to implement and
the theorems to prove.
* A makefile for checking your environment and code.
**Late submissions:** Carefully review the course policies on
[submission and late assignments][late]. Verify before the deadline
on CMS that you have submitted the correct version.
**Prohibited Coq features.**
Anything—theorems, definitions, tactics, etc.—in the Coq standard library
is permitted for use, except for the logic section of the assignment, as
described below. You may not use any third-party Coq libraries or tactics.
We recommend that you continue to use a private git repo on the [*CIS
GitHub*][cisgithub] for version control. But you do not need to submit
a git log for this assignment.
## Part 0: Makefile
As usual, we provide a makefile.
* `make check` will check your Coq environment and the names and types
of your required definitions and theorems. Run that early and often and always before
submitting your solution.
* `make admitted` (which takes a little while to run) will produce a list of all the
theorems you have `Admitted` rather than proved. It calls those "Axioms".
* `make clean` will delete generated files produced by the make and build
## Part 1: Coq
Follow the instructions in `a5.v`. In short, you will:
* implement and verify two kinds of queues,
* prove some theorems in formal logic, and
* prove a summation theorem using induction.
Your entire `a5.v` must compile and pass `make check`; otherwise, you
will receive minimal credit on the assignment. If you find yourself
unable to complete a theorem by the deadline, you should leave the
`Theorem` statement (don't comment it out), and use the `Admitted`
command to tell Coq to accept the theorem without (finished) proof.
Any theorem whose proof is incomplete (perhaps because you used
`Admitted`) will receive no credit.
In the logic section of the assignment (theorems `logic1` through
`logic4`), you may not use the `auto` or `tauto` tactics, because
those would largely trivialize the logical proofs you need to write.
But those tactics are fine to use in the rest of the assignment.
Here are some tips:
* The tactics used most often in the course staff solution are
`destruct`, `discriminate`, `intros`, `simpl`, `simpl in`, and
`trivial`. Also used are `apply`, `assumption`, `auto`,
`contradiction`, `rewrite`, `unfold`, and `unfold in`. Only a couple
theorems require `induction`, and those are clearly marked. In the
logic section, `split`, `left`, and `right` are also needed; and in
the summation theorem, `ring`. All of these are reviewed in the [3110
Coq Tactics Cheatsheet][cheatsheet].
* Factoring out helper lemmas can be very helpful, and the staff solution
does so several times.
* If you ever use `simpl` or `unfold` and get back a subgoal involving
a `match` or `fix` expression, you are probably headed down the
## Part 2: Overview document
You may omit the "Summary" and "Design, Implementation, and Testing"
portions of the [overview document][overview] for this assignment.
## What to turn in
Submit files with these names on [CMS][cms]:
* `a5.v`, containing your solution code.
* `overview.pdf`, containing your overview document. We also accept `.txt`
and `.md` files.
* Optionally, `karma.zip`, if you did any karma problems that require additional
The course staff will assess the following aspects of your solution.
The percentages shown are the approximate weight we expect each to
* **Correctness.** [90%] Did you complete the required definitions and proofs
without using `Admitted` or `admit`? As a rough guide, here is a further
breakdown of the approximate weight we expect to assign to the parts of
- implementation and verification of simple queues: 20%
- implementation and verification of two-list queues:
+ up through equation 7 inclusive: 25%
+ the counterexample and proof for revised equation 8: 15-20%
+ the proofs for rep_ok: 5-10%
- proofs in formal logic: 15%
- the mathematical and Coq proof by induction on a summation: 15%
* **Overview.** [10%] Did you complete the overview document? Does it provide
all the required information?
**Sum of Cubes is Square of Sums:**
Prove the following property:
forall n m, sum_cubes_to n = sum_to n * sum_to n
where `sum_to` is the function that adds the numbers from `0`
Volume 1 in the [_Software Foundations_][sf] textbook series,
[_Logical Foundations_][lf], covers the basics of Coq in more detail
than we do in this course. Our coverage of Coq overlaps with the first
six chapters in the book (_Basics, Induction, Lists, Poly, Tactics,_
and _Logic_). Download the textbook and complete the non-optional 1
through 3-star exercises in those chapters. Some of the problems will
feel like review, while others will be more challenging than the ones
in this assignment. Submit your Coq source files.
**Even more Coq:**
In addition to doing the exercises in the first six chapters of
[_Logical Foundations_][lf], expand your understanding of Coq,
programming languages, and formal verification by completing the
non-optional 1 through 3-star exercises in the chapters _IndProp, Maps,_
and _ProofObjects_. Feel free to work through more of the book if you'd
like. Submit your Coq source files.