Erlend Hamberg

Advent of Code 2025 in Lean 4 – Day 9

2025-12-09
Tags: , .

Today’s problem was about 2D rectangles and collision detection. In the first part, we only had to find the largest rectangle we could create from pairs of points, while in part 2 we also had to check that they were inside a polygon defined by a list of edges.1 The description also said that “[points] that are adjacent […] will always be on either the same row or the same column.”, which is basically reminding us that the rectangles and edges are axis-aligned, meaning we can use the good old AABB for checking if a given rectangle intersects with an edge.

So let’s just get a rectangle data type in place:

structure Rect where
    topLeft : Position
    bottomRight : Position
    deriving Repr

def Rect.of (p1 p2 : Position) : Rect :=
  {
    topLeft := { x := min p1.x p2.x, y := min p1.y p2.y },
    bottomRight := { x := max p1.x p2.x, y := max p1.y p2.y }
  }

This is where I first get a bit uncomfortable: To safely use this data type, one has to use the .of constructor, as the default .mk constructor won’t guarantee that the points are actually the top left and bottom right. This is fine for an AoC solution, but it is an accident waiting to happen, so I saw that I could make the default constructor private:

structure Rect where
    private mk ::

… and lived happily ever afterfor five minutes, until I realized that I could still use Rect.mk and get a completely wrong answer! I don’t have time to dig more into this right now, but I guess this would have worked if it crossed a namespace boundary?

Anyway! I can’t spend much longer on this, so let’s just get some helpers in place:

def Rect.area (self : Rect) : Nat :=
    let width := (self.bottomRight.x - self.topLeft.x + 1).natAbs
    let height := (self.bottomRight.y - self.topLeft.y + 1).natAbs
    width * height

def Rect.intersects (self other : Rect) : Bool :=
  self.topLeft.x < other.bottomRight.x
    && self.bottomRight.x > other.topLeft.x
    && self.topLeft.y < other.bottomRight.y
    && self.bottomRight.y > other.topLeft.y

With those helpers, and after realizing that I can simply treat edges as (thin) Rects too, the solution ended up being quite elegant.

Things I (re-)learned today

  • Creating and requiring the use of a smart constructor for a data type isn’t (completely) straightforward.

Solution

import Aoc
open Aoc

structure Rect where
    topLeft : Position
    bottomRight : Position
    deriving Repr

def Rect.of (p1 p2 : Position) : Rect :=
  {
    topLeft := { x := min p1.x p2.x, y := min p1.y p2.y },
    bottomRight := { x := max p1.x p2.x, y := max p1.y p2.y }
  }

def Rect.area (self : Rect) : Nat :=
    let width := (self.bottomRight.x - self.topLeft.x + 1).natAbs
    let height := (self.bottomRight.y - self.topLeft.y + 1).natAbs
    width * height

def Rect.intersects (self other : Rect) : Bool :=
  self.topLeft.x < other.bottomRight.x
    && self.bottomRight.x > other.topLeft.x
    && self.topLeft.y < other.bottomRight.y
    && self.bottomRight.y > other.topLeft.y

def main : IO Unit := do
  let input <- readLines "Day09/input.txt"
  let points := input.toList.map (Position.parse · |> Option.get!)

  -- part 1
  let areas := points.flatMap (λ p1 => points.map (λ p2 => (Rect.of p1 p2).area))
  IO.println s!"Part 1: {areas.max?.get!}"

  -- part 2
  let edges := points.zipWith Rect.of (points.tail ++ [points.head!])
  let areas := points.flatMap (λ p1 => points.map (λp2 =>
    let rect := Rect.of p1 p2
    if edges.any (·.intersects rect) then
      none
    else
        some rect.area
    ))
    |>.filterMap id

  IO.println s!"Part 2: {areas.max?.get!}"

  1. As often is the case, figuring out exactly what they’re asking for was half the challenge.↩︎