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:


Starter code. Follow the instructions in a10.v to complete the assignment. As usual, we provide a makefile.

Permitted and prohibited Coq features.



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