# 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:** * [Introduction](#intro) * [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&ndash;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&mdash;theorems, definitions, tactics, etc.&mdash;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.