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.
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
collaborators definition at the top of your solution file.
Table of contents:
Follow the instructions in
a10.v to complete the assignment.
As usual, we provide a makefile.
make checkwill 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
Admittedrather 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 extractwill extract your verified efficient queue implementation to OCaml in the files
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 cleanwill 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
automay not appear anywhere in your solution file. That implies that the
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.
Factoring out helper lemmas can be very helpful, and the staff solution does so several times.
If you ever use
unfoldand get back a subgoal involving a
fixexpression, you probably are headed down the wrong path. Back up and figure out how to get simpler results.
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.
Make sure you updated all the information in the
at the top of the file, including
make check a final time. Your entire
a10.v must compile and
make check; otherwise, you will receive zero credit on the
assignment. An unfortunate number of students failed to pass
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.