Lean 4 Is A Cool Language

Originally published on Cohost. Initially, I had planned on writing pwcc in Lean 4, and this post was part of that exploratory process.

---

Following along with https://lean-lang.org/lean4/doc/examples/bintree.lean.html, because i Just Want To Start Writing Code and reading examples is the best way to get acquainted.

Starting off, we have just a simple polymorphic tree definition:

inductive Tree (β : Type v) where
  | leaf
  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
  deriving Repr

And, skipping over a few things, both a naïve toList implementation and a tail-recursive one:

def Tree.toList (t : Tree β) : List (Nat × β) :=
  match t with
  | leaf => []
  | node l k v r => l.toList ++ [(k, v)] ++ r.toList

def Tree.toListTR (t : Tree β) : List (Nat × β) :=
  go t []
where
  go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
    match t with
    | leaf => acc
    | node l k v r => go l ((k, v) :: go r acc)

Neat! Good to see that a functional programming language can in fact do functional programming things. Wait, what’s this next paragraph:

We now prove that t.toList and t.toListTR return the same list. The proof is on induction, and as we used the auxiliary function go to define Tree.toListTR, we use the auxiliary theorem go to prove the theorem.

oh…

theorem Tree.toList_eq_toListTR (t : Tree β)
        : t.toList = t.toListTR := by
  simp [toListTR, go t []]
where
  go (t : Tree β) (acc : List (Nat × β))
     : toListTR.go t acc = t.toList ++ acc := by
    induction t generalizing acc <;>
      simp [toListTR.go, toList, *, List.append_assoc]

The [csimp] annotation instructs the Lean code generator to replace any Tree.toList with Tree.toListTR when generating code.

oh???

@[csimp] theorem Tree.toList_eq_toListTR_csimp
                 : @Tree.toList = @Tree.toListTR := by
  funext β t
  apply toList_eq_toListTR

Like i knew that this was the “functional programming used for proving things” language, but such a tight integration w/ the compiler itself is very cool. Formal verification ftw!