<
* [Assignment information](#info)
* [Part 0: Makefile](#makefile)
* [Part 1: Coq](#coq)
* [Part 2: Overview document](#overview)
* [What to turn in](#turnin)
* [Assessment](#assessment)
* [Karma](#karma)
<a name="intro"></a>
## Introduction
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.
<a name="info"></a>
## Assignment information
**Objectives.**
* Formally verify programs using the Coq proof assistant.
* Practice proofs in formal logic.
* Practice proof by induction.
**Recommended reading.**
* [Lectures and recitations 19–23][web]
* The 3110 [Coq tactics cheatsheet][cheatsheet]
* [The Coq Survival Kit][survivalkit], an external reference for Coq tactics
[web]: http://www.cs.cornell.edu/Courses/cs3110/2018sp/
[survivalkit]: https://coq.inria.fr/files/coq-itp-2015/CoqSurvivalKit.pdf
[cheatsheet]: coq-tactics-cheatsheet.html
**Requirements.**
* 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.**
<span style="color:green;"> UPDATE [11/17/17]:
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.
</span>
[late]: http://www.cs.cornell.edu/Courses/cs3110/2018sp/syllabus.php#late
**Git.**
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.
[cisgithub]: https://github.coecis.cornell.edu/
<a name="makefile"></a>
## 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
systems.
<a name="coq"></a>
## 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
wrong path.
<a name="overview"></a>
## Part 2: Overview document
You may omit the "Summary" and "Design, Implementation, and Testing"
portions of the [overview document][overview] for this assignment.
[overview]: http://www.cs.cornell.edu/Courses/cs3110/2017fa/handouts/overview.html
<a name="turnin"></a>
## 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
files.
[cms]: https://cms.csuglab.cornell.edu/
<a name="assessment"></a>
## Assessment
The course staff will assess the following aspects of your solution.
The percentages shown are the approximate weight we expect each to
receive.
* **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
the assignment:
- 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?
<a name="karma"></a>
## Karma
<img src="camel_orange.png" height="40" width="40">
<img src="camel_black.png" height="40" width="40">
<img src="camel_black.png" height="40" width="40">
**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`
to `n`.
<img src="camel_orange.png" height="40" width="40">
<img src="camel_black.png" height="40" width="40">
<img src="camel_black.png" height="40" width="40">
**More Coq:**
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.
[sf]: https://softwarefoundations.cis.upenn.edu/current/index.html
[lf]: https://softwarefoundations.cis.upenn.edu/current/lf-current/index.html
<img src="camel_orange.png" height="40" width="40">
<img src="camel_orange.png" height="40" width="40">
<img src="camel_black.png" height="40" width="40">
**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.
]]>