tidying

Aoc2024/Day04/Solve.lean

@@ -13,43 +13,19 @@ private def countXmasOccurrencesInRow : List Char -> Int
 
 #guard countXmasOccurrencesInRow "ABXMASXMASXMA".toList == 2
 
-private def countXmasOccurrencesInRows (grid : Grid): Int :=
-  grid.sumBy countXmasOccurrencesInRow
+private def countXmasOccurrencesInRows (grid : Grid): Int := grid.sumBy countXmasOccurrencesInRow
 
 private def gridToString (g : Grid) : String := g.map List.asString |> String.intercalate "\n"
 
 #guard gridToString [['A', 'B', 'C'], ['D', 'E', 'F']] = "ABC\nDEF"
 
 private def flipHorizontal (grid : Grid) : Grid := grid.map (·.reverse)
 
--- ported from https://hackage.haskell.org/package/universe-base-1.1.4/docs/src/Data.Universe.Helpers.html#diagonals
-private def diagonals (grid : List (List α)) : List (List α) :=
-  let rec go (b : List (List α)) (es : List (List α)) : List (List α) :=
-    let diagonal := b.filterMap List.head?
-    let ts := b.filterMap List.tail?
-    diagonal :: match es with
-      | [] => ts.transpose
-      | e :: es' => go (e :: ts) es'
-  (go [] grid).tail!
-
-#guard diagonals [
-  ["A", "B", "C", "D"],
-  ["E", "F", "G", "H"],
-  ["I", "J", "K", "L"],
-] == [
-  ["A"],
-  ["E", "B"],
-  ["I", "F", "C"],
-  ["J", "G", "D"],
-  ["K", "H"],
-  ["L"],
-]
-
 private def allGridTransformations : List (Grid -> Grid) := [
   id,
   List.transpose,
-  diagonals,
-  diagonals ∘ flipHorizontal,
+  List.diagonals,
+  List.diagonals ∘ flipHorizontal,
 ]
 
 private def transformGridInAllWays (grid : Grid) : List Grid := allGridTransformations.map (· grid)

Aoc2024/Utils.lean

@@ -1,4 +1,5 @@
 import Std
+import Batteries
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec
 open Std (HashSet)
@@ -49,14 +50,23 @@ namespace List
 
   def sum (xs: List Int) : Int := xs.foldl .add 0
 
+  #guard [].sum = 0
+  #guard [1, 2, 3].sum = 6
+
   def sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (λ acc x => acc + f x) 0
 
+  #guard [1, 2, 3].sumBy (λ x => x * x) = 14
+
   def toSet {α:Type} [BEq α] [Hashable α] (xs: List α) : HashSet α :=
     HashSet.ofList xs
 
   def differences (xs: List Int) : List Int :=
     xs.zip xs.tail |>.map (λ (a, b) => b - a)
 
+  #guard [].differences == []
+  #guard [1].differences == []
+  #guard [1, 2, 3, 2, 5].differences == [1, 1, -1, 3]
+
   def slidingWindows (n : Nat) (xs : List α) : List (List α) :=
     match xs with
       | [] => []
@@ -65,23 +75,36 @@ namespace List
         if window.length < n then []
         else window :: slidingWindows n xs
 
+  #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 = []
+
+  -- ported from https://hackage.haskell.org/package/universe-base-1.1.4/docs/src/Data.Universe.Helpers.html#diagonals
+  def diagonals (grid : List (List α)) : List (List α) :=
+    let rec go (b : List (List α)) (es : List (List α)) : List (List α) :=
+      let diagonal := b.filterMap List.head?
+      let ts := b.filterMap List.tail?
+      diagonal :: match es with
+        | [] => ts.transpose
+        | e :: es' => go (e :: ts) es'
+    (go [] grid).tail!
+
+  #guard [
+    ["A", "B", "C", "D"],
+    ["E", "F", "G", "H"],
+    ["I", "J", "K", "L"],
+  ].diagonals = [
+    ["A"],
+    ["E", "B"],
+    ["I", "F", "C"],
+    ["J", "G", "D"],
+    ["K", "H"],
+    ["L"],
+  ]
 end List
 
-#guard [].sum = 0
-#guard [1, 2, 3].sum = 6
-
-#guard [1, 2, 3].sumBy (λ x => x * x) = 14
-
-#guard [].differences == []
-#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 :=