From 335ee643f4c9924c93edacec68b7772c6d4e0ec6 Mon Sep 17 00:00:00 2001 From: Matt Russell Date: Sun, 8 Dec 2024 13:00:32 +0000 Subject: [PATCH] day8 --- Aoc2024/Day08/Main.lean | 2 +- Aoc2024/Day08/Solve.lean | 24 +++++++++++++++++++----- Aoc2024/Day08/Types.lean | 6 ++++++ Aoc2024/Utils.lean | 37 +++++++++++++++++++++++++++++++++++++ DayXX/Types.lean | 1 + 5 files changed, 64 insertions(+), 6 deletions(-) diff --git a/Aoc2024/Day08/Main.lean b/Aoc2024/Day08/Main.lean index 30ccf01..f2f8a9c 100644 --- a/Aoc2024/Day08/Main.lean +++ b/Aoc2024/Day08/Main.lean @@ -16,4 +16,4 @@ def main : IO Unit := do IO.println s!"Example: {parseAndSolvePart2 exampleInput}" let answerPart2 := parseAndSolvePart2 puzzleInput IO.println s!"Puzzle: {answerPart2}" - assert! (answerPart2 == -1) + assert! (answerPart2 == 1182) diff --git a/Aoc2024/Day08/Solve.lean b/Aoc2024/Day08/Solve.lean index 33b384e..dca931b 100644 --- a/Aoc2024/Day08/Solve.lean +++ b/Aoc2024/Day08/Solve.lean @@ -28,10 +28,11 @@ private def findAntinodes (antennaGroup : List Point) : List Point := do 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 := - 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 + getAntennaeGroups input |>.bind findAntinodes |>.filter (input.bounds.contains) |>.toSet.size def parseAndSolvePart1 (s : String): Int := parseInput s |> solvePart1 @@ -39,8 +40,21 @@ def parseAndSolvePart1 (s : String): Int := parseInput s |> solvePart1 -- Part 2 -private def solvePart2 (input : PuzzleInput) : Int := sorry +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 := + 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) + input.bounds.allPoints.countP isAntinode def parseAndSolvePart2 (s : String): Int := parseInput s |> solvePart2 --- #guard parseAndSolvePart2 exampleInput == 34 +#guard parseAndSolvePart2 exampleInput == 34 diff --git a/Aoc2024/Day08/Types.lean b/Aoc2024/Day08/Types.lean index c604c03..ce8636a 100644 --- a/Aoc2024/Day08/Types.lean +++ b/Aoc2024/Day08/Types.lean @@ -1,3 +1,4 @@ +import Aoc2024.Utils import Std open Std (HashSet) @@ -31,6 +32,11 @@ 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 +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 } diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean index e8abe42..2ddc037 100644 --- a/Aoc2024/Utils.lean +++ b/Aoc2024/Utils.lean @@ -46,6 +46,9 @@ def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) := #guard (sepBy digits (skipChar ',')).run "4" == .ok [4] #guard (sepBy digits (skipChar ',')).run "" == .ok [] +instance listBind: Bind List where bind := List.bind +instance listPure: Pure List where pure := List.pure + namespace List def sum (xs: List Int) : Int := xs.foldl .add 0 @@ -132,6 +135,7 @@ namespace List | some y => if f x > f y then some x else some y | none => some x ) none + #guard [1, 2, 3, 4].maxBy id == some 4 def replicateM (n : Nat) (options : List α) : List (List α) := @@ -140,9 +144,30 @@ namespace List | 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]] + def eraseAll [BEq α] (x: α) (xs : List α) : List α := xs.filter (· != x) + #guard [1, 2, 3, 2].eraseAll 2 == [1, 3] + + def combinations {α} [BEq α] (n : Nat) (xs : List α) : List (List α) := + match n with + | 0 => [[]] + | n + 1 => + match xs with + | [] => [] + | x :: xs => (xs.combinations n).map (x :: ·) ++ xs.combinations (n + 1) + + #guard [1, 2, 3].combinations 0 == [[]] + #guard [1, 2, 3].combinations 1 == [[1], [2], [3]] + #guard [1, 2, 3].combinations 2 == [[1, 2], [1, 3], [2, 3]] + #guard [1, 2, 3].combinations 3 == [[1, 2, 3]] + #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 :: ·)) + end List namespace Std.HashSet @@ -180,3 +205,15 @@ namespace Option #guard (some 42).getOrThrow "Error" == Except.ok 42 #guard (none : Option Int).getOrThrow "Error" == Except.error "Error" end Option + +def natRange (from_ to : Nat) : List Nat := + let ns := List.range (to - from_) + ns.map (· + from_) +#guard natRange 0 3 == [0, 1, 2] +#guard natRange 1 4 == [1, 2, 3] + +def intRange (m n : Int) : List Int := + ((List.range (Int.toNat (n - m))) : List Nat).map fun (r : Nat) => (m + r : Int) +#guard intRange 0 3 == [0, 1, 2] +#guard intRange (-3) 2 == [-3, -2, -1, 0, 1] +#guard intRange 1 1 == [] diff --git a/DayXX/Types.lean b/DayXX/Types.lean index e69de29..59780fa 100644 --- a/DayXX/Types.lean +++ b/DayXX/Types.lean @@ -0,0 +1 @@ +import Aoc2024.Utils