Lean lecture

Schedule

• Malá Strana SW1: Tuesday 9:00 – 10:30 (lecture), 10:40 – 11:20 (exercise / consultation)
• or Karlín K4: Wednesday 17:20 – 18:50 (lecture), 19:00 – 19:40 (exercise / consultation)

Links

• Official Lean website – installation, documentation, ...
• Lean 4 Web – Lean in a web browser
• Natural Number Game – gamified Lean tutorial
• Lean Zulip chat – Forum for the Lean community. You can ask beginner questions in the `new-members` channel, and there is a good chance someone will come to help.
• Search tools: Loogle, Leansearch, Moogle
• Lectures by Robert Šámal from the winter semester.

Lectures

I am following my write-up notes here in the directory LeanTeaching. The actual files shown in the lectures are stored in the directory Live.

1. Lean as a basic functional language: Numbers, top-bottom type inference, functions, recursion, structures, object-oriented syntax, inductive types
2. Dependent types, Pi & Sigma types, Vector implementations, Curry-Howard correspondence (Propositions as Types), inductive type vs. proposition (examples Or & Exists).
3. Forward & backward proof, basic tactics (refine, exact, intro, apply), practical example (tactics induction, rw, rw??), library search
4. Equality levels: Syntactic / definitional / provable. Why rw fails with rewriting under a binder, or with rewriting an index of a list.
5. Tactic Zoo, part 1: Many goal oriented / assumptions oriented tactics, rewriting, scripting.
6. Tactic Zoo, part 2: Massaging, closing (bashing) & organizing tactics.
7. Typeclasses: Bundled / unbundled data structures. Defining a custom type class: type class as a structure, instance as def. Specific type classes: Add, Decidable, coercions (CoeT, Coe)
8. Quotients: Setoid, mk'', lift. Containers: List, Multiset, Finset, Set, set comprehension, coercion to type, finiteness (Fintype, Finite), cardinality, maximum, sum. Analysis: filters (filtered quantifiers), predicates vs. dummy values.
9. Universes: Lean's logical strength, inaccessible cardinals, ZFCSet, universe-polymorphic constants.

Homework

1. Extending numerical Expr data type. [Lean file]
2. Implementing dependent zeros function, and writing explicit proof terms. [Lean file]
3. Proving identity about LCM & proving correntness of Expr.deriv [Lean file]
4. Making floor defeq & low-level proofs: [Lean file]
5. Reverting clear_value & using rcases syntax & scripting exercise [Lean file]
6. Typeclass operator overloading for Expr & finding the right library typeclasses for orthogonal lines. [Lean file]
7. Formalize certain math definitions: IMO problem (filtered forall) & putnam problem (geometry) & sets modulo finite difference. [Lean file]
8. Define large type constructions using the ZFC operations & include correct universe-polymorphic definitions. [Lean file]

Project / Exam

Other info