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: Monday 9 February, 15:00 — 17:00 (Beirut time)
• Place: IOEC (Oxy) 518
• Online Meeting Link
• Recording

Core Concepts

• The Hitchhiker’s Guide to Logical Verification chapter 3 (backward proofs): tactic mode (by keyword), basic tactics (intro, apply, exact, assumption), reasoning about logical connectives (And, Or, Not, Iff, Exists), introduction and elimination rules, focus combinator { ... } for structuring proofs
• Reasoning about equality: three kinds (syntactic, definitional, propositional), rfl tactic (definitional equality), rw tactic (rewriting), simp tactic (simplification), ac_rfl tactic (associativity and commutativity)
• Mathematical induction: induction tactic, base case and inductive step, induction hypothesis, examples (proving commutativity of addition)
• The Hitchhiker’s Guide to Logical Verification chapter 4 (forward proofs): structured constructs (fix, assume, show … from, have), forward reasoning about connectives and quantifiers, calculational proofs (calc keyword for chaining equalities), forward reasoning within tactic-based proofs (mixing styles)
• Propositions-as-Types (PAT): programs ↔ proofs, types ↔ propositions, universal quantification as dependent functions, proof terms (what tactics compile to), type checking = proof checking

Slides

Week 4 Slides: Download PDF

Readings

1. Theorem Proving in Lean 4 (Chapters 5-6)
2. Functional Programming in Lean 4 (Interlude 2)
3. The Hitchhiker’s Guide to Logical Verification (Chapters 3-4)

Weekly Quiz

Quiz 4: Tactics and Proof Strategies

Quiz Link: Take Quiz 4

Deadline: Before Week 5 session
Passing Score: 60%

Navigation

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

Questions? Reach out on the course Discord!