Week 5: Tactic-Based Proving I — Backward Proofs

Overview

Lecturer

  • Daniel Dia — Course creator, primary instructor & organizer (American University of Beirut); Computer & Communications Engineering (CCE) and Mathematics dual-degree student (AUB).

Session Information

Core Concepts

  • Review of proof techniques: backward proofs (tactic mode with intro/apply/exact/assumption), forward proofs (structured constructs with fix/assume/show/have), calculational proofs (calc for chaining equalities), mixing both styles within proofs
  • Propositions-as-Types (PAT) principle: programs ↔ proofs, types ↔ propositions, type checking = proof checking, universal quantification as dependent functions (∀x:σ, P(x) := (x:σ)→P(x)), tactics compile to proof terms
  • LoVe chapter 6 (inductive predicates): functions of type ... → Prop, introduction/elimination rules, examples (Even numbers with zero/add_two rules, Sorted lists, Palindromes, full binary trees), logical symbols as inductive predicates (And, Or, Exists, Equality with only reflexivity), rule induction (structural induction on proof terms)
  • LoVe chapter 3 (operational semantics): formal semantics of programming languages (mathematical specification of program meaning), the WHILE language (skip, assignment, sequence, conditional, while), State = String → ℕ
  • Big-step semantics: judgment (S, s) ⟹ t (entire execution from state s to t), rules for each construct, determinism property, limitations (cannot express nontermination or intermediate states)
  • Small-step semantics: judgment (S, s) ⇒ (S’, s’) (one step of execution), configurations (final vs non-final), reflexive transitive closure using Star (chain multiple steps), can express nontermination and intermediate states, comparison with big-step, equivalence: (S,s)⟹t ↔ (S,s)⇒*(skip,t)

Slides

Week 5 Slides: Download PDF

Readings

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

Programming Assignment

Assignment 4: The Natural Number Game (Continued)

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!