MSc-level course at Vrije Universiteit Amsterdam, computer science

6 credits

Academic year 2021–2022, period 2

This course introduces the proof assistant Lean, its type-theoretic foundations, and its applications to computer science and mathematics.

- Jasmin Blanchette (VU Amsterdam)

- Anne Baanen (VU Amsterdam)
- Jannis Limperg (VU Amsterdam)

- Lecture 1
- Tuesday 17:30–19:00, weeks 44–50, room VU MF-A307
- Exercise 1
- Wednesday 13:30–17:00, weeks 44–50, rooms VU MF-BK37 and NU-5A91
- Lecture 2
- Thursday 15:30–17:00, weeks 44–50, room VU HG-10A33
- Exercise 2
- Friday 15:30–17:00, weeks 44–50, rooms VU NU-6B58 and NU-5A91
- Final exam
- Tuesday 21 December (week 51) 08:30–11:15 (with extra time: 11:45), room RAI blok 9

See also the official VU timetable.

The course consists of 14 lectures:

- Basics
- Definitions and Statements
- Backward Proofs
- Forward Proofs

- Functional–Logic Programming
- Functional Programming
- Inductive Predicates
- Monads
- Metaprogramming

- Program Semantics
- Operational Semantics
- Hoare Logic
- Denotational Semantics

- Mathematics
- Logical Foundations of Mathematics
- Basic Mathematical Structures
- Rationals and Real Numbers
- Guest lecture

These are the videos from 2020, covering the same material as this year.
The headings and numbers correspond to the *Hitchhiker's Guide*.

Lecture 1: Preface + Definitions and Statements

- Preface
- 1.1. Types and Terms
- Intermezzo: The Karate Kid ("Wax On, Wax Off")
- 1.2. Type Definitions
- 1.3. Function Definitions
- 1.4. Lemma Statements
- Example: Typing Derivation

Lecture 2: Backward Proofs

- 2.1. Tactic Mode + 2.2. Basic Tactics
- 2.3. Reasoning about Logical Connectives and Quantifiers
- Intermezzo: The Hitchhiker's Guide to the Galaxy ("Don't Panic")
- 2.4. Reasoning about Equality
- 2.6. Proofs by Mathematical Induction + 2.8. Cleanup Tactics
- Epilogue: Proof! from The Master Theorem Games

Lecture 3: Forward Proofs

- 3.1. Structured Proofs + 3.2. Structured Constructs
- 3.3. Forward Reasoning about Connectives and Quantifiers
- 3.4. Calculational Proofs + 3.5. Forward Reasoning with Tactics
- 3.6. Dependent Types
- 3.7. The Curry–Howard Correspondence
- Intermezzo: Type Theory
- 3.8. Induction by Pattern Matching

Lecture 4: Functional Programming

- 4.1. Inductive Types + 4.2. Structural Induction
- 4.3. Structural Recursion + 4.4. Pattern Matching Expressions
- 4.5. Structures + 4.6. Type Classes
- Intermezzo: Why Killers Have Lists
- 4.7. Lists + 4.8. Binary Trees

Lecture 5: Inductive Predicates

- 5.1. Introductory Examples
- Intermezzo: Jeu de Paume
- 5.2. Logical Symbols
- 5.3. Rule Induction
- 5.5. Elimination
- 5.6. Further Examples

Lecture 6: Monads

- 6.1. Introductory Example
- 6.2. Two Operations and Three Laws
- Intermezzo: Monad in the 21st Century
- 6.3. A Type Class + 6.4. No Effects
- 6.5. Exceptions
- 6.6. Mutable State
- 6.7. Nondeterminism
- 6.9. A Generic Algorithm: Iteration over a List

Lecture 7: Metaprogramming

- 7.1. Tactics and Tactic Combinators
- 7.2. The Metaprogramming Monad
- Intermezzo: Meet the Guy in Charge of the President's Teleprompter
- 7.3. Names, Expressions, Declarations, and Environments
- 7.4. First Example: A Conjunction-Destructing Tactic
- 7.5. Second Example: A Provability Advisor

Lecture 8: Operational Semantics

- 8.1. Formal Semantics
- 8.2. A Minimalistic Imperative Language
- About State
- 8.3. Big-Step Semantics
- 8.4. Properties of the Big-Step Semantics
- Intermezzo: Neil Armstrong's First Steps on the Moon
- 8.5. Small-Step Semantics
- 8.6. Properties of the Small-Step Semantics

Lecture 9: Hoare Logic

- First Things First: Formalization Projects
- Intermezzo: Veruca Salt – Don't Make Me Prove It
- 9.1. Hoare Triples
- Zwischenspiel: Hoare on Hoare Triples
- 9.2. Hoare Rules
- 9.3. A Semantic Approach to Hoare Logic
- 9.4. First Program: Exchanging Two Variables
- 9.5. Second Program: Adding Two Numbers
- 9.7. A Verification Condition Generator + 9.8. Second Program Revisited: Adding Two Numbers
- 9.9. Hoare Triples for Total Correctness

Lecture 10: Denotational Semantics

- 10.1. Compositionality + 10.2. A Relational Denotational Semantics
- 10.3. Fixpoints
- 10.4. Monotone Functions
- Intermezzo: Monotony (Short Film)
- 10.5. Complete Lattices
- 10.6. Least Fixpoint + 10.7. A Relational Denotational Semantics, Continued + 10.8. Application to Program Equivalence

Lecture 11: Logical Foundations of Mathematics

- 11.1. Universes
- 11.2. The Pecularities of Prop
- 11.3. The Axiom of Choice
- Intermezzo: Proof that 1 = 2
- 11.4. Subtypes
- 11.5. Quotient Types (Part A)
- 11.5. Quotient Types (Part B)

Lecture 12: Basic Mathematical Structures

- 12.1. Type Classes over One Binary Operator
- Intermezzo: Finite Simple Group (of Order Two)
- 12.2. Type Classes over Two Binary Operators
- 12.3. Coercions
- 12.5. Lists, Multisets, and Finite Sets
- 12.6. Order Type Classes

Lecture 13: Rational and Real Numbers

- 13.1. Rational Numbers
- 13.2. Real Numbers (Part A)
- 13.2. Real Numbers (Part B)
- Epilogue: Crisis in the Foundations of Mathematics

Guest Lecture: Johan Commelin (Albert-Ludwigs-Universität Freiburg)

We are available if you need help or advice, or just want to let us know about your progress or have suggestions to improve the course (for this year or next year).

For queries concerning the practical work or technical issues with
installing or running Lean, please email the teaching assistants
(Jannis Limperg and Wolf bij 't Vuur) with
`[LoVe]` in the subject line.

For queries concerning the lectures, please email the lecturer (Jasmin Blanchette)
with `[LoVe]` in the
subject line. Addressing an email in academia is always a puzzle; here, a
simple "Dear Jasmin" suffices.

We will also try to monitor Canvas regularly, but because of the subtle blue-on-blue "You got mail" indicator, it is all too easy to miss messages there. To reach fellow students and instructors all at once, you can use Canvas for discussions and questions related to Lean.

Proof assistants are software tools that can be used to check the correctness of a specification of a program or the proof of a mathematical theorem. The course is concerned with Lean, a proof assistant that is developed primarily at Microsoft Research. In the practical work, we learn to use Lean. We will see how to use the system to prove mathematical theorems in a precise, formal way, and how to verify small functional programs (e.g., a sorting algorithm). In the course, we focus on its dependent type theory and on the Curry–Howard correspondence between proofs and functional programs (λ-terms). These concepts are the basis of Lean but also of other popular systems, including Agda, Coq, and Matita.

The course is oriented towards the application of proof assistants to computer science and mathematics. We will use Lean, a modern system developed at Microsoft Research. In each lecture, we will review a Lean file, which can be downloaded from the materials section below.

Although the course is application-driven, this is a university course,
so theory is important as well. We will cover it as it emerges, but you
are expected to read the materials we refer to,
especially the lecture notes (*The Hitchhiker's Guide to Logical Verification*).

To each of the first 13 lectures correspond

- a chapter in
*The Hitchhiker's Guide* - a Lean demo file (e.g.,
`love01_definitions_and_statements_demo.lean`) - a Lean exercise sheet (e.g.,
`love01_definitions_and_statements_exercise_sheet.lean`) - a Lean homework sheet (e.g.,
`love01_definitions_and_statements_homework_sheet.lean`–for the first 11 lectures only)

The exercises are crucial. __Theorem proving can only be learned by
doing.__ We will assist you during the group exercises and answer
questions on Canvas; the "Discussions" panel of Canvas is a great way to
get help and to connect with fellow students, especially in the time of
cholera. We will also help you set up Lean and Visual Studio Code on your
computer. See the installation instructions for
the necessary software (Lean and its mathematical library).

Lecture 14 is a special guest lecture, showing a real application of Lean.

For the group exercises, we recommend that you bring your own wine^H^H^H^Hlaptop.

The homework given at lecture *n* must be submitted on Canvas by
the beginning of lecture *n* + 2. The deadline is strict. There are
11 homework sheets, but we will only grade the first 10 that have been
submitted. Thus, missing a single deadline might not affect your grade.

The homework counts for 25% of the final grade and __must therefore be
done individually__. As in previous years, suspected cases of plagiarism
will be reported to the examination board.

Optionally, you can choose to replace two homeworks by a project. This is a great way to improve your theorem proving skills in little time. You can think up a nice formalization project for yourself, such as these:

- Define a functional data structure (e.g., some kind of tree) and verify a few operations on it.
- Define your own small programming language and study its semantics formally.
- Formalize some results from undergrad mathematics.

You are encouraged to discuss your plans with your instructors before starting your project. You should set yourself a time limit before starting your project. Also incomplete formalizations are welcome. We will be generous while grading them, so that you are not penalized for choosing the project over the regular homework. Please document your formalization well, such that we can see what it does or is intended to do. In our experience, doing a project is the absolute best way to learn theorem proving.

Below you will find previous exams as well as a mock exam.

- Logical Verification 2020–2021 at VU (by J.C. Blanchette and G. Ebner):

final exam sheet

resit exam sheet - Logical Verification 2019–2020 at VU (by J.C. Blanchette and A. Bentkamp):

final exam sheet

resit exam sheet - Logical Verification 2018–2019 at VU (by J.C. Blanchette and J. Hölzl):

mock exam sheet and solution

final exam sheet

resit exam sheet

- Lean community (web page)
- Visual Studio Code (web page)
- Lean's mathematical library (git repository)
*Theorem Proving in Lean*(tutorial)*Concrete Semantics: With Isabelle/HOL*(book)