Advent of Code 2022 - Lean4
This year, I attempted Advent of Code in Lean 4 - A theorem prover and programming language. My full solutions are available on github:anurudhp/aoc2022
Lean 4 has very nice constructs for writing “imperative” looking code. This was presented in a functional pearl by Seb Ullrich et. al. in ‘do’ unchained: embracing local imperativity in a purely functional language.
Here are a few random highlights:
§ Breadth-first Search - imperatively
The do notation allows for imperative code, like while and for-loops. And lean’s compiler does reuse analysis to optimize mutation of objects by doing them in-place when possible. Especially useful when mutating lists or arrays. And this is surprisingly good! With no effort, I managed to write very efficient code with “mutation”.
Here is a BFS code from day 12:
def bfs (grid : Grid) (s e : Pos) : Nat := Option.get! do
let n := grid.length
let m := grid.head!.length
let neigh : Pos → List Pos
| u@(x, y) => Id.run do
let mut res := []
if x > 0 then res := (x - 1, y) :: res
if y > 0 then res := (x, y - 1) :: res
if x + 1 < n then res := (x + 1, y) :: res
if y + 1 < m then res := (x, y + 1) :: res
res.filter (grid.at · <= grid.at u + 1)
let mut q := Queue.empty.enqueue (s, 0)
let mut seen := [s]
while not q.isEmpty do
let ((u, d), q') := q.dequeue?.get!
q := q'
if u == e then return d
for v in neigh u do
if not $ seen.elem v then
q := q.enqueue (v, d + 1)
seen := v :: seen
none
§ Adding new notation / syntax rules
Lean’s macro system makes it very nice to extend the syntax, like this one in day 22:
-- ...
macro_rules | `($x ∈ [ $l ... $r ]) => `($l ≤ $x && $x ≤ $r)
def Grid.next₂ (g : Grid) : Pos → Pos | p@(x, y, d) => Id.run do
if let .Up := d then
if x == 1 && y ∈ [ 51 ... 100] then return (y + 100, 1, .Rt) -- A → F
-- ...
§ Issue: Recursion with nested types
One issue I ran into was with defining recursive functions over a nested type. Somehow lean is unable to figure out the function terminates. Here is an example from day 7:
Consider a tree type, where the children are stored in a list.
inductive FSTree :=
| Node (name : String) (size : Nat) (children : List FSTree)
| Leaf (name : String) (size : Nat)
Here is a simple recursive function that computes the subtree size.
partial def FSTree.part1 : FSTree → Nat
| Node _ sz sub => (if sz <= 100000 then sz else 0) + (sub.map part1).foldl Nat.add 0
| _ => 0
I have to mark it partial because lean is unable to prove termination - the indirection FSTree → List → FSTree confuses it.
My understanding is that it is impossible to create a cyclic data structure, so lean should accept this function. Perhaps there is some simple proof to convince it, but for now I don’t know how to do this.
