This is the accompanying code for the invited lean tutorial held at VSTTE 2024 by Sebastian Ullrich and Joachim Breitner.
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.
To prepare for the tutorial, please do the following:
- Install Lean
- Clone this repository
- Ensure that you can build the code by running
lake build
from the command line - Ensure that your editor is correctly connected to Lean by opening one of the files, introducing an error, and checking that there is feedback
The tutorial will be in live-coding presentation style, with breaks for hands-on experiences. Here are suggested tasks that you could try:
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 finisht them without help.
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 like0 + x = x
,1 * x = x
.Hints:
- It may be helpful to define a (non-recursive) function
Expr.optOp
with the same type asExpr.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.
- It may be helpful to define a (non-recursive) function
-
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
and write a theorem aboutOption.bind
andOption.isSome
. Or you can defineExpr.eval'
that returnsValue
(noOption
) and prove that for expressions without division, the result ofExpr.eval
isOption.some
of the value returned byExpr.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?
-
Add nice input syntax for
Env.get σ "x"
andEnv.set
, e.g.σ[[x]]
andσ[[x := e]]
and update some of the proof statements.Instead of
syntax
andmacro_rules
you can also try to use thenotation
command as documented at https://lean-lang.org/lean4/doc/notation.html; 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
byskip
toStmt.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 onEnv
, add the@[ext]
attribute to theEnv
structure. This will allow you to useapply Env.ext
(or even start the proof withext 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 thatinduction
works. You can do that using a helper theorem that you finally apply, or explore thegeneralize
tactic.
Imp/Expr.lean
re-exports the expression language:Imp/Expr/Basic.lean
contains the AST of expressionsImp/Expr/Eval.lean
contains an evaluator for expressionsImp/Expr/Optimize.lean
contains a formally verified optimization passImp/Expr/Syntax.lean
adds a more convenient syntax for expressionsImp/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 statementsImp/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. It also contains a function that implements these semantics, which can be used to run programs.
Imp.lean
imports the other libraries, and contains a concluding demo of using a verified bit blaster to quickly prove theorems.
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.