part 2

Author: mdr

Aoc2024/Day07/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 == 637696070419031)

Aoc2024/Day07/Solve.lean

@@ -5,13 +5,16 @@ import Aoc2024.Day07.Types
 
 -- Part 1
 
+private def concatenate (a : Int) (b : Int) : Int := (reprStr a ++ reprStr b).toInt!
+
 private def evalNumbers (numbers : List Int) (operators : List Operator): Int :=
   match numbers with
     | [] => 0
     | h :: t =>
       t.zip operators |>.foldl (fun acc (n, op) => match op with
         | .add => acc + n
         | .multiply => acc * n
+        | .concatenation => concatenate acc n
       ) h
 
 #guard evalNumbers [11, 6, 16, 20] [.add, .multiply, .add] == 292
@@ -25,21 +28,22 @@ private def replicateM (n : Nat) (options : List α) : List (List α) :=
 #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]]
 
-private def canEquationPossiblyBeTrue (equation : Equation) : Bool :=
-  let operators := replicateM equation.numbers.length [.add, .multiply]
+private def canEquationPossiblyBeTrue (operators : List Operator) (equation : Equation) : Bool :=
+  let operators := replicateM equation.numbers.length operators
   operators.any λ ops => evalNumbers equation.numbers ops == equation.testValue
 
 private def solvePart1 (equations : List Equation) : Int :=
-  equations.filter canEquationPossiblyBeTrue |>.sumBy (λ e => e.testValue)
+  equations.filter (canEquationPossiblyBeTrue [.add, .multiply]) |>.sumBy (·.testValue)
 
 def parseAndSolvePart1 (s : String): Except String Int := parseEquations s |>.map solvePart1
 
 #guard parseAndSolvePart1 exampleInput == Except.ok 3749
 
 -- Part 2
 
-private def solvePart2 (equations : List Equation) : Int := sorry
+private def solvePart2 (equations : List Equation) : Int :=
+  equations.filter (canEquationPossiblyBeTrue [.add, .multiply, .concatenation]) |>.sumBy (·.testValue)
 
 def parseAndSolvePart2 (s : String): Except String Int := parseEquations s |>.map solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == Except.ok -1
+#guard parseAndSolvePart2 exampleInput == Except.ok 11387

Aoc2024/Day07/Types.lean

@@ -6,6 +6,5 @@ deriving Repr, BEq, Hashable, Inhabited
 inductive Operator where
   | add
   | multiply
+  | concatenation
 deriving Repr, BEq, Hashable, Inhabited
-
-def Operator.all : List Operator := [Operator.add, Operator.multiply]