day8

Aoc2024/Day08/Main.lean

@@ -16,4 +16,4 @@ def main : IO Unit := do
   IO.println s!"Example: {parseAndSolvePart2 exampleInput}"
   let answerPart2 := parseAndSolvePart2 puzzleInput
   IO.println s!"Puzzle: {answerPart2}"
-  assert! (answerPart2 == -1)
+  assert! (answerPart2 == 1182)

Aoc2024/Day08/Solve.lean

@@ -28,19 +28,33 @@ private def findAntinodes (antennaGroup : List Point) : List Point := do
   else
     []
 
+private def getAntennaeGroups (input : PuzzleInput) : List (List Point) :=
+  input.decoratedChars |> removeDots |>.toArray.groupByKey (·.2) |>.map (λ _ v => v.map (·.1) |>.toList) |>.values
+
 private def solvePart1 (input : PuzzleInput) : Int :=
-  let antennasByFrequency : HashMap Char (List Point) :=
-    input.decoratedChars |> removeDots |>.toArray.groupByKey (·.2) |>.map (λ _ v => v.map (·.1) |>.toList)
-  antennasByFrequency.values.bind findAntinodes |>.filter (input.bounds.contains) |>.toSet.size
+  getAntennaeGroups input |>.bind findAntinodes |>.filter (input.bounds.contains) |>.toSet.size
 
 def parseAndSolvePart1 (s : String): Int := parseInput s |> solvePart1
 
 #guard parseAndSolvePart1 exampleInput == 14
 
 -- Part 2
 
-private def solvePart2 (input : PuzzleInput) : Int := sorry
+private def combinationPairs [BEq α] (xs : List α) : List (α × α) := do
+  let [x1, x2] <- xs.combinations 2 | []
+  return (x1, x2)
+
+private def isInLineWith (pair : (Point × Point)) (point : Point) : Bool :=
+  let (p1, p2) := pair
+  let v1 := p1.vectorTo p2
+  let v2 := p1.vectorTo point
+  v1.x * v2.y == v1.y * v2.x
+
+private def solvePart2 (input : PuzzleInput) : Int :=
+  let antennaePairs := getAntennaeGroups input |>.bind combinationPairs
+  let isAntinode (point : Point) : Bool := antennaePairs.any (λ pair => isInLineWith pair point)
+  input.bounds.allPoints.countP isAntinode
 
 def parseAndSolvePart2 (s : String): Int := parseInput s |> solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == 34
+#guard parseAndSolvePart2 exampleInput == 34

Aoc2024/Day08/Types.lean

@@ -1,3 +1,4 @@
+import Aoc2024.Utils
 import Std
 open Std (HashSet)
 
@@ -31,6 +32,11 @@ def Rectangle.contains (r : Rectangle) (p : Point) : Bool :=
   r.topLeft.x ≤ p.x && p.x < r.topLeft.x + r.width &&
     r.topLeft.y ≤ p.y && p.y < r.topLeft.y + r.height
 
+def Rectangle.allPoints (r : Rectangle) : List Point := do
+  let x <- intRange r.topLeft.x (r.topLeft.x + r.width)
+  let y <- intRange r.topLeft.y (r.topLeft.y + r.height)
+  return { x := x, y := y }
+
 #guard Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 1, y := 1 }
 #guard !Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 2, y := 2 }
 

Aoc2024/Utils.lean

@@ -46,6 +46,9 @@ def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) :=
 #guard (sepBy digits (skipChar ',')).run "4" == .ok [4]
 #guard (sepBy digits (skipChar ',')).run "" == .ok []
 
+instance listBind: Bind List where bind := List.bind
+instance listPure: Pure List where pure := List.pure
+
 namespace List
 
   def sum (xs: List Int) : Int := xs.foldl .add 0
@@ -132,6 +135,7 @@ namespace List
       | some y => if f x > f y then some x else some y
       | none => some x
     ) none
+
   #guard [1, 2, 3, 4].maxBy id == some 4
 
   def replicateM (n : Nat) (options : List α) : List (List α) :=
@@ -140,9 +144,30 @@ namespace List
       | 0 => acc
       | n + 1 => loop n (acc.bind λ l => options.map (λ o => o :: l))
     loop n [[]]
+
   #guard [1, 2].replicateM 0 == [[]]
   #guard [1, 2].replicateM 3 == [[1, 1, 1], [2, 1, 1], [1, 2, 1], [2, 2, 1], [1, 1, 2], [2, 1, 2], [1, 2, 2], [2, 2, 2]]
 
+  def eraseAll [BEq α] (x: α) (xs : List α)  : List α := xs.filter (· != x)
+  #guard [1, 2, 3, 2].eraseAll 2 == [1, 3]
+
+  def combinations {α} [BEq α] (n : Nat) (xs : List α) : List (List α) :=
+    match n with
+      | 0 => [[]]
+      | n + 1 =>
+        match xs with
+          | [] => []
+          | x :: xs => (xs.combinations n).map (x :: ·) ++ xs.combinations (n + 1)
+
+  #guard [1, 2, 3].combinations 0 == [[]]
+  #guard [1, 2, 3].combinations 1 == [[1], [2], [3]]
+  #guard [1, 2, 3].combinations 2 == [[1, 2], [1, 3], [2, 3]]
+  #guard [1, 2, 3].combinations 3 == [[1, 2, 3]]
+  #guard [1, 2, 3].combinations 4 == []
+  #guard [1, 2, 3, 4].combinations 2 == [[1, 2], [1, 3], [1, 4], [2, 3], [2, 4], [3, 4]]
+
+      -- xs.bind (λ x => (xs.filter (· != x)).combinations n.map (x :: ·))
+
 end List
 
 namespace Std.HashSet
@@ -180,3 +205,15 @@ namespace Option
   #guard (some 42).getOrThrow "Error" == Except.ok 42
   #guard (none : Option Int).getOrThrow "Error" == Except.error "Error"
 end Option
+
+def natRange (from_ to : Nat) : List Nat :=
+  let ns := List.range (to - from_)
+  ns.map (· + from_)
+#guard natRange 0 3 == [0, 1, 2]
+#guard natRange 1 4 == [1, 2, 3]
+
+def intRange (m n : Int) : List Int :=
+  ((List.range (Int.toNat (n - m))) : List Nat).map fun (r : Nat) => (m + r : Int)
+#guard intRange 0 3 == [0, 1, 2]
+#guard intRange (-3) 2 == [-3, -2, -1, 0, 1]
+#guard intRange 1 1 == []

DayXX/Types.lean

@@ -0,0 +1 @@
+import Aoc2024.Utils