Week 5: Proofs & Semantics

Overview

We’ll review backward and foward proofs in Lean4, introduce inductive predicates through The Hitchhiker’s Guide to Logical Verification chapter 6, and take a good look at operational semantics through chapter 3 (for culture, essentially).

Lecturer

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

Session Information

• Date and Time: Monday 16 February, 15:00 — 17:00 (Beirut time)
• Place: IOEC (Oxy) 518
• Online Meeting Link (Meeting number: 2390 183 3397; Password: 4PBgfeGT*3)
• Session Recording (YouTube)

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)

Navigation

• ← Previous Week: Intro to Tactic-based Proving
• Back to Course Overview
• Next Week: Contributing to Mathlib →

Questions? Reach out on the course Discord!