Proving with Computer Assistance 2IMF15
Teacher
Herman Geuvers: home page
Room number MF6.079A (only on Thursdays) For contact, use the e-mail address herman at cs dot ru dot nl
Location and time
AUD 15 on Thursdays, hours 5-8, 13:45-17:30.
Prerequisites
We assume that you are familiar with a bit of logic, especially natural deduction and (untyped) lambda calculus.
- For those not familiar with untyped lambda calculus:
I will do a short recapitulation in hour 2 of the Lecture 1. Furthermore, read "Introduction to Lambda Calculus" of
Barendregt and Barendsen, Chapter 1, Chapter 4 pp. 22-26, Chapter 2
pp. 12-14 (read = as beta-equality =_{\beta})
As exercises you may try 2.5 -- 2.10.
Material
- The
book Type
Theory and Formal Proof -- An Introduction (Rob Nederpelt and
Herman Geuvers) has appeared in November 2014 with Cambridge
University Press. The course basically covers the material in the book
with a "hands on experience": using the proof assistant
Coq. The link
above gives background material. You
can order
the book with CUP, or via the teacher.
- On lambda calculus: Introduction to Lambda Calculus by Barendregt and Barendsen.
- On Type Theory: Introduction to Type Theory by Herman Geuvers.
- The slides of the course, please find the pdfs below.
- Coq
in a Hurry by Yves Bertot. A quick introduction to Coq, notably read Section 3.
- A quick reference page
with a list of simple useful Coq tactics.
System we will use
We will be using the Proof
Assistant Coq in this course. You can download
and install Coq locally, but you can also use it through the ProofWeb
webinterface
at http://prover-pca.cs.ru.nl/new. For ProofWeb:
- Get a login, by sending a mail
- with subject: [pwca]
- 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.
- Go to http://prover-pca.cs.ru.nl/new
- Login to "Proving with Computer Assistance 2017"
- Load one of the files (preferably start with
the proposition_logic.v file)
- You can now type in tactics to create proofs in natural deduction. You can also select these from the Templates menu.
- Check "Fitch style natural deduction" in the Display menu, to see the proofs in Fitch style.
- If you don't know what to do, load the file proposition_logic.v and "play" the proofs that are given there.
The course by week
This schedule may be subject to changes!
- 9/2 hour 5-6 Lecture 1 Overview and Introduction: Proof Assistants,
Verification, Logic, Type Theory, Formulas-as-types, Coq.
Short recapitulation of lambda calculus.
- 9/2 hour 7-8 Lecture 2 Simple Type theory and
"Formulas-as-Types" for propositional logic.
- 16/2 hour 5-6 Lecture 3 Dependent Type Theory.
- 16/2 hour 7-8 Lecture 4 Natural Deduction
(proposition logic and predicate logic) in Coq, using ProofWeb.
Be sure to bring a laptop
with wireless internet connection
- All students that have sent me a login request on prover before
February 13, 12:00 now have a login. Please try it
on http://prover-pca.cs.ru.nl/new. If
you don't have a login, send me a mail (see above).
- Here is
a page
with a list of simple useful tactics
- Proposition Logic: Here is the file with the
proposition logic Coq exercises
of the lecture. Complete this at home and send it to the teacher
by mail by February 23.
- Here is the proposition_log file with
some answers filled in.
- Predicate logic: Here is a file with
the predicate logic Coq
exercises. Complete this (you can skip the "Challenge
problem") at home and send it to the teacher by mail by
February 23.
- Here is the pred_log file with
some answers filled in, also of
the "Challenge problem".
- 23/2 hour 5-6 Lecture 5 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.
- 23/2 hour 7-8 Lecture 6
Polymorphic Types: ML style and full
polymorphism
- 2/3 No Lecture, because of Carnaval holiday week.
- 9/3 hour 5-6 Lecture 7
Higher order logic, Calculus of Constructions
- 9/3 hour 7-8 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:
- 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) and either (1) send
your solutions to the teacher by mail (2) or save them on
prover by March 16.
- 16/3 hour 5-6 Lecture 9
More inductive types; Presentation
of the Coq assignment.
- Do the files on lists coq_list_03.v up to coq_list_06.v on
prover and either (1) send your solution to the teacher by mail
(2) or save them on prover by March 23.
- 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 and either (1) send your solution to the
teacher by mail (2) or save them on prover by March 23.
- Here is a page
about the Coq assignment. Alternative suggestions for the Coq assignment can be found here .
- 16/3 hour 7-8 Lecture 10
Programming with inductive types and dependent inductive types.
- 23/3 hour 5-6 Lecture 11
Examples of cool and useful Coq features + Work on Coq assignment.
Be sure to bring a laptop with wireless internet connection
- 23/3 hour 7-8 Lecture 12
- Work on Coq assignment
Be sure to bring a laptop with wireless internet connection
- 30/3 hour 5-6, Lecture 13 Overview of Type Theory.
- 30/3, hoour 7-8 Lecture 14 Work on Coq assignment
- 6/4 hour 5-6 Lecture 15 Recap of all exercises
- 6/4 hour 7-8 Lecture 15 Treatment of
the exam
of July 2010. Work on Coq assignment.
Examination
The mark for the course is determined by the 2
marks you will get for the two items listed below.
- Final mark = (Written Exam mark + Coq Assignment mark)/2
with the condition that your Written Exam mark should be 5 or higher.
Note that you don't receive a mark if you
haven't completed all parts of the course.
- Written exam Thursday 20-04-2017, 13:30- 16:30
- 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.)
For the second chance ("Hertentamen"), all guidelines above apply with the following dates/deadlines:
- Written exam: ??
- Coq assignment deadline: ?? .
Coq Assignments
Deadline: Thursday 20-04-2017; deliver your assignment by mail to the teacher.
Here is a page about the
of Coq assignment. (Look here
for some additional comments regarding the use of lists.) Options:
- You can do the assignment on the ProofWeb system.
- You can install Coq locally on your machine.
To complete the Coq assignment follow these steps:
- Solve the assignment and write a report (more on that below).
- Deliver your solution (Report + separate Coq .v files) via mail.
A couple of remarks concerning the report:
- 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 definitions and the line of your
proofs (e.g. sublemmas 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.
Useful links
herman at cs dot ru dot nl