wip

Author: mdr

Aoc2024/Day08/Parser.lean

@@ -2,20 +2,15 @@ import Aoc2024.Day08.Examples
 import Aoc2024.Day08.Types
 import Aoc2024.Utils
 import Std
-open Std.Internal.Parsec.String
-open Std.Internal.Parsec
 
-instance : Bind List where bind := List.bind
-instance : Pure List where pure := List.pure
-
-private def decorateWithCoordinates (s: String): List (Point × Char) := do
+private def decorateWithCoordinates (s: String): List PointAndChar := do
   let (y, line) <- s.splitOn "\n" |> .enum
   let (x, c) <- line.toList.enum
-  pure (⟨x, y⟩, c)
+  pure ⟨⟨x, y⟩, c⟩
 
 def parseInput (s : String): PuzzleInput :=
   let decoratedChars := decorateWithCoordinates s
-  let (xs, ys) := decoratedChars.map (·.1.toPair) |>.unzip
+  let (xs, ys) := decoratedChars.map (·.point.toPair) |>.unzip
   let width := xs.max?.map (· + 1 |>.toNat) |>.getD 0
   let height := ys.max?.map (· + 1 |>.toNat) |>.getD 0
   let bounds: Rectangle := { topLeft := Point.origin, width, height }

Aoc2024/Day08/Solve.lean

@@ -7,32 +7,20 @@ open Std (HashMap)
 
 -- Part 1
 
-private def groupByChar (decoratedChars : List (Point × Char)) : List (Char × List Point) :=
-  decoratedChars.groupBy (λ (_, c1) (_, c2) => c1 == c2) |>.map (λ l => (l.head!.2, l.map (·.1)))
+private def removeDots (decoratedChars : List PointAndChar) : List PointAndChar := decoratedChars.filter (·.char != '.')
 
-#guard groupByChar [(⟨0, 0⟩, 'a'), (⟨1, 0⟩, 'a'), (⟨0, 1⟩, 'b'), (⟨1, 1⟩, 'b')] == [
-  ('a', [⟨0, 0⟩, ⟨1, 0⟩]),
-  ('b', [⟨0, 1⟩, ⟨1, 1⟩])
-]
-
-private instance hashableChar: Hashable Char where hash c := c.toNat |> hash
-
-private def removeDots (decoratedChars : List (Point × Char)) : List (Point × Char) :=
-  decoratedChars.filter (λ (_, c) => c != '.')
+private def getAntennaeGroups (input : PuzzleInput) : List (List Point) :=
+  input.decoratedChars |> removeDots |>.groupByAndTransformValues (·.char) (·.point) |>.values
 
 private def findAntinodes (antennaGroup : List Point) : List Point := do
   let antenna1 <- antennaGroup
   let antenna2 <- antennaGroup
   if antenna1 != antenna2 then
     return antenna2.add (antenna1.vectorTo antenna2)
-  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 :=
-  getAntennaeGroups input |>.bind findAntinodes |>.filter (input.bounds.contains) |>.toSet.size
+  getAntennaeGroups input |>.flatMap findAntinodes |>.filter (input.bounds.contains) |>.toSet.size
 
 def parseAndSolvePart1 (s : String): Int := parseInput s |> solvePart1
 
@@ -44,15 +32,15 @@ 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 :=
+private def Point.isColinearWith (point : Point) (pair : (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)
+  let antennaePairs := getAntennaeGroups input |>.flatMap combinationPairs
+  let isAntinode (point : Point) : Bool := antennaePairs.any point.isColinearWith -- exploiting special property of the input
   input.bounds.allPoints.countP isAntinode
 
 def parseAndSolvePart2 (s : String): Int := parseInput s |> solvePart2

Aoc2024/Day08/Types.lean

@@ -32,15 +32,23 @@ 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
 
+#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 }
+
 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 }
+#guard Rectangle.allPoints { topLeft := Point.origin, width := 2, height := 2 } ==
+  [{ x := 0, y := 0 }, { x := 0, y := 1 }, { x := 1, y := 0 }, { x := 1, y := 1 }]
+
+structure PointAndChar where
+  point: Point
+  char: Char
+deriving Repr, Inhabited, BEq, Hashable
 
 structure PuzzleInput where
   bounds : Rectangle
-  decoratedChars : List (Point × Char)
-deriving Repr, Inhabited, BEq
+  decoratedChars : List PointAndChar
+deriving Repr, Inhabited, BEq, Hashable

Aoc2024/Utils.lean

@@ -2,7 +2,7 @@ import Std
 import Batteries
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec
-open Std (HashSet)
+open Std (HashSet HashMap)
 
 -- https://brandonrozek.com/blog/writing-unit-tests-lean-4/
 def Except.deq [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by
@@ -166,7 +166,13 @@ namespace List
   #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 :: ·))
+  def groupByKey [BEq α] [Hashable α] (key : β → α) (xs : List β): HashMap α (List β) :=
+     xs.toArray.groupByKey key |>.map (λ _ v => v.toList)
+
+  def groupByAndTransformValues [BEq α] [Hashable α] (key : β → α) (f : β → γ) (xs : List β): HashMap α (List γ) :=
+    xs.groupByKey key |>.map (λ _ v => v.map f)
+
+  def flatMap {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := join (map b a)
 
 end List
 
@@ -217,3 +223,5 @@ def intRange (m n : Int) : List Int :=
 #guard intRange 0 3 == [0, 1, 2]
 #guard intRange (-3) 2 == [-3, -2, -1, 0, 1]
 #guard intRange 1 1 == []
+
+instance hashableChar: Hashable Char where hash c := c.toNat |> hash