Week 8: Advanced Metaprogramming and Decision Procedures (Guest Session)

Overview

Dr. Rob Lewis from Brown University will guide us through different strategic approaches to tactic design, from direct proof manipulation to sophisticated decision procedures, with a deep dive into how tactics like linarith work under the hood.

Guest Lecturer

• Dr. Rob Lewis — Assistant Professor of Computer Science (Brown University), instructor of CS1715 (Formal Proof and Verification)

Session Information

• Date and Time: Monday 16 March, 15:00 — 17:00 (Beirut time)
• Place: IOEC (Oxy) 518
• Online Meeting Link
• Recording

Core Concepts

• High-level tactic strategies: direct proof (goal/context manipulation), proof by reflection (verified computation with syntax representation and interpretation), proof by certificate (external oracle generates certificate, kernel verifies)
• Proof by reflection example: representing boolean expressions as inductive types, interpretation function to Prop, normalization to Bool, correctness theorem, reducing goals to computation
• Linear arithmetic and certificate checking: deciding satisfiability of linear inequality systems, certificate as nonnegative coefficients proving contradiction, why verification is easier than generation, modular oracle architecture
• The linarith tactic implementation: preprocessing, parsing linear structure, certificate generation (Fourier-Motzkin elimination, Simplex, external tools), validation in kernel
• Fourier-Motzkin elimination algorithm: successive variable elimination by partitioning inequalities (pos/zero/neg), deriving new comparisons, tracking derivations to produce certificates
• Nonlinear arithmetic: decidability (Tarski’s result, cylindrical algebraic decomposition), computational challenges, nlinarith tactic, applications to static analysis

Slides

Week 8 Slides: Download PDF

Readings

1. The Hitchhiker’s Guide to Logical Verification (Chapters 7-8)
2. Functional Programming in Lean 4 (Chapters 4-5-8)

Weekly Quiz

Quiz 8: Monads and Metaprogramming

Quiz Link: Take Quiz 8

Deadline: Before Week 9 session
Passing Score: 60%

Navigation

• ← Previous Week: Mathematical Foundations of Proof Assistants
• Back to Course Overview
• Next Week: The Broader Landscape & Project Kick-off →

Questions? Reach out on the course Discord!