From c8dd6d5dad60100d5f72d547eca9ffc209f333b0 Mon Sep 17 00:00:00 2001
From: Matt Russell <MattRussellUK@gmail.com>
Date: Mon, 2 Dec 2024 08:19:36 +0000
Subject: [PATCH] utils

---
 Aoc2024/Day02/Solve.lean | 24 ++++----------------
 Aoc2024/Utils.lean       | 49 ++++++++++++++++++++++++----------------
 2 files changed, 35 insertions(+), 38 deletions(-)

diff --git a/Aoc2024/Day02/Solve.lean b/Aoc2024/Day02/Solve.lean
index d80a4bd..67de237 100644
--- a/Aoc2024/Day02/Solve.lean
+++ b/Aoc2024/Day02/Solve.lean
@@ -5,18 +5,12 @@ import Aoc2024.Day02.Examples
 open Std (HashSet)
 namespace Aoc2024.Day02
 
-private def increasingSlowly: HashSet Int := HashSet.ofList [1, 2, 3]
-private def decreasingSlowly: HashSet Int := HashSet.ofList [-1, -2, -3]
-
-private def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=
-  xs.all ys.contains
-
-#guard isSubsetOf (HashSet.ofList [1, 3]) (HashSet.ofList [1, 2, 3]) == true
-#guard isSubsetOf (HashSet.ofList [1, 4]) (HashSet.ofList [1, 2, 3]) == false
+private def increasingSlowly: HashSet Int := [1, 2, 3].toSet
+private def decreasingSlowly: HashSet Int := [-1, -2, -3].toSet
 
 private def isSafe (report : Report) : Bool :=
-  let diffs := differences report |> HashSet.ofList
-  isSubsetOf diffs increasingSlowly || isSubsetOf diffs decreasingSlowly
+  let diffs := report.differences.toSet
+  diffs.isSubsetOf increasingSlowly || diffs.isSubsetOf decreasingSlowly
 
 #guard isSafe [7, 6, 4, 2, 1] == true
 #guard isSafe [1, 2, 7, 8, 9] == false
@@ -31,16 +25,8 @@ def parseAndSolvePart1 (s : String): Except String Int := parseReports s |>.map
 
 #guard parseAndSolvePart1 exampleInput == Except.ok 2
 
-private def removeNth (n: Nat) (xs: List α) : List α :=
-  xs.take n ++ xs.drop (n + 1)
-
-#guard removeNth 0 [1, 2, 3] == [2, 3]
-#guard removeNth 1 [1, 2, 3] == [1, 3]
-#guard removeNth 2 [1, 2, 3] == [1, 2]
-#guard removeNth 3 [1, 2, 3] == [1, 2, 3]
-
 private def isSafeWithTolerance (report : Report) : Bool :=
-  List.range report.length |>.map (λ n => removeNth n report) |>.any isSafe
+  List.range report.length |>.map report.removeNth |>.any isSafe
 
 private def solvePart2 (reports : List Report) : Int := reports.countP isSafeWithTolerance
 
diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean
index c19e6fa..b86c332 100644
--- a/Aoc2024/Utils.lean
+++ b/Aoc2024/Utils.lean
@@ -3,10 +3,6 @@ open Std.Internal.Parsec.String
 open Std.Internal.Parsec
 open Std (HashSet)
 
-def List.sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (λ acc x => acc + f x) 0
-
-#guard [1, 2, 3].sumBy (λ x => x * x) = 14
-
 -- https://brandonrozek.com/blog/writing-unit-tests-lean-4/
 def Except.deq [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by
   unfold DecidableEq
@@ -49,23 +45,38 @@ def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) :=
 #guard (sepBy digits (skipChar ',')).run "4" == .ok [4]
 #guard (sepBy digits (skipChar ',')).run "" == .ok []
 
-def differences (xs: List Int) : List Int :=
-  xs.zip xs.tail |>.map (λ (a, b) => b - a)
+namespace List
+
+  def sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (λ acc x => acc + f x) 0
+
+  def toSet {α:Type} [BEq α] [Hashable α] (xs: List α) : HashSet α :=
+    HashSet.ofList xs
+
+  def removeNth (n: Nat) (xs: List α) : List α :=
+    xs.take n ++ xs.drop (n + 1)
+
+  def differences (xs: List Int) : List Int :=
+    xs.zip xs.tail |>.map (λ (a, b) => b - a)
+
+end List
+
+#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 differences [] == []
-#guard differences [1] == []
-#guard differences [1, 2, 3, 2, 5] == [1, 1, -1, 3]
+#guard [1, 2, 3].removeNth 0 == [2, 3]
+#guard [1, 2, 3].removeNth 1 == [1, 3]
+#guard [1, 2, 3].removeNth 2 == [1, 2]
+#guard [1, 2, 3].removeNth 3 == [1, 2, 3]
 
-def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=
-  xs.all ys.contains
+namespace Std.HashSet
 
-#guard isSubsetOf (HashSet.ofList [1, 3]) (HashSet.ofList [1, 2, 3]) == true
-#guard isSubsetOf (HashSet.ofList [1, 4]) (HashSet.ofList [1, 2, 3]) == false
+  def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=
+    xs.all ys.contains
 
-def removeNth (n: Nat) (xs: List α) : List α :=
-  xs.take n ++ xs.drop (n + 1)
+end Std.HashSet
 
-#guard removeNth 0 [1, 2, 3] == [2, 3]
-#guard removeNth 1 [1, 2, 3] == [1, 3]
-#guard removeNth 2 [1, 2, 3] == [1, 2]
-#guard removeNth 3 [1, 2, 3] == [1, 2, 3]
+#guard [1, 3].toSet.isSubsetOf [1, 2, 3].toSet == true
+#guard [1, 2, 3].toSet.isSubsetOf [1, 3].toSet == false