A10: Prove It! Solution

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 deHnition at the top of your solution Ple.







Table of contents:




Instructions







Scope







Submission










Instructions










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







make check will check your Coq environment and the names and types of your required de nitions 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




http://www.cs.cornell.edu/courses/cs3110/2018fa/a10/ 1/3
12/21/2018 A10: Prove It! - CS 3110 Fall 2018




theorems.







make extract will extract your veriVed e cient queue implementation to OCaml in the les







tlqueue.mli and tlqueue.ml . This is just for fun—there’s nothing you need to do with




these. If you haven’t Xnished proving the theorems about two-list queues, it will warn you.







make clean will delete generated Iles 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 de nitions 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 identiIed 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 Ple. 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 gure out how to get simpler results.










Scope










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







Good: The logic proofs and induction proofs are completed.







Excellent: Two-list queues are implemented and veriVed.







If you nd yourself unable to complete a theorem by the deadline you should leave the Theorem




http://www.cs.cornell.edu/courses/cs3110/2018fa/a10/ 2/3
12/21/2018 A10: Prove It! - CS 3110 Fall 2018







statement in the Xle—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 le, including







collaborators and hours_worked .







Run make check a Enal 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 le.




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













3/3