You can view lecture demo files and view lecture recordings here.
We will aim to update this table shortly after each lecture. All
lecture recordings can also be found on
Panopto.
| Date |
Topic |
Resources |
Summary |
| 9/4 |
Introduction
|
Recording
Ch. 0 notes
|
We'll talk about what Lean is and see what it can do, and also go over
some organizational points about the course.
Takeaways: Verified programming
is fun and powerful!
|
| 9/9 |
The basics of Lean syntax
|
Recording
Ch. 1-2 notes
|
In this lecture we'll learn the basics of the Lean programming and specification
language: types and terms, type inhabitation, and writing and evaluating very
simple functional programs. No proving yet!"
|
| 9/11 |
Dependent type theory
|
Recording
Ch. 1-2 notes
|
We'll finish Chapter 2 of the HHG, and get a head start on some material
from Chapter 4. Today's topics: inductive types (continued), function definition
and evaluation, specifications, and dependent type theory.
|
| 9/16 |
Backward (tactic) proofs
|
Recording
Ch. 3 notes
|
We'll dive into the meat of the HHG Ch. 3: what are some of the moves
available to us in the tactic proving minigame, beyond intro and
apply? How do we deal with logical connectives: And,
Or, Not, and so on?
|
| 9/18 |
Backward (tactic) proofs, contd.
|
Recording
Ch. 3 notes
|
We'll continue talking about tactic proofs. How do we deal with equality?
What about the natural numbers? We'll also talk about classical vs constructive
logic.
|
| 9/23 |
Forward proofs
|
Recording
Ch. 4 notes
|
We'll see another way to write proofs in Lean, incorporating forward
reasoning. Structured ("proof-term") proofs are a little closer to the underlying
logic. Surprise: proofs in Lean are, literally, just terms in the type theory.
|
| 9/25 |
Dependent types
|
Recording
|
We talked about dependent types before; now, more. The type theory that
Lean is based on, the Calculus of Inductive Constructions, is an instance of dependent
type theory. In DTT, we follow the PAT principle: propositions as types, proofs
as terms. (Buzzword: the Curry-Howard correspondence!) We'll look deeper today
into these foundations. Time permitting, we'll look at a few important algorithms,
including unification.
|
| 9/30 |
Functional programming: data structures
|
Recording
Ch. 5 notes
|
Chapter 5 of the Hitchhiker's Guide introduces some paradigms — inductive
types, structures, recursive definitions, type classes — that might be familiar
from other functional programming languages. The interesting thing for us is how
these paradigms interact with writing proofs. For instance, how do we mix properties
into data structures?
|
| 10/2 |
Functional programming: type classes, lists, trees
|
Recording
|
Type classes are a language feature inspired by Haskell with equivalents
in Scala, ML, and other languages. They allow us a kind of ad hoc polymorphism:
we can define functions on types that implement certain interfaces, and can declare
that certain types implement these interfaces, without bundling the interfaces
into the data type itself. we'll see how this interacts with some of the data
structures we like to use, as we implement and specify functions on these types.
|
| 10/7 |
Inductive predicates
|
Recording
Ch. 6 notes
|
We'll cover ch. 6 of the Hitchhiker's Guide today, on inductive predicates.
This will complete what we need to know about foundations for now: inductive predicates
give us a way to introduce new propositions and prove things about them. Inductive
predicates are also the source of most of the propositional symbols we've used
so far — And, Or, Exists, Eq,
….
|
| 10/9 |
Big-step operational semantics
|
Recording
|
We're jumping ahead to Chapter 9 today! Time to start putting what we've
learned into practice. We'll define the syntax of a toy programming language inside
of Lean, discussing the difference between shallow and deep embeddings. Using
inductive predicates, we'll define a transition system and use this to prove things
about the execution of programs in this toy language.
|
| 10/16 |
Small-step operational semantics
|
Recording
|
The big-step semantics we saw on Monday aren't fine-grained. We can't reason
about intermediate states. An alternative is using a small-step semantics, where
our program execution path is broken down much further. This comes with upsides
and downsides.
|
| 10/21 |
A look under the hood
|
Recording
|
We'll talk theory today, about the data structures and process flow that
underlie a proof assistant. Basically, we'll think about Lean as a programming
language in the sense of the last two lectures. What's its syntax? What are its
semantics??
|
| 10/23 |
Logical foundations
|
Recording
|
As this course has progressed, we've gotten some insight into the foundations
of Lean and its type theory. But some features have remained mysterious. In the
next few lectures we'll poke some more at this foundational theory. Today we'll
be focusing in particular on the type universe Prop, what we're allowed
and disallowed in this universe compared to the others.
|
| 10/28 |
Algebraic structures
|
Recording
|
We'll jump ahead again to chapter 13, where we'll start talking about algebraic
structures. But we'll also improvise a bit here. After we see some basic structures,
we'll define some mathematical types of our own.
|
| 10/30 |
Numbers and sets
|
Recording
|
We'll continue the Ch 13 material we started last time, including a little
more with the complex number playground. We'll also talk about embeddings between
different numerical structures, and some different kinds of "set-like" objects.
|
| 11/4 |
Logical foundations, contd.
|
Recording
|
We'll continue with chapter 12 today, talking about more foundational
constructs. As we discussed last class, there's a grab bag of features that we
can take or leave: proof irrelevance, impredicative Prop, the axiom of choice,
and others. Why should we be convinced that the collection we choose is consistent?
We'll introduce the notion of a model of the type theory to answer questions
like this.
|
| 11/6 |
Quotients, rationals, and reals
|
Recording
|
The last bit of Ch. 12, on quotient types, is very relevant to what we
want to do next! We'll wrap up that discussion (including talking a bit about
the computability properties of quotients) and then immediately use quotient types
to define some familiar things. Rational and real numbers are interesting mathematically,
and for programming purposes, they can be a very convenient tool for writing specifications.
Even if we don't compute with real numbers they're useful to have around.
|
| 11/11 |
Real numbers
|
Recording
|
We finished last week with the rational numbers. Now we need to complete
them to get the reals. This will take yet another quotient. The reals bring to
light some computability issues that we've touched on briefly before: what does
it mean to compute with real numbers? How do we do it in normal languages? If
time permits, we'll look at mathlib's implementation of the reals and see some
generalizations.
|
| 11/13 |
Monads and tactics
|
Recording
|
Lean has a very powerful framework for writing custom tactics.
These tactics are written in Lean itself, with a number of catches to make
this possible. Today we'll see the fundamentals of this approach. We'll
learn the (very) basics about monads, a technique used in some functional
languages to simulate programming with side effects. (But this isn't an FP
class and we're not going to dwell on monads, beyond what we need to know.)
Chapter 7 of the HHG is a more detailed introduction to monads.
|
| 11/18 |
Monads and tactics
|
Recording
|
More from chapters 7 and 8 of the HHG. We'll look at macros, a simple kind of metaprogram.
Then we'll turn our attention to the TacticM monad, which provides an API for interacting
with our context and goals.
|
| 11/20 |
Monads and tactics
|
Recording
|
We'll continue our discussion of metaprogramming by implementing a few custom tactics. Along the way,
we'll see some more metaprogramming techniques and a few "imperative-like" features of monads that make
our lives easier when writing tactics.
|
| 11/25 |
Monads and tactics
|
Recording
|
Metaprogramming TBD
|
| 12/2 |
Guest lecture TBD
|
Recording
|
|
| 12/4 |
Tactic design strategies
|
Recording
|
The tactics we've seen so far manipulate the tactic state in stages.
Today we'll consider some high level designs for automation: proof by certificate
and proof by reflection. We'll also talk about the strategy and algorithm behind
the tactic linarith, a great example of a "large" metaprogram
that shows off a number of interesting design principles.
|
