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.