Last update: 8-5-2006. (announcement of office hours for groups supervised by Francien Dechesne.)

Teachers:
Francien Dechesne (lectures, lab sessions, final assignment),
Adam Koprowski (lab sessions, final assignment),
Rob Nederpelt (2IF40: all questions about the theoretical part).

Dates (2006):
February 8: introductory lecture to Coq
February 15+20: lab sessions
February 22: lecture on other systems (PVS).
May 12: deadline for handing in the final assignment.

Note: This page will be updated and more information will be added during the course, so please check this page regularly.
Information about the theoretical part of the course is posted at the webpage for 2IF40.

• Announcements (important information!)
• Downloads and links
• Study Material, Slides etc.
• Final Assignment
• Contact

Coq (v 8.0)

Installation required before the practical session!

• homepage: http://coq.inria.fr/
• download page for Coq: http://coq.inria.fr/distrib-eng.html; also for Coq's interactive development environment Coq IDE (for Linux and Windows). Unfortunately, the user interface CoqIDE has proven to be extremely unstable running under Windows. Therefore, it is strongly recommended to run Coq under Linux if possible.

"Coq in a Hurry" (pdf) is a nice quick introduction to Coq (recommended!); a more extensive introduction is the Online tutorial (html).
The following general documentation can easily be found from the Help-menu of CoqIDE:

• Online library (searchable for lemmas and definitions in the library)
• Online reference manual (html) (look through the indices)

Exercise file for the lab sessions: CoqLab.v.

ProofGeneral

Runs under (X)Emacs. Recommended instead of Coq IDE if you run Coq on MacOS X.
Also works for other proof assistants, like Isabelle.

• ProofGeneral homepage
• download

PVS

• homepage: http://pvs.csl.sri.com/
• Tutorial
• Manuals

To use PVS you can connect to the svstud server on which it is installed. (If you do not have a password for svstud yet, contact Jan de Jong of the Notebook Service center: HG8.86, tel. 2979.) To use its emacs interface you need a client for X Windows: this is built-in for Linux; use eXceed for Windows. To start PVS, log in to svstud and type: pvs my_file.pvs.

• February 8, Introduction to Coq: slides, demo Coq-script
• February 15+20, Lab sessions: exercise-file CoqLab.v.
• February 22, Introduction to PVS: slides. The demo was from the one-day course on PVS in Eindhoven, given recently by Dr. Erik Poll from Radboud University Nijmegen. The material of that course (slides, quick reference, exercises) is very useful, and can be found at Erik Poll's homepage.

Here is the list of choices for the final assignment: assignments06.pdf.
Here is the Coq-script for option D: STLC.v.

Please form a group of 2 or 3 students, choose an exercise and mail me before March 1:
1) the names and student numbers of the members of the group,
2) the assignment you choose to do.
If you want to use PVS rather than Coq, please indicate so as well.

Apart from the Coq- (or PVS-) code, you are expected to write a report, in which you:

• list the members of the group and their student numbers;
• explain the problem and your approach to it;
• explain why you defined certain lemmas and how you used certain tactics (you don't need to discuss every single step of every proof!);
• describe the main problems you encountered and your solution to them;
• give your experience with the prover(s): what did you (not) like about the tools you used?
• describe the cooperation within the group (division of labour?);
• add your code as an appendix.

Special request: The report does not need to resemble a master's thesis in volume!
Text and code together should fit well within at most 15 pages. Table of contents, abstract, overview of the contents etc. are really not necessary. Also, only include you Coq code in the main text if it is relevant to show a particular point that is made in the text. Refer to the appendix otherwise.

For the final evaluation, both the code and the report will be discussed in the presence of all members of the group. For this, you can make an appointment by mailing me, adding both the report and the code (the *.v-file in case of Coq, or the *.pvs and *.prf-files in case of PVS) as attachment.

The deadline for handing in the assignment is May 12, 2006.

Some tips and hints:

• Avoid using the type bool; define predicates using Prop. Don't use equality (=) to prove propositions equivalent, use bi-implication (<->) instead.
• For a way to do case distinctions on the natural numbers (for example when defining FastSearch in Exercise A), have a look at these examples.
  To deal with this construction in proofs, try the "destruct"-tactic ("case" works as well, but has more complications).
• Exercise A: In part 1, define the type Tree for binary trees of natural numbers.
  (The word `binary' was unintendedly omitted in a previous version of the assignments.)
• Exercise A: Be warned that part 4 is not trivial. Analyze the problem and define appropriate sublemmas.
• It may be instructive to try out your definitions on a concrete example
  (e.g. in exercises A and B: try out your predicate Ordered on a tree containing, say, 5 natural numbers).
• You can use 'apply False_ind.' to convert any subgoal into 'False'.
  (You can check that False_ind: forall P:Prop, False -> P.)

Francien Dechesne

email: f.dechesne@tue.nl

Room: HG 7.17

Office hours for the Final Assignment:
Mon 8 May: 12:30 - 13:30
Tue 9 May: 12:30 - 13:30
Wed 10 May: 11:00 - 12:00
Thu 11 May: 11:30 - 12:30
Fri 12 May: 10:00 - 12:00