Proving with Computer Assistance

Teacher

Location and time

• On Type Theory: Basics of Type Theory by Rob Nederpelt. Copies will be handed out at the lecture.
• On Type Theory: Introduction to Type Theory by Herman Geuvers. Copies will be handed out at the lecture.
• On lambda calculus: Introduction to Lambda Calculus by Barendregt and Barendsen. Copies will be handed out at the lecture.
• Coq in a Hurry by Yves Bertot. A quick introduction to Coq
• PVS lecture notes by Adam Koprowski and PVS quick reference card for basic PVS commands.

Systems we will use

1. Get a login, by sending a mail consisting of one line
   LoginName,password,Name Student
   to the teacher and he wil create one for you. Note: Don't use spaces, because a space surrounding "password" will become part of your password.
2. Go to http://prover.cs.ru.nl
3. Login to "Proving with Computer Assistance 2011"
4. Load one of the files (preferably start with the examples.v file)
5. You can now type in tactics to create proofs in natural deduction. You can also select these from the Templates menu.
6. Check "Fitch style natural deduction" in the Display menu, to see the proofs in Fitch style.
7. If you don't know what to do, load the file examples.v and "play" the proofs that are given there.
8. If you want to refresh your natural deduction, download the manual and start playing the "prop" and "pred" files. These have special tactics for doing basic Fitch style natural deduction. You will probably only be needing the Proof Web Fitch style commands plus this special info in case you get stuck with the insert command.

The course by week (Schedule may change)

• 3/2 Lecture 1 Overview and Introduction: Proof Assistants, Verification, Logic, Type Theory, Formulas-as-types, Coq/PVS.
  Short recapitulation of lambda calculus.
  • Here are the slides
  • Make exercises 2.5 -- 2.10 of Introduction to Lambda Calculus by Barendregt and Barendsen.
• 10/2 Lecture 2 Simple Type theory and "Formulas-as-Types" for propositional logic.
  • Here are the slides of the second hour.
  • Make the theory exercises.
• 17/2 Lecture 3 The Curry variant of Simple Type Theory: principal type algorithm.
  
  • Here are the slides of the lecture.
  • The first three pages of this document describe the principal type algorithm in detail.
  • Make the exercises.
  • NB Here are some answers to the exercises.
• 24/2 Lecture 4 Polymorphic Types: ML style and full polymorphism
  
  • Here are the slides of the lecture.
  • Make the exercises.
  • NB Here are some answers to the exercises.
• 3/3 Lecture 5 Dependent Type Theory.
  • Here are the slides of the lecture.
  • Make the exercises.
  • Here are some answers to the exercises.
• 10/3 No class (carnaval holiday week).
• 17/3 Lecture 6 Answers to exercises + Natural Deduction (proposition logic) in Coq, using ProofWeb. Be sure to bring a laptop with wireless internet connection
  • Here is the file with the Coq exercises of the lecture. Complete this at home and send it to the teacher by March 23. You can do this by loading it into the ProofWeb system and do them with Coq.
  • In the lecture, we have shown a bit of another Coq file with exercises. You can see it in html format. If you want to make the exercises, here is the file CoqLab.v.
• 24/3 Lecture 7 Natural Deduction (predicate logic) in Coq, using ProofWeb. Be sure to bring a laptop with wireless internet connection
  • Here is a page with a list of simple useful tactics
  • Here is a Coq file with exercises on predicate logic. Please deliver by mail by March 30.
• 31/3 Lecture 8 Inductive Types.
  • Here are the slides
  • Here are three files that have been shown at the lecture and you can load into Coq/Prover:
    • simple inductive examples from the lecture
    • coq_nat_01.v
    • coq_nat_02.v
  • Do the files coq_nat_03.v up to coq_nat_10.v on prover (and coq_nat_11.v if you want a challenge). Here is the worked out version of coq_nat_11.v, where you can also see the use of the omega tactic.
• 7/4 and 14/4 No class (Exam weeks)
• 21/4 Lecture 9 More Coq exercises: Inductive types, recursion. Be sure to bring a laptop with wireless internet connection
  • Do the exercises on lists coq_list_03.v up to coq_list_06.v on prover.
  • Here is an example file, showing how to do the first exercise on trees in Coq, with a long proof script and a very short one. Look here for the htm-ized file and look here for the Coq source file. (Paste it into Proofweb and see how it works.)
  • Do the exercises on trees coq_tree_02.v up to coq_tree_04.v on prover.
  • Presentation of the Coq assignment
    Here is a page with assignment suggestions
• 28/4 Lecture 10 Higher order logic, Calculus of Constructions, Pure Type Systems
  • Here are the slides of the lecture.
  • Make the exercises.
  • Here are some answers to the exercises.
  • You can also make the exercises with Coq. Here is the Coq .v file. Here is a Coq .v file with answers.
• 5/5 No class
• 12/5 Lecture 11 Answers to exercises + Work on Coq assignment. Be sure to bring a laptop.
  • Here is a page where an earlier example assignment has been worked out. It has been created from a coq .v file .
  • We have uses the Proviola system (by Carst Tankink) to produce this documented page.
• 19/5 Lecture 12 Introduction to PVS. Lecture notes (by Adam Koprowski) and PVS pvs_intro.pvs. Here is a quick reference card for basic PVS commands.
• 26/5 Lecture 13 Presentation of the PVS assignment
• 2/6 No Class
• 9/6 Lecture 14 Work on Coq assignment or PVS assignment.
• 16/6 Lecture 15 Treatment of the exam of July 2010. Work on Coq assignment or PVS assignment

Assignments

• You can do the assignment on the ProofWeb system.
• You can install Coq locally on your machine. Here are some Coq installation suggestions (by Adam Koprowski) on how to do that.

• Choose the exercise from the list of assignment suggestions or invent one yourself. (In the latter case: discuss it with the teacher!)
• Register for the final assignment by sending an email to H. Geuvers. The email should contain your name and student number and your choice of the assignment.
• Solve the assignment and write a report (more on that below).
• Deliver your solution (Report + separate Coq .v files) via mail.

• 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:
  • Name and student number.
  • 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.
  • Possibly add the Coq code as an appendix. (But note that you should deliver the Coq .v files separately anyway.)
• 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.

PVS assignment

• Make the exercises in pvs_intro.pvs, but you may leave aside the parts "Squares" and "StampsTutorial".
• Make the exercises in KnasterTarski.pvs. This amounts to proving the famous "Knaster Tarski fixed piont theorem" for monotone functions over a complete lattice. (In the file we just take a powerset with the subset relation for the complete lattice.)
• Deliver the .prf files of pvs_intro.pvs and of KnasterTarski.pvs. (That are the files that PVS has created while you are doing the proof.) Deliver them via mail, individually and don't forget to give the files your own name.

Examination

• Written exam Tuesday, June 28, 2010, 14.00 -- 17.00.
  • The written exam will consist of questions comparable to the ones that were given during the lectures: see above for the pdf files.
  • It is an open book exam, so you can bring any paper material you want
• Older exams:
  • The exam of July 2010.
  • Here is the exam of 2008. (NB: the original version, which may still be at the Gewis website, contained a mistake; this is the corrected version.)

• Written exam: Thursday 18-08-2010, 09:00-12:00
• Coq assignment deadline: Wednesday 17-08-2010 .
• PVS assignment deadline: Wednesday 17-08-2010.

Useful links

• The Coq online standard library.
• The Coq home page
• The Coq online reference manual.
• The ProofWeb system
• The PVS home page
• A convenient PVS page of Erik Poll at Radboud University Nijmegen.