Week 4: Intro to Tactic-based Proving (Guest Session)

Overview

Guest lecturer Rida Hamadani will guide us through both backward and forward proof techniques in Lean4, covering The Hitchhiker’s Guide to Logical Verification chapters 3 and 4. We’ll explore the tactic mode, structured constructs, calculational proofs, and the Propositions-as-Types (PAT) principle.

Guest Lecturer

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

Session Information

• Date and Time: Wednesday 11 February, 15:00 — 17:00 (Beirut time)
• Place: Online
• Online Meeting Link (Meeting Number: 2393 041 4987; Password: rJpXCAM@434)

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

Core Concepts

• 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.

Slides

Week 4 Slides: Download PDF

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

Readings

1. Important: Mathematics in Lean 4 (Chapter 1 + at least one chapter covering a topic of your choosing)
2. bis) Theorem Proving in Lean 4 (Chapters 5-6)
3. bis) Functional Programming in Lean 4 (Interlude 2)
4. The Hitchhiker’s Guide to Logical Verification (Chapters 3-4)

Programming Assignment

Assignment 4: The Natural Number Game

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

Assignment: The Natural Number Game (Lean Game Server)

Navigation

• ← Previous Week: Thinking Functionally
• Back to Course Overview
• Next Week: More on Tactics & Inductive Predicates →

Questions? Reach out on the course Discord!