Erlend Hamberg

Advent of Code 2025 in Lean 4 – Day 5

2025-12-05
Tags: , .

Quick one today. The problem was all about ranges, so I added some helpers on Std.Rcc (“range, closed, closed”) to my utility library:

def Std.Rcc.intersect (r1 r2 : Std.Rcc Nat) : Option (Std.Rcc Nat) :=
  let lower := max r1.lower r2.lower
  let upper := min r1.upper r2.upper
  if lower ≤ upper then some (Std.Rcc.mk lower upper) else none

def Std.Rcc.union (r1 r2 : Std.Rcc Nat) : Std.Rcc Nat :=
  Std.Rcc.mk (min r1.lower r2.lower) (max r1.upper r2.upper)

I also added infix operators for these functions1:

infixl:50 " ∩ " => Std.Rcc.intersect
infixl:50 " ∪ " => Std.Rcc.union

With that in place, solving the problem was quite easy: checking for inclusion in part 1 and collecting the intersecting ranges and summing their sizes in part 2

Things I (re-)learned today

  • I can define infix operators for functions, like in Haskell, using infixl/infixr.

Solution

import Aoc
open Aoc

def parseRange (range : String) : Except String (Std.Rcc Nat) :=
  match range.splitOn "-" with
  | [start, stop] => Except.ok (Std.Rcc.mk (start.toNat!) (stop.toNat!))
  | _ => Except.error s!"Invalid range: {range}"

def main : IO Unit := do
  let blocks ← readBlocks "Day05/input.txt"
  let (freshRanges, ingredients) ← match blocks with
    | #[b1, b2] => pure (b1, b2)
    | _ => IO.ofExcept (Except.error s!"Expected 2 blocks of lines")
  let ingredients := ingredients.map (·.toNat!)
  let freshRanges ← freshRanges.mapM parseRange |> IO.ofExcept

  -- part 1
  let fresh := ingredients.filter (λ i => freshRanges.any (i ∈ ·))
  IO.println s!"Part 1: {fresh.size}"

  -- part 2
  let combinedRanges := freshRanges.foldl (λ acc r =>
      let (intersecting, rest) := acc.partition (r ∩ · |> Option.isSome)
      intersecting.foldl (· ∪ ·) r :: rest
  ) []
  IO.println s!"Part 2: {combinedRanges.foldl (· + ·.size) 0}"

  1. Bonus: Look at how cute the ∪ operator is for an anonymous function using the placeholder syntax: (· ∪ ·)↩︎