Advent Of Code 2025 - Day 5

Stream: general

[Alfredo Moreira-Rosa]

Here is my solution for day 5. This one was easy. Just merging ranges in part two. Litle trick is to order the ranges first.

Solution

namespace Day05
-- PARSER

inductive ParseError
  | invalidNumberInRange (a b : String)
  | invalidNumber (n: String)
  | invalidRangeOrd (l h : Nat)
  | invalidRangeFormat (s : String)
  | invalidInputFormat (n : Nat)

instance : ToString ParseError where
  toString
  | .invalidNumberInRange a b => s!"Invalid number in range: '{a}-{b}'"
  | .invalidNumber n => s!"Invalid number: '{n}'"
  | .invalidRangeOrd l h => s!"Invalid range order: '{l}-{h}', expected lower ≤ higher"
  | .invalidRangeFormat s => s!"Invalid range format: '{s}', expected '<nat>-<nat>'"
  | .invalidInputFormat n => s!"Invalid input format, expected 2 sections but got {n}"

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 Range := Nat × Nat

def parseRange (s : String) : Except ParseError Range := do
  let parts := s.splitOn "-"
  match parts with
  | [a, b] =>
    match (a.toNat?, b.toNat?) with
    | (some na, some nb) =>
      if na ≤ nb then
        return (na, nb)
      else
        throw <| .invalidRangeOrd na nb
    | _ => throw <| .invalidNumberInRange a b
  | _ => throw <| .invalidRangeFormat s

def parseRanges (input : String) : Except ParseError (List Range) :=
  input.splitOn "\n" |>.mapM parseRange

def parseId (idStr : String) : Except ParseError Nat :=
  match idStr.toNat? with
  | some id => return id
  | none => throw <| .invalidNumber idStr

def parseIds (input : String) : Except ParseError (List Nat) :=
  input.splitOn "\n" |>.mapM parseId

def parseInput (input : String) : IO ((List Range) × List Nat) := do
  let lines := input.splitOn "\n\n"
  match lines with
    | [rangesSection, idSection] => do
      let ranges ← parseRanges rangesSection
      let ids ← parseIds idSection
      return (ranges, ids)
    | _ => throw <| (ParseError.invalidInputFormat lines.length : IO.Error)

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

-- COMMON

def Range.size (r : Range) : Nat := r.2 - r.1 + 1

instance instNatInRange : Membership Nat Range where
  mem range id := id ≥ range.1 ∧ id ≤ range.2

instance instDecidableNatInRange (id: Nat) (range : Range) : Decidable (id ∈ range) :=
  inferInstanceAs (Decidable (id ≥ range.1 ∧ id ≤ range.2))

-- PART 1

def freshIngredients (ranges: List Range) (ids: List Nat) : List Nat :=
  ids.filter fun id => ranges.any (id ∈ ·)

def freshIngredientsCount (ranges: List Range) (ids: List Nat) : Nat :=
  freshIngredients ranges ids |>.length

/--
info: 3
-/
#guard_msgs in
#eval do
  let input := "3-5\n10-14\n16-20\n12-18\n\n1\n5\n8\n11\n17\n32"
  let (ranges, ids) := ← parseInput input
  return freshIngredientsCount ranges ids

#eval do
  let input := ← readInput
  let (ranges, ids) := ← parseInput input
  return freshIngredientsCount ranges ids

-- PART 2

def mergeOrderedRanges (r1 r2 : Range) : Option Range :=
  if r2.1 ≤ r1.2 then
    some (r1.1, max r1.2 r2.2)
  else
    none

def mergeOverlappingRanges (ranges : List Range) : List Range :=
  ranges.mergeSort (fun a b => a.1 ≤ b.1)
    |>.foldl (fun acc r =>
      match acc with
      | [] => [r]
      | h::t =>
        match mergeOrderedRanges h r with
        | some merged => merged::t
        | none => r::acc
    )
    []

def countFreshIngredientsRanges (ranges: List Range) : Nat :=
  mergeOverlappingRanges ranges |>.map Range.size |>.sum

/--
info: 14
-/
#guard_msgs in
#eval do
  let input := "3-5\n10-14\n16-20\n12-18\n\n1\n5\n8\n11\n17\n32"
  let (ranges, _) := ← parseInput input
  return countFreshIngredientsRanges ranges

#eval do
  let input := ← readInput
  let (ranges, _) := ← parseInput input
  return countFreshIngredientsRanges ranges

end Day05

[Alfredo Moreira-Rosa]

Edit: Timings where not properly computed, fixed.

Here are the timings for all 5 first days. Lean is pretty fast so far.

Running Day 1...
Parsing time: 4.42ms
Part 1: 1158 (459ns)
Part 2: 6860 (510ns)

Running Day 2...
Parsing time: 1.51ms
Part 1: 5398419778 (369ns)
Part 2: 15704845910 (231ns)

Running Day 3...
Parsing time: 2.88ms
Part 1: 17412 (528ns)
Part 2: 172681562473501 (813ns)

Running Day 4...
Parsing time: 52.26ms
Part 1: 1553 (356ns)
Part 2: 8442 (353ns)

Running Day 5...
Parsing time: 2.13ms
Part 1: 598 (155ns)
Part 2: 360341832208407 (145ns)