Proofs and reliable programming using Coq
This is a course in 7 modules of 3 hours each, with the following tentative plan
- Programming with simple types and recursive data-types
- Logical formulas and the proposition-as-type correspondence in practice
- Tactic-based theorem proving
- Reasoning by induction on programs
- Advanced proof-by-induction guidelines
- More data-types (binary trees, binary numbers)
- Dependent types
Course notes: lesson 1, lesson 2, lessons 3-4, lesson 5, lesson 6, lesson 7
Useful links: a short tutorial Coq in a Hurry, a book Mathematical Components, another book for american graduate students Software Foundations, an in-browser Coq instantiation, the Coq website, and the Coq installation page.
1. Programming with simple types and recursive data-types
In this lesson we learn the basics of pattern-matching and recursive programming in the Coq system, using first the list data structure and then the natural number data structure as examples. This is also the occasion to teach about notations and implicit arguments. These notes cover the main part of this lesson. To test whether you understood this lesson, here are a few diagnostic questions and the corresponding answers. Please contact the teacher if these diagnostic questions show there is still some misconceptions.
2. Logical formulas and the proposition-as-type correspondence in practice
In this lesson, we practice the syntax of a variety of logical connectives. These notes cover the main part of this lesson. The table in this quick reference page summarizes the tactics that were taught. Diagnostic questions, answers.
3. Reasoning by cases and by induction about programs and their behavior
In this lesson, we show how reasoning about programs can be organized. These notes cover the main part of the lesson, diagnostic questions, answers.
4. Reasoning by induction, continued
In this less we continue the presentation of tactics that are useful to reason about programs. We work on a few exercises taken from the previous lesson’s notes. Homework is based on question 5(a) from these notes.
5. Advanced techniques for proof by induction: multi-step and induction loading.
In this lesson, we look at proofs by induction that require specific preparation and concentrate on the question of induction loading. Part of the lessons applied here can be taken from these notes, diagnostic questions, answers.
6. More data-types
In this lesson, we depart from just lists and natural numbers to see data-types that make more computations feasible. In particular, we observe binary numbers and various kinds of binary trees. This course will follow these course notes.
7. Dependent types
In this lesson, we show that the logical language and the programming language are combined in a single programming language, where the expressive power is given by dependent types. We show how recursive programming combines with dependent types to give a nice and powerful programming language. This course follows these course notes, example file.
