A10: Prove It!

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.

Collaboration policy: It’s important that everyone in the course have experience with Coq. So this assignment is to be done as individuals, not with partners nor with teams. You are welcome to talk about the assignment at a high level, as well as Coq in general, with other students—especially your project team. 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 in the provided collaborators definition at the top of your solution file.

Table of contents:

• Instructions
• Scope
• Submission

Instructions

Starter code. Follow the instructions in a10.v to complete the assignment. 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”. If you have proved all the theorems, you will get this output:

  * Axioms: <none>
  

  Then you will know you are done with the assignment and have not forgotten to prove any theorems.

• make extract will extract your verified efficient queue implementation to OCaml in the files tlqueue.mli and tlqueue.ml. This is just for fun—there’s nothing you need to do with these. If you haven’t finished proving the theorems about two-list queues, it will warn you.

• make clean will delete generated files produced by the make and build systems.

Permitted and prohibited Coq features.

• The starter code imports some Coq libraries. You may not change the imports to include additional libraries. You are permitted to use any definitions and theorems, etc., in those libraries. But, to be clear, it’s not worth your time to comb through them looking for useful theorems. There was only one problem in the entire assignment for which the staff solution used a library theorem, and that problem is clearly identified in the starter code.

• The starter code contains hints for various problems about what tactics might be useful. You are welcome to use additional tactics of your choice, with the following exception: the string auto may not appear anywhere in your solution file. That implies that the auto, tauto, eauto, etc., tactics may not be used in your solution. The rationale for this restriction is twofold. First, and perhaps surprisingly, using those tactics is actually likely to make your job harder, not easier, because we haven’t spent time covering the intricacies of what proof automation can and cannot achieve. Second, there are just a few places on the assignment where automation would completely solve the problem, thus robbing you of the opportunity to learn something.

Hints:

• 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 probably are headed down the wrong path. Back up and figure out how to get simpler results.

Scope

• Satisfactory: The solution passes make check. Simple queues are implemented and verified.

• Good: The logic proofs and induction proofs are completed.

• Excellent: Two-list queues are implemented and verified.

If you find yourself unable to complete a theorem by the deadline, you should leave the Theorem statement in the file—don’t comment it out—and use the Admitted command to tell Coq to accept the theorem without proof. Any theorem whose proof is incomplete (perhaps because you used Admitted) will receive no credit, regardless of how close the solution is to a complete proof.

Coding standards are not applicable to this assignment and will not be assessed.

Submission

Make sure you updated all the information in the Author module at the top of the file, including collaborators and hours_worked.

Run make check a final time. Your entire a10.v must compile and pass make check; otherwise, you will receive zero credit on the assignment. An unfortunate number of students failed to pass make check last year. Don’t be one of them this year.

Submit your solution to CMS. Double-check before the deadline that you have submitted the intended version of your file.

Congratulations! You have completed the final 3110 assignment and proved to be victorious.