Week 8: Metaprogramming in Lean 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, Fall 2025) | Website

Session Information

• Date and Time: Monday 16 March, 15:00 — 17:00 (Beirut time)
• Place: Online
• Online Meeting Link (Meeting number: 2390 183 3397; Password: 44PBgfeGT*3)
• Session Recording (Recording’s Password: jSWXMt*3)

Core Concepts

In this lecture, we’ll talk about different strategies for designing tactics. Traditional tactics work by analyzing the proof state and (partially) assembling a proof term much like you could do by hand. We’ll implement the basic components of the interval_cases tactic in this way, following a tutorial by Heather Macbeth, with exercises for the interested participants. Following that, we’ll discuss two alternative strategies. Proof by certificate involves running unverified code to generate a witness of the truth of the goal, and then proving this certificate is correct; linarith is an example of such a tactic. Proof by reflection involves proving the correctness of an algorithm in the object language, and then transforming this algorithm into a tactic with a small wrapper of meta code.

Slides

Week 8 Materials (made by Dr. Lewis): Week 8 Materials GitHub Repository

Readings

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

Exercises & Extra Steps

As an exercise for the reader, Dr. Lewis left the following tasks to learn more about metaprogramming in Lean:

• Generally expand the my_interval_cases tactic’s functionality and features to be more like Mathlib’s interval_cases tactic
• More specifically, implement it such that we extract the numbers from the hypothesis instead of supplying them, i.e. removing the with ... between ... bit

Navigation

• ← Previous Week: Mathematical Foundations of Proof Assistants
• Back to Course Overview
• Next Week: Lean, Rust, and the Future of Reliable Software & Project Kick-off →

Questions? Reach out on the course Discord!