Erlend Hamberg

Advent of Code 2025 in Lean 4 – Day 2

2025-12-02
Tags: , .

Today’s problem was also quite simple, and I couldn’t find any interesting maths/proofs – just a lot of (inefficient?) string building and comparisons. I first defined my own simple type representing an inclusive range:

structure InclusiveRange where
  start: Nat
  stop : Nat

… but later discovered the built-in range types.

I ended up adding a small String method to my small utility library today, too:

def String.repeat (s : String) (n : Nat) : String :=
    List.replicate n s |> List.foldl (· ++ ·) ""

Things I (re-)learned today

  • I can namespace functions either by using an explicit namespace or by simply using dotted syntax when naming them.
  • There are different types of ranges in Lean. [1:10] is a Std.Range while 1...=3 is a Std.Rcc Nat (cc = closed, closed) and 1..<3 is a Std.Rco Nat (co = closed, open).
  • I can create aliases for types using abbrev
  • Besides #eval to see what an expression evaluates to, I can use #check to see its type.
  • IO.ofExcept can be used to throw an error if an Except action fails, which is convenient for AoC code.

Solution

import Aoc
open Aoc

abbrev InclusiveRange := Std.Rcc Nat

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

def Part1.isInvalid (id : Nat) : Bool :=
  let digits := toString id
  let len := digits.length
  len % 2 == 0 && (digits.take (len / 2) == digits.drop (len / 2))

def Part2.isInvalid (id : Nat) : Bool :=
  let digits := toString id
  let len := digits.length
  -- an ID is invalid if we can reconstruct it by repeating a prefix
  (List.range' 1 (len / 2)).map (fun prefixLen =>
    len % prefixLen  == 0 &&
      (digits.take prefixLen).repeat (len / prefixLen) == digits
  ) |> List.or

def main : IO Unit := do
  let input ← IO.FS.readFile "Day02/input.txt"
  let ranges <- input.trim.splitToList (· == ',')
    |> List.mapM parseRange
    |> IO.ofExcept

  let invalid : List Nat := ranges.flatMap (Std.Rcc.toList)
    |> .filter Part1.isInvalid
  IO.println s!"Part 1: {invalid.sum}"

  let invalid := ranges.flatMap (Std.Rcc.toList)
    |> List.filter Part2.isInvalid
  IO.println s!"Part 2: {invalid.sum}"