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
• Assignment information
• Part 0: Makefile
• Part 1: Coq
• Part 2: Overview document
• What to turn in
• Assessment
• Karma

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.

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
• The 3110 Coq tactics cheatsheet
• The Coq Survival Kit, an external reference for Coq tactics

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. Verify before the deadline on CMS that you have submitted the correct version.

Prohibited Coq features. 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.

Git. We recommend that you continue to use a private git repo on the CIS GitHub 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 systems.

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.

• 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.

Part 2: Overview document

You may omit the "Summary" and "Design, Implementation, and Testing" portions of the overview document for this assignment.

What to turn in

Submit files with these names on 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.

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?

Karma

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.

More Coq:

Volume 1 in the Software Foundations textbook series, Logical Foundations, 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, 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.