Advent Of Code 2025 - Day 7

Stream: general

[Alfredo Moreira-Rosa]

This is my solution for day 7 of Advent of Code.
I'm really happy with the solution, using HashSet for part 1 and HashMap for part 2.
Main surprise was that Lean core don't define intersection, difference or unionWith out of the box.
So i defined them.
The solution ends up being really small thanks to those helpers. Parsing was also really simple.

Solution

import Std.Data.HashSet
import Std.Data.HashMap
import LeanAoc.utils.HashSet
import LeanAoc.utils.HashMap

def parseInput (s: String): List (List Nat) :=
  s.splitOn "\n" |>.map (fun line =>
    line.toList.zipIdx |>.filterMap (fun (c, i) =>
      if c ≠ '.' then some i else none))

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

-- PART 1

def splitTachyons (acc: (Std.HashSet Nat × Nat)) (splitters: Std.HashSet Nat) : (Std.HashSet Nat × Nat) :=
  let (tachyons, count) := acc
  let hits := tachyons ∩ splitters
  let notHits := tachyons \ splitters
  (notHits ∪ hits.map (· + 1) ∪ hits.map (· - 1), count + hits.size)


def countSplitTachyonBeams (input: List (List Nat)) : Nat :=
  match input with
  | [] => 0
  | beam :: diagramList =>
    let init := Std.HashSet.ofList beam
    let diagram := diagramList.map Std.HashSet.ofList
    diagram.foldl splitTachyons (init, 0) |>.2

/--
info: 21
-/
#guard_msgs in
#eval do
  let inputStr := ".......S.......
...............
.......^.......
...............
......^.^......
...............
.....^.^.^.....
...............
....^.^...^....
...............
...^.^...^.^...
...............
..^...^.....^..
...............
.^.^.^.^.^...^.
..............."
  let input := parseInput inputStr
  return countSplitTachyonBeams input

#eval do
  let inputStr ← readInput
  let input := parseInput inputStr
  return countSplitTachyonBeams input

-- PART 2

def splitQuantumTachyons (tachyons splitters: Std.HashMap Nat Nat) : Std.HashMap Nat Nat :=
  let hits := tachyons ∩ splitters
  let notHits := tachyons \ splitters
  notHits ∪⁺ hits.mapKey (· + 1) ∪⁺ hits.mapKey (· - 1)

def countSplitQuantumTachyonBeams (input: List (List Nat)) : Nat :=
  match input.map (·.map (·, 1)) with
  | [] => 0
  | beam :: diagramList =>
    let init := Std.HashMap.ofList beam
    let diagram := diagramList.map Std.HashMap.ofList
    let manyWorlds := diagram.foldl splitQuantumTachyons init
    manyWorlds.values.sum

/--
info: 40
-/
#guard_msgs in
#eval do
  let inputStr := ".......S.......
...............
.......^.......
...............
......^.^......
...............
.....^.^.^.....
...............
....^.^...^....
...............
...^.^...^.^...
...............
..^...^.....^..
...............
.^.^.^.^.^...^.
..............."
  let input := parseInput inputStr
  return countSplitQuantumTachyonBeams input

#eval do
  let inputStr ← readInput
  let input := parseInput inputStr
  return countSplitQuantumTachyonBeams input

Here are my HashSet Helpers :

import Std.Data.HashSet

namespace Std.HashSet

def map [BEq α] [BEq β] [Hashable α] [Hashable β] (s : HashSet α) (f : α → β) : HashSet β :=
  s.fold (fun acc x => acc.insert (f x)) (HashSet.emptyWithCapacity)

def intersection {α : Type} [BEq α] [Hashable α] (s1 s2 : HashSet α) : HashSet α :=
  s1.filter (fun x => s2.contains x)

def difference {α : Type} [BEq α] [Hashable α] (s1 s2 : HashSet α) : HashSet α :=
  s1.filter (fun x => ¬ s2.contains x)

instance {α : Type} [BEq α] [Hashable α] : Inter (HashSet α) where
  inter := intersection

instance {α : Type} [BEq α] [Hashable α] : SDiff (HashSet α) where
  sdiff := difference

end Std.HashSet

And here are the HashMap ones :

import Std.Data.HashMap

namespace Std.HashMap

def mapKey [BEq α] [BEq β] [BEq γ] [Hashable α] [Hashable β] [Hashable γ]
    (m : HashMap α β) (f : α → γ) : HashMap γ β :=
  m.fold (fun acc k v => acc.insert (f k) v) (HashMap.emptyWithCapacity)

def unionWith {α β : Type} [BEq α] [Hashable α] [BEq β] [Hashable β] (f : β → β → β) (m1 m2 : HashMap α β) : HashMap α β :=
  m2.fold (fun acc k v =>
    match acc.get? k with
    | some v' => acc.insert k (f v' v)
    | none => acc.insert k v) m1

def intersection {α β : Type} [BEq α] [Hashable α] [BEq β] [Hashable β] (m1 m2 : HashMap α β) : HashMap α β :=
  m1.fold (fun acc k v =>
    if m2.contains k then
      acc.insert k v
    else
      acc) (HashMap.emptyWithCapacity)

def difference {α β : Type} [BEq α] [Hashable α] [BEq β] [Hashable β] (m1 m2 : HashMap α β) : HashMap α β :=
  m1.fold (fun acc k v =>
    if ¬ m2.contains k then
      acc.insert k v
    else
      acc) (HashMap.emptyWithCapacity)

instance {α β : Type} [BEq α] [Hashable α] [BEq β] [Hashable β] : Inter (HashMap α β) where
  inter := intersection

instance {α β : Type} [BEq α] [Hashable α] [BEq β] [Hashable β] : SDiff (HashMap α β) where
  sdiff := difference

class UnionPlus (α : Type u) where
  unionPlus : α → α → α

infixl:65 " ∪⁺ " => UnionPlus.unionPlus

instance {α β : Type} [BEq α] [Hashable α] [BEq β] [Hashable β] [Add β] : UnionPlus (HashMap α β) where
  unionPlus := unionWith (· + ·)

end Std.HashMap

[Alfredo Moreira-Rosa]

And execution time are also suprisingly good (so i suspect i'm measuring it badly, because part 2 is expected to be slower):

Running Day 7...
Parsing time: 8.12ms
Part 1: 1524 (461ns)
Part 2: 32982105837605 (237ns)

[Kim Morrison]

Alfredo Moreira-Rosa said:

Main surprise was that Lean core don't define intersection, difference or unionWith out of the box.

I think these are (mostly?) in the nightlies, arriving in v4.27.0-rc1 in a few days.

[Alfredo Moreira-Rosa]

Good news. Thanks for the insight!