Stefan Fehrenbach
2015-11-19

# The Lean Theorem Prover

Some time ago I heard about the Lean theorem prover. I think it was before I interned at Microsoft Research. While I was there, someone mentioned it and its online tutorial. A couple weeks back I stumbled again over the Lean tutorial. This time I actually tried it. It’s cool.

Compared to other proof assistants and dependently typed languages it is very approachable. The tutorial does not make too many assumptions. Most importantly, there is a code editor and a running Lean process right there in the browser. No fighting cabal or installing proof general to try things.

So I worked through the tutorial, which has exercises! As with most things, I did not really have a reason. I did it for the fun of it.

This week, Brian McKenna asked on Twitter (presumably as an exercise) for a function that is both idempotent and an involution.

Idempotent: f(f(x)) = f(x)
Involution: f(f(x)) = x

Find functions with either property. How many functions can you find which have both?

There is only one function with both properties: the identity function.

He later linked to proofs in Idris and Coq. I thought that would make a nice exercise in Lean. It is not exactly my problem, but, unlike exercises in the tutorial, it is also not explicitly positioned as a Lean exercise. There were solutions to take inspiration from, but my own ended up being quite different.

``````open function

lemma ideminvoid (A : Type)
(f : A -> A)
(f_idem : forall x, f (f x) = f x)
(f_invo : forall x, f (f x) = x)
: forall x, f x = id x :=

take x, calc f x = f (f x) : f_idem
... = x       : f_invo
... = id x    : rfl``````

I like the `calc` part of the proof. It reads very much like a proof on a whiteboard: f(x) = f(f(x)), because f is idempotent; f(f(x)) = x, because f is an involution; x = id(x), because `rfl`, which stands for “just evaluate both sides and see that they are the same thing”, in this case, we just use the definition of `id`.

Unfortunately, the tool support for doing actual proofs (as opposed to doing the tutorial) is a bit “meh” compared to Agda, Idris, and Coq. Lean has an Emacs mode, but it’s not great. I also don’t quite understand why they don’t use proof general. To be fair, it’s a very young project.

Anyways, this is what a proof (by a complete beginner) in Lean looks like.