Lean tutorial

This is the accompanying code for the invited Lean tutorial held at the VeTSS Summer School 2025 by Sebastian Ullrich and Joachim Breitner.

Introductory slides

Overview

In this tutorial we will see the following features of Lean

• basic functional programming
• extensible custom syntax for domain-specific functions
• inductive predicates and proofs

The example use-case is a standard task in programming language theory: Embedding a small imperative language, defining its semantics, and reasoning about it.

We won't have time to explain everything in complete detail, but we hope that the overview we provide is a good starting point for learning to use Lean. Please see the documentation section of the Lean website for further resources. The Lean Zulip is a friendly and helpful place to ask questions for both beginners and experts.

Preparing for the Tutorial

To prepare for the tutorial, please do the following:

1. Install Lean
2. Clone this repository
3. Ensure that you can build the code by running lake build from the command line
4. Ensure that your editor is correctly connected to Lean by opening one of the files, introducing an error, and checking that there is feedback

Hands-on tasks

The tutorial will be in live-coding presentation style, with breaks for hands-on experiences. Here are suggested tasks that you could try:

First hands-on break

Suggested tasks, in rough order of difficulty. These are invitations to play around with Lean; unless you have prior experience with it or very similar tools like Isabelle or Coq, it is not likely to finish them without help. Maybe team up!

The tasks have a programming and a proving component. You can also choose to focus on the programming part.

The branch exercises contains the result of solving all the exercises.

• Add unary operations (negation, logical not) to the expression language.

• Let Expr.optimize apply rules like 0 + x = x, 1 * x = x.

  Hints:

  • It may be helpful to define a (non-recursive) function Expr.optOp with the same type as Expr.op, that serves as a “smart constructor”. Pattern matching can be elegant here!
  • In general it is advisible to write a separate theorem about each involved function (BinOp.apply, Expr.optOp, Expr.optimize) separately than to do it all in one go. If these theorems are set up just right, they are good @[simp] lemmas, and will make the subsequent proof easy.

• Prove that Expr.optimize is idempotent: (e : Expr) : e.optimize.optimize = e.optimize.

• Write a function Expr.hasDiv : Expr → Bool that checks if division is used in the expression.

  Prove that if an expression has no division, then Expr.eval will always return a result.

  Hint: There are various ways of phrasing this. You can use Option.isSome. Or you can define Expr.eval' that returns Value (no Option) and prove that for expressions without division, the result of Expr.eval is Option.some of the value returned by Expr.eval'.

  Food for thought: How does this task relate to the previous task and the optimization 0 * x = 0? If you have done both tasks, can you combine them?

Second hands-on break

• Add nice input syntax for Env.get σ "x" and Env.set, e.g. σ[[x]] and σ[[x := e]] and update some of the proof statements.

  Instead of syntax and macro_rules you can also try to use the notation command as documented at https://lean-lang.org/doc/reference/latest//Notations-and-Macros/Notations/#notations; this will also make the new syntax show up in the InfoView (in other words, it will also delaborate).

• Add the optimization that replaces x := x by skip to Stmt.optimize.

  Use #guard_msgs to check that it does what you want it to do on a small example.

  Finally, extend the verification proof.

  Hints:

  You may want to prove @[simp] theorem set_get_same {σ : Env} : σ.set x (σ.get x) = σ for that. To prove an equality on Env, add the @[ext] attribute to the Env structure. This will allow you to use apply Env.ext to prove that two environments are the same. (It also allows you to start the proof with ext y : 2 – check the docstring to see what that does.)

• (Short but tricky):

  Complete this proof that a looping program has no output

  def loop := imp {while (1) {skip;}}
  theorem infinite_loop : ¬ BigStep σ loop σ' := by

  Hint:

  Rephrase the statement so that the three arguments to BigStep are variables, so that induction works. You can do that using a helper theorem that you finally apply, or explore the generalize tactic.

Code Structure

• Imp/Expr.lean re-exports the expression language:
  • Imp/Expr/Basic.lean contains the AST of expressions
  • Imp/Expr/Eval.lean contains an evaluator for expressions
  • Imp/Expr/Optimize.lean contains a formally verified optimization pass
  • Imp/Expr/Syntax.lean adds a more convenient syntax for expressions
  • Imp/Expr/Delab.lean causes Lean to use the convenient syntax in its output (not part of tutorial, but nice to have!)
• Imp/Stmt.lean re-exports the statement language:
  • Imp/Stmt/Basic.lean contains the AST and a convenient concrete syntax for statements
  • Imp/Stmt/Delab.lean causes Lean to use the convenient concrete syntax in its output (not part of tutorial, but nice to have!)
  • Imp/Stmt/Optimize.lean contains an optimization pass (unverified)
  • Imp/Stmt/BigStep.lean contains big-step operational semantics, and uses them to prove the optimizer correct.
  • Imp/Stmt/Run.lean contains an executable interpreter that follows this semantics, and is proven (totally) correct.
• Imp.lean imports the other libraries, and contains a concluding demo of using a verified bit blaster to quickly prove theorems.

Acknowledgments

This tutorial was previously held at VSTTE 2024 by Sebastian Ullrich and Joachim Breitner.

This content is based on material written by David Thrane Christiansen for the tutorial "Lean for the Functional Programmer", presented at Mødegruppen for F#unktionelle Københavnere by David Thrane Christiansen on 2024-08-27 and 2024-09-24.

This material itself is based on a tutorial presented at SSFT24 by David Thrane Christiansen, co-developed with Leonardo de Moura.