Week 4: Dependent Types Part 2

Overview

Rida Hamadani (they/them) — Mathematical formalization researcher, former Lean Expert at Harmonic, Graduate student in resurgence theory (LMAP, France) | Website

Please note: This session will not be recorded as the guest lecturer has requested that no recording be made during the presentation.

The Hitchhiker’s Guide to Logical Verification chapter 3 (backward proofs): tactic mode (by keyword), basic tactics (intro, apply, exact, refine), reasoning about logical connectives and quantifiers (And, Or, Not, Iff, Exists), introduction and elimination rules, and focus bullets (·) for structuring proofs.
Reasoning about equality and automation: three kinds (syntactic, definitional, propositional), rfl tactic, rw/rwa tactics, symm tactic, and decision procedures including decide, omega, simp, simp_all, tauto, aesop, and grind.
Mathematical induction: induction tactic with with | ... patterns, base case and inductive step, induction hypothesis, by_cases for assuming a statement and its negation, cases for decomposing “OR” statements, and obtain tactic for decomposing existentials.
The Hitchhiker’s Guide to Logical Verification chapter 4 (forward proofs): structured constructs (have, obtain), forward reasoning about connectives and quantifiers, calculational proofs (calc keyword for chaining transitive relations), and forward reasoning within tactic-based proofs.
Propositions-as-Types (PAT) and Extensionality: programs ↔ proofs, types ↔ propositions, proof terms, and function/set extensionality (ext).
Mathlib and List reasoning: reasoning about list permutations (~), order duals (αᵒᵈ), and utilizing library lemmas for natural numbers and lists.

Week 4 Slides: Download PDF

Lean4 Code from the Hands-on Session: Download .lean file

Objective: Practice tactic-based proof writing in Lean through the Natural Number Game.

Assignment: The Natural Number Game (Lean Game Server)

Questions? Reach out on the course Zulip!