Proving with Computer Assistance: practical part (2IF48)

This is the page of the practical part of the course Proving with Computer Assistance. For the information about the theoretical part of the course please consult the web page for 2IF40.

• F. Dechesne (lectures, final assignment)
• A. Koprowski (lab sessions, final assignment)

News/announcements

• 8/06: The ultimate deadline for handing in solutions to the final assingment is set to 15/07.
• 24/04: Updated hints on performing case distinction.
• 13/04: Some hints published.
• 29/03: Materials from the last lecture available in materials section.
• 28/03: Announced office hours for the consultation for the final assignment.
• 28/03: Registration finished. If you did not receive email confirming your registration for the final assignment please contact me as soon as possible!
• 5/03: Details about the final assignment are available now.
• 27/02: The problems with CoqIDE in version 8.1 of Coq are resolved by now and hence we decided to use this version of the system for the course (see the updated installation instructions)
• 26/02: Exercises for lab session with Coq are now available.
• 14/02: Materials from the first lecture (handout version of slides + Coq script) are now available.
• 14/02: Posted installation instructions for Coq + CoqIDE.
• Registration for lab session is required. You can register during the lecture on Wed 14/02, 10:45-12:30, Matrix 1.41. Following options are available:
  • Wed 28 Feb., 10:45-12:30, MA 1.41 (group full!)
  • Wed 28 Feb., 15:30-17:15, HG 5.95
  • Thu 1 Mar, 13:30-15:15, HG 5.95
• More to come... check this page out later to find all the information about the practical part of the course.

Coq v 8.1 resources

• homepage: http://coq.inria.fr
• download page: http://coq.inria.fr/distrib-eng.html
• To comfortably work with Coq you will also need an user interface (see below)

• CoqIDE (Download) is a user-friendly Coq user interface. Its main disadvantage is that the version for Windows is very unstable.
• Proof General (Homepage | Download) is a Coq user interface working on top of XEmacs. It is not as user friendly as CoqIDE (unless you are familiar with XEmacs) but is stable even on Windows. Besides it also works with other proof assistants, like Isabelle.

• Coq in a Hurry (pdf): a nice quick introduction to Coq (recommended).
• Online reference manual (html): useful if you need more information on certain aspect of Coq (like usage of a particular tactic etc.)
• Online library: browsable standard library of Coq (with index to all the lemmas and definitions)

The following instructions assume you are using Windows operating system. If you are interested in installation for another platform then consult Coq distribution page or contact the course instructor.

For the purpose of this course we will be using the interface of CoqIDE as its installation is very easy. It boils down to downloading the Coq 8.0pl3 distribution from here and following the installation instructions (basically pressing next a number of times). At this point you may want to upgrade to Coq 8.1 which you can do by installing its distribution from here. This has the following advantages:

• documentation and the description of the standard library on Coq web page refer to ver. 8.1 of the system and there are some changes compared with 8.0pl3 and
• CoqIDE seems to be more stable in 8.1

Course schedule and materials

Final assignment

• Form a team of 2 or 3 students.
• Choose the exercise from the following list of exercises: assignments07.pdf.
  Here is the Coq script for exercise D: STLC.v
• Register for the final assignment before March 15th by sending an email to A. Koprowski. The email should contain names and student numbers of all the members of the group and your choice of the exercise.
• Solve the exercise and write a report (more on that below).
• Send your solution (Coq file + report) before May 11th to your assignor (F. Dechesne or A. Koprowski) The last chance deadline: July 15th
• After submitting your solution make an appointment for the final evaluation. Final evaluation is a short meeting (30min) of all the members of the group with their assignor where you will shortly discuss your solution (both Coq part and the report). You will also receive your grade then.

• Do not make it too long. 15 pages is the absolute maximum but normally it should be much shorter. Keep in mind that longer does not mean better!
• What you should write:
  • Names and student numbers of all the members of the group.
  • Explanation of the problem and your approach to it.
  • Description of the main problems you encountered and solutions you used. If you had some alternative ideas to solve those problems describe them and explain your choice for the solution to this problem.
  • Write about your experience with the prover. What did you like, what you did not like etc.
  • Describe the cooperation within the group and the division of labor.
  • Add the Coq code as an appendix.
• What you should not write
  • Do not unnecessarily repeat the code. Refer to appendix and quote the code only to illustrate something.
  • Do not write obvious things! Description of the proofs of the shape: "the goal is as follows so we apply this tactic and that is what we get..." are useless.

• groups supervised by Francien Dechesne: 4/04-25/04, Tuesdays and Wednesdays 12:45-14:00, HG 7.17
• groups supervised by Adam Koprowski: 11/04-4/05, Wednesdays 13:00-15:00 + arbitrary other time upon appointment, HG 6.78

• Avoid using the type bool; define predicates using Prop. Don't use equality (=) to prove equivalence of propositions, use bi-implication (

  <->

  ) instead.
• For a way of doing case distinction see the following script
• If you have contradictory hypotheses then you may want to convert your goal to 'False'. This can be done by 'apply False_ind.' (try: 'Check False_Ind.')