tidying

Aoc2024/Day04/Main.lean

@@ -8,8 +8,12 @@ def main : IO Unit := do
   let exampleInput <- IO.FS.readFile "Aoc2024/Day04/inputs/example.txt"
   let puzzleInput <- IO.FS.readFile "Aoc2024/Day04/inputs/input.txt"
   IO.println s!"Example: {solvePart1 exampleInput}"
-  IO.println s!"Puzzle: {solvePart1 puzzleInput}" -- 2524
+  let answerPart1 := solvePart1 puzzleInput
+  IO.println s!"Puzzle: {answerPart1}"
+  assert! (answerPart1 == 2524)
   IO.println ""
   IO.println "Part 2"
   IO.println s!"Example: {solvePart2 exampleInput}"
-  IO.println s!"Puzzle: {solvePart2 puzzleInput}" --
+  let answerPart2 := solvePart2 puzzleInput
+  IO.println s!"Puzzle: {answerPart2}"
+  assert! (answerPart2 == 1873)

Aoc2024/Day04/Solve.lean

@@ -51,17 +51,49 @@ private def allGridTransformations : List (Grid -> Grid) := [
   diagonals ∘ flipHorizontal,
 ]
 
-def solvePart1 (s : String): Int :=
-  let grid := parseGrid s
-  allGridTransformations.sumBy (λ transformation => transformation grid |> countXmasOccurrencesInRows)
+private def transformGridInAllWays (grid : Grid) : List Grid := allGridTransformations.map (· grid)
 
-#eval solvePart1 exampleInput1
+def solvePart1 (s : String): Int := parseGrid s |> transformGridInAllWays |>.sumBy countXmasOccurrencesInRows
 
 #guard solvePart1 exampleInput1 = 4
 #guard solvePart1 exampleInput2 = 18
 
 -- Part 2
 
-def solvePart2 (things : s) : Int := sorry
+private def slidingGrids (grid : Grid): List Grid :=
+  grid.slidingWindows 3 |>.bind (λ rowBundle => rowBundle.map (List.slidingWindows 3) |>.transpose)
+
+#guard slidingGrids [['A', 'B', 'C', 'D', 'E'], ['F', 'G', 'H', 'I', 'J'], ['K', 'L', 'M', 'N', 'O']] ==
+[
+  [
+    ['A', 'B', 'C'],
+    ['F', 'G', 'H'],
+    ['K', 'L', 'M']
+  ], [
+    ['B', 'C', 'D'],
+    ['G', 'H', 'I'],
+    ['L', 'M', 'N']
+  ], [
+    ['C', 'D', 'E'],
+    ['H', 'I', 'J'],
+    ['M', 'N', 'O']
+  ]
+]
+
+private def is2Mas: Grid -> Bool
+  | [r1, r2, r3] =>
+    let match1 := match r1 with | ['M', _, 'S'] => true | _ => false
+    let match2 := match r2 with | [_, 'A', _] => true | _ => false
+    let match3 := match r3 with | ['M', _, 'S'] => true | _ => false
+    match1 && match2 && match3
+  | _ => false
+
+private def rotate90 (grid : Grid) : Grid := grid.transpose.map (·.reverse)
+
+private def allRotations (grid : Grid) : List Grid :=
+  [grid, rotate90 grid, iterate 2 rotate90 grid, iterate 3 rotate90 grid]
+
+def solvePart2 (s : String) : Int :=
+  parseGrid s |> slidingGrids |>.bind allRotations |>.countP is2Mas
 
--- #guard solvePart2 exampleInput2 = 9
+#guard solvePart2 exampleInput2 = 9

Aoc2024/Utils.lean

@@ -57,6 +57,14 @@ namespace List
   def differences (xs: List Int) : List Int :=
     xs.zip xs.tail |>.map (λ (a, b) => b - a)
 
+  def slidingWindows (n : Nat) (xs : List α) : List (List α) :=
+    match xs with
+      | [] => []
+      | (x :: xs) =>
+        let window := x :: xs.take (n - 1)
+        if window.length < n then []
+        else window :: slidingWindows n xs
+
 end List
 
 #guard [].sum = 0
@@ -68,6 +76,12 @@ end List
 #guard [1].differences == []
 #guard [1, 2, 3, 2, 5].differences == [1, 1, -1, 3]
 
+#guard [1, 2, 3, 4, 5].slidingWindows 2 = [[1, 2], [2, 3], [3, 4], [4, 5]]
+#guard [1, 2, 3, 4, 5].slidingWindows 1 = [[1], [2], [3], [4], [5]]
+#guard [1, 2, 3, 4, 5].slidingWindows 0 = [[1], [2], [3], [4], [5]]
+#guard [1].slidingWindows 2 = []
+#guard ([]: List Nat).slidingWindows 2 = []
+
 namespace Std.HashSet
 
   def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=
@@ -83,3 +97,8 @@ namespace String
 end String
 
 #guard "1\n2\n3".lines == ["1", "2", "3"]
+
+def iterate (n : Nat) (f : α -> α) (x : α) : α :=
+  match n with
+  | 0 => x
+  | n + 1 => iterate n f (f x)