# Proving with Computer Assistance 2IMF15

## Teacher

Room number MF6.079A (only on Thursdays) For contact, use the e-mail address herman at cs dot ru dot nl

## Location and time

The course will be given on-line via canvas, the TUE education environment on
• Mondays, 9:45--11:30
• Thursdays, 13:30-15:15

## Prerequisites

We assume that you are familiar with a bit of logic, especially natural deduction and preferably (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 the selected pages of 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, please make 2.5 -- 2.10.

## System we will use

We will be using the Proof Assistant Coq in this course.
• You have to download and install Coq yourself. Preferably, you can do this by using the page of Lasse Blaauwbroek, a PhD student at Radboud University Nijmegen. Here you get Coq with some additional automation tactics. You can consult Lasse in case you have problems with installing Coq. Lasse will also later in the course assist with the Coq practicals.
• Through the course we will be showing a number of Coq files and some you will need to fill in the proofs yourself as an exercise. Here is the zip file with all the Coq files.

## The course by week

This schedule may be subject to changes!

• 1/2, 9:45--11:30 Lecture 1
Overview and Introduction: Proof Assistants, Verification, Logic, Type Theory, Formulas-as-types, Coq.
Short recapitulation of lambda calculus.
• 4/2, 13:30-15:15 Lecture 2
Natural Deduction in Coq: proposition logic and predicate logic. Be sure to have Coq installed on your laptop/computer
• 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 11.
• 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 11.
• Here is the pred_log file with some answers filled in, also of the "Challenge problem".
• 8/2, 9:45--11:30 Lecture 3
Simple Type theory and "Formulas-as-Types" for propositional logic.
• 11/2, 13:30-15:15 Lecture 4
Dependent Type Theory.
• 22/2, 9:45--11:30 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.
• 25/2, 13:30-15:15 Lecture 6
Polymorphic Types: ML style and full polymorphism
• 1/3, 9:45--11:30 Lecture 7
Inductive Types.
• Here are the slides
• Here are three files that have been shown at the lecture and you can load into Coq:
• Do the files coq_nat_03.v up to coq_nat_10.v (and coq_nat_11.v if you want a challenge) and send your solutions to the teacher by mail by March 8.
Here are some worked out versions:
• 4/3, 13:30-15:15 Lecture 8
More inductive types; Presentation of the Coq assignment.
• Read slides 15-17 and 24-32 of the slides of last week on inductive types.
• Do the files on lists coq_list_03.v up to coq_list_06.v and send your solution to the teacher by mail by March 11.
• Here are the example files, showing how to do the first exercises on lists in Coq: coq_list_01.v and coq_list_02.v.
• Do the exercises on trees coq_tree_03.v up to coq_tree_05.v and send your solution to the teacher by mail by March 11.
• Here is an example file, showing how to do the first exercise on trees in Coq. Look here for the htm-ized file and look here for the Coq source file.
• Here is the presentation of the Coq assignment. Alternative suggestions for the Coq assignment can be found here .
• 8/3, 9:45--11:30 Lecture 9
Programming with inductive types and dependent inductive types; Examples of cool and useful Coq features.
• 11/3, 13:30-15:15 Lecture 10
Higher order logic, Calculus of Constructions
• 15/3, 9:45--11:30 Lecture 11
Some meta-theory of Type Systems (I): Church-Rosser property
• Here are the slides of the lecture.
• Here are the exercises for the lecture.
• Here are some answers to the exercises.
• 18/3, 13:30-15:15 Lecture 12
Work on Coq assignment
• Here is a page where an earlier example assignment has been worked out. It has been created from a coq .v file .
• We have used the "Proviola" system (by Carst Tankink) to produce this documented page.
• 22/3, 9:45--11:30 Lecture 13
Some meta-theory of Type Systems (II): Normalization
• Here are the slides of the lecture.
• Here are the exercises for the lecture.
• 25/3, 13:30-15:15 Lecture 14
Work on Coq assignment
• 29/3, 9:45--11:30 Lecture 15
Recap of all paper exercises of previous lectures: here are some extra exercises relating to normalization ad Church-Rosser. Possibility to ask questions about the Coq assignment.
• For the notes of the lecture, comprising hand-written answers to various exercises, see the syllabus on canvas.
• 1/4, 13:30-15:15 Lecture 16
Treatment of old exams and possibility to ask questions about earlier exercises and the 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.
• You don't receive a mark (so I will write "NV") if you haven't completed all parts of the course.
• In case your Written Exam mark is below 5, this is also your Final mark.
• Written exam Tuesday April 6, Time: 09:00--12:00 on campus (I assume for now)
• 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 retake exam ("Hertentamen"), all guidelines above apply with the following dates/deadlines:
• Written exam: Monday June 28, 18:00-21:00.
• Coq assignment deadline: Tuesday June 29.
NB. You can chosse to only retake one part of the exam, so only the Written exam, or only the Coq assignment. In any case: register for the retake!

## Coq Assignments

Deadline: Thursday April 8; do the assignment in couples 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.) 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:
• Names and student numbers.
• 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.

herman at cs dot ru dot nl