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

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. Theorem Proving in Lean 4 (Chapters 7-8)
2. The Hitchhiker’s Guide to Logical Verification (Chapters 6-9)

Weekly Quiz

Quiz 5: Inductive Predicates & Semantics

Quiz Link: Take Quiz 5

Deadline: Before Week 6 session
Passing Score: 60%

Programming Assignment

Assignment 4: Inductive Predicates and Semantics

Objective: Define and reason about inductive predicates and program semantics.

Assignment: PROOF101 Programming Assignment 4

Navigation

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

Questions? Reach out on the course Discord!