Lectures¶
1. Introduction, motivation.¶
In the first class we looked at how does a formalized proof (proof verified by a computer) look like on somewhat advanced examples (Cantor theorem, squeeze theorem). The idea is not to understand everything, but to get impression, what this will be about: what is an ITP, how does this interactivity look like.
Homework (ungraded): install Lean and go through the sheet of the first class, to get an impression.
Video recording Lean file used Slides
2. Logic: basic proofs using tactics intro, apply, exact, trivial, and exfalso.¶
In this class we started to prove basic (and trivial) statements in propositional logic. For reference about the tactics we were using, see notes by Bhavik Mehta.
The homework is in the repo (also linked in below -- as a file and as link to live server).
Submit the homework via postal owl, you should've gotten enroll link by email.
Video recording A Video recording B Class github repo Homework Homework on live-lean
3. Logic: more proofs using tactics cases, constructor, left/right, rw, rfl. Real numbers: ring, or norm_num. Also use.¶
We learned techniques to deal with conjuction (cases, constructor) and disjunction (left/right and cases again).
There are two tactics in each case, because assumptions and goal work differently.
We saw several ways to get shorter proofs: using assumption together with <;>, and a diabolical tactics rcases.
We also started a bit with real numbers -- so far just the easy way using tactics ring and norm_num that do the
trivial stuff for us.
We also saw intro to deal with "for all" quantifier and use for existential quantifier.
Video recording A Video recording B Video recording C Homework Homework on live-lean
4. Real numbers: dealing with sequences and quantifiers (intro, specialize, use, obtain). First glimpse of types.¶
We proved basic theorems about limits of sequnces of real numbers. Mainly as a motivation to learn new techniques:
- defining a lambda function (keyword fun)
- dealing with quantifiers: intro and specialize for \(\forall\), use and obtain for \(\exists\))
- linarith, norm_num and ring_nf for simplifying expressions with real numbers
- exact? for easy search for the right theorem in the mathlib
In the end we learned a bit about types; we will learn more next week.
Video recording A Video recording B Video recording C Homework Homework on live-lean
5. Functions in many guises. PAT principle. Inductive types.¶
We learned (recalled) what is a lambda function, and generally function types. Also basic encounter with inductive types,
and recursive definitions. We observed the PAT-principle (propositions as types, proofs as terms), which is the basic of
Lean proof verification: to verify a proof is correct, Lean "only" needs to verify it has the right type.
We also saw how you may use the inductive types to make this work with And etc.
You will see more of this in the homework -- this time it does not use Mathlib, and some of the proofs are trivial. However, as you work though the sheet, you hopefully will get more familiar with the PAT principle, perhaps even start to trust it.
Video recording A Video recording B Video recording C Homework Homework on live-lean
6. Tactics rw, calc. Injectivity&surjectivity. Finite inductive types.¶
Video recording part C is rerecorded part of part B -- for 10 minutes the camera was pointing to a wrong place, sorry! Next class is on Nov 19, as Nov 12 is deans sporting day!
In this class we gained more practice with using rw tactic and saw the useful calc tactic that lets us conveniently
work with transitive relations. Also, we saw how to study properties of functions -- injectivity and surjectivity. We
constructed counterexamples to a statement about these properties -- building specific (inductive) types for this
one purpose.
Video recording A Video recording B Video recording C Homework Homework on live-lean