🏳️‍⚧️ and I make good posts sometimes!

pfp by me!
banner by https://twitter.com/spect_ion


fediverse
‪@PolyWolf@social.treehouse.systems‬
bluesky
@wolf.girl.technology

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
syntax highlighting by codehost

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!


You must log in to comment.

in reply to @PolyWolf's post:

i am currently trying to learn but their documentation is very hit-or-miss unfortunately. "Monads" section of this book has many TODOs in it. i will write my silly lexer & report back on how hard it was