Posted on December 29, 2022

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.