wip

Aoc2024/Day07/Solve.lean

@@ -16,7 +16,7 @@ private def Equation.isTrue (equation : Equation) (operators : List Operator) :
 private def Equation.operatorPositions (equation : Equation) : Nat := equation.numbers.length - 1
 
 private def canEquationPossiblyBeTrue (operators : List Operator) (equation : Equation) : Bool :=
-  replicateM equation.operatorPositions operators |>.any equation.isTrue
+  operators.replicateM equation.operatorPositions |>.any equation.isTrue
 
 private def solveGeneric (operators : List Operator) (equations : List Equation) : Int :=
   equations.filter (canEquationPossiblyBeTrue operators) |>.sumBy (·.testValue)

Aoc2024/Day08/Examples.lean

@@ -11,3 +11,55 @@ def exampleInput :=
 .........A..
 ............
 ............"
+
+def puzzleInput :=
+"....K..........................8.................z
+.....n..............r...........z.................
+.......................w....8.............3...E...
+.....Q.....U..4.........8.........................
+...............rc...w........i....................
+...........K.........i..2.........................
+..................4.....i.........................
+K.....n....................w...........z..........
+..U......Q........................I...............
+..........i.....I.....Q....g....................5E
+..Q......................................5........
+..........c............8......w...g..........5....
+.............................I.O..................
+.Z.............4....b.....................k.......
+..n........4......r..g..6..c.............3........
+....Z............c................................
+...................................x..............
+.......................................O..........
+...............U...................E..........5...
+.....f..........................OI3......k........
+..m.......o......F.......R........x...............
+m...........o..v6..3...............X..............
+..............H6v.....F.g.....................W...
+...........o....Fb....v...............E...........
+...Z.............a................................
+......U6.............V............................
+.9.............b..............pTk.................
+.......m........V.........H1....x.................
+...m.................H....................MX......
+............t.a............H......................
+........Z...a............v.....1..T..p.W..X.......
+.............................9...x.......p........
+.....J.....................V..1................0..
+...........r..j..........a............pT..........
+.G..................J...N......f..................
+...........G......T....B........W.e...........M...
+..........j.............Rk.............M..........
+.........q.............MB......R.F..1..P....X...f.
+............................V....o...........h....
+...........................................W......
+......b......u............................e.......
+.............................................0....
+..CA....Gt..O........................7.....e....0.
+C.u......A..9J..N........................h.....e..
+uj....q..........N.2..................7...........
+G....N.....uJ...............................0.....
+.................B................P.......h.......
+...C....q...........R.........P...................
+.....q..tC....2.9.....B............P....f.........
+...............2.................................7"

Aoc2024/Day08/Main.lean

@@ -10,7 +10,7 @@ def main : IO Unit := do
   IO.println s!"Example: {parseAndSolvePart1 exampleInput}"
   let answerPart1 := parseAndSolvePart1 puzzleInput
   IO.println s!"Puzzle: {answerPart1}"
-  assert! (answerPart1 == -1)
+  assert! (answerPart1 == 344)
   IO.println ""
   IO.println "Part 2"
   IO.println s!"Example: {parseAndSolvePart2 exampleInput}"

Aoc2024/Day08/Parser.lean

@@ -5,7 +5,6 @@ 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
 
@@ -21,5 +20,3 @@ def parseInput (s : String): PuzzleInput :=
   let height := ys.max?.map (· + 1 |>.toNat) |>.getD 0
   let bounds: Rectangle := { topLeft := Point.origin, width, height }
   { bounds, decoratedChars }
-
--- #guard parseInput exampleInput == ??

Aoc2024/Day08/Solve.lean

@@ -2,6 +2,8 @@ import Aoc2024.Utils
 import Aoc2024.Day08.Examples
 import Aoc2024.Day08.Parser
 import Aoc2024.Day08.Types
+import Std
+open Std (HashMap)
 
 -- Part 1
 
@@ -13,21 +15,32 @@ private def groupByChar (decoratedChars : List (Point × Char)) : List (Char ×
   ('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 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 solvePart1 (input : PuzzleInput) : Int :=
-  let groups := input.decoratedChars |> removeDots |> groupByChar
-  sorry
+  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
 
 def parseAndSolvePart1 (s : String): Int := parseInput s |> solvePart1
 
--- #guard parseAndSolvePart1 exampleInput == 14
+#guard parseAndSolvePart1 exampleInput == 14
 
 -- Part 2
 
 private def solvePart2 (input : PuzzleInput) : Int := sorry
 
 def parseAndSolvePart2 (s : String): Int := parseInput s |> solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == -1
+-- #guard parseAndSolvePart2 exampleInput == 34

Aoc2024/Day08/Types.lean

@@ -10,6 +10,17 @@ def Point.toPair (p : Point) : (Int × Int) := (p.x, p.y)
 
 def Point.origin : Point := { x := 0, y := 0 }
 
+structure Vector where
+  x : Int
+  y : Int
+deriving BEq, Hashable, Repr, Inhabited
+
+def Point.vectorTo (from_ to : Point) : Vector := { x := to.x - from_.x, y := to.y - from_.y }
+#guard ({ x := 1, y := 1 } : Point).vectorTo { x := 2, y := 2 } == { x := 1, y := 1 }
+
+def Point.add (p : Point) (v : Vector) : Point := { x := p.x + v.x, y := p.y + v.y }
+#guard Point.add { x := 1, y := 1 } { x := 2, y := 2 } == { x := 3, y := 3 }
+
 structure Rectangle where
   topLeft : Point
   width: Nat

Aoc2024/Utils.lean

@@ -134,6 +134,15 @@ namespace List
     ) none
   #guard [1, 2, 3, 4].maxBy id == some 4
 
+  def replicateM (n : Nat) (options : List α) : List (List α) :=
+    let rec loop (n : Nat) (acc : List (List α)) : List (List α) :=
+      match n with
+      | 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]]
+
 end List
 
 namespace Std.HashSet
@@ -171,12 +180,3 @@ namespace Option
   #guard (some 42).getOrThrow "Error" == Except.ok 42
   #guard (none : Option Int).getOrThrow "Error" == Except.error "Error"
 end Option
-
-def replicateM (n : Nat) (options : List α) : List (List α) :=
-  let rec loop (n : Nat) (acc : List (List α)) : List (List α) :=
-    match n with
-    | 0 => acc
-    | n + 1 => loop n (acc.bind λ l => options.map (λ o => o :: l))
-  loop n [[]]
-#guard replicateM 0 [1, 2] == [[]]
-#guard replicateM 3 [1, 2] == [[1, 1, 1], [2, 1, 1], [1, 2, 1], [2, 2, 1], [1, 1, 2], [2, 1, 2], [1, 2, 2], [2, 2, 2]]