Advent Of Code 2025 - Day 4

Stream: general

[Alfredo Moreira-Rosa]

He is my solution for day 4 of advent of code. Using HashMap to speedup lookup.

Solution

import LeanAoc.utils.List
import Std.Data.HashMap

namespace Day04

-- PARSING

inductive ParseError
  | invalidCharacter (c : Char) (row : Nat)
  | emptyGrid
  | inconsistentRowLength (row : Nat) (expected : Nat) (actual : Nat)

instance : ToString ParseError where
  toString
  | .invalidCharacter c row => s!"Invalid character '{c}' in row {row + 1}"
  | .emptyGrid => "Empty grid"
  | .inconsistentRowLength row expected actual =>
    s!"Row {row + 1} has {actual} characters, expected {expected}"

instance : Coe ParseError IO.Error where
  coe e := IO.userError (toString e)

instance : MonadLift (Except ParseError) IO where
  monadLift
  | .ok a => return a
  | .error e => throw ↑e

abbrev Pos := Int × Int

structure Grid where
  data : Std.HashMap Pos Nat

def parseLine (s : String) (row : Nat) : Except ParseError (Array Nat) := do
  if s.isEmpty then
    return #[]
  let mut result : Array Nat := #[]
  for c in s.toList do
    match c with
    | '@' => result := result.push 1
    | '.' => result := result.push 0
    | _ => throw <| .invalidCharacter c row
  return result

def parseInput (input : String) : IO Grid := do
  let lines := input.splitOn "\n"
  if lines.isEmpty then throw <| IO.userError "Empty grid"

  let mut data : Std.HashMap Pos Nat := Std.HashMap.emptyWithCapacity
  let mut expectedLength : Option Nat := none
  for rowNum in List.range lines.length do
    let line := lines[rowNum]!
    let parsedLine ←
      match parseLine line rowNum with
      | .ok arr => pure arr
      | .error e => throw ↑e
    match expectedLength with
    | none =>
      expectedLength := some parsedLine.size
    | some len =>
      if parsedLine.size != len then
        throw <| (ParseError.inconsistentRowLength rowNum len parsedLine.size : IO.Error)
    for colNum in [0:parsedLine.size] do
      if parsedLine[colNum]! > 0 then
        data := data.insert (rowNum, colNum) parsedLine[colNum]!
  return ⟨data⟩

def readInput : IO String := do
  IO.FS.readFile "LeanAoc/day04/input.txt"

-- COMMON

def neighboursOf (pos : Pos) : List Pos :=
  let r := pos.1
  let c := pos.2
  [(r - 1, c - 1), (r - 1, c), (r - 1, c + 1),
   (r, c - 1),             (r, c + 1),
   (r + 1, c - 1), (r + 1, c), (r + 1, c + 1)]

def Grid.hasPaperRoll (grid : Grid) (pos : Pos) : Bool :=
  grid.data.contains pos

def Grid.countAdjacent (grid : Grid) (pos : Pos) : Nat :=
  neighboursOf pos |>.filter grid.hasPaperRoll |>.length

def Grid.isAccessible (grid : Grid) (pos : Pos) : Bool :=
  grid.countAdjacent pos < 4

def Grid.remove (grid : Grid) (pos : Pos) : Grid :=
  ⟨grid.data.erase pos⟩

def Grid.removeAll (grid : Grid) (positions : List Pos) : Grid :=
  positions.foldl (init := grid) fun g pos => g.remove pos

def Grid.positions (grid : Grid) : List Pos :=
  grid.data.keys

-- PART 1

def countAccessible (grid : Grid) : Nat :=
  grid.positions.filter grid.isAccessible |>.length

#eval do
  let input ← readInput
  let grid ← parseInput input
  return countAccessible grid

-- PART 2

def Grid.allNeighboursOf (grid : Grid) (positions : List Pos) : List Pos :=
  positions.foldl (fun acc pos =>
    let neighbors := neighboursOf pos
      |>.filter fun pos => grid.hasPaperRoll pos && grid.isAccessible pos
    neighbors ++ acc) [] |>.eraseDups

def countTotalRemovable (grid : Grid) : Nat :=
  let accessibles := grid.positions.filter grid.isAccessible
  go grid accessibles 0 grid.data.size
where
  go (grid : Grid) (accessible : List Pos) (acc : Nat) (fuel : Nat) : Nat :=
    match fuel with
    | 0 => acc
    | fuel' + 1 =>
      if accessible.isEmpty then acc
      else
        let newGrid := grid.removeAll accessible
        let newCandidates := newGrid.allNeighboursOf accessible
        go newGrid newCandidates (acc + accessible.length) fuel'

#eval do
  let input ← readInput
  let grid ← parseInput input
  return countTotalRemovable grid

end Day04