day 7 part 1

Author: mdr

Aoc2024/Day07/Examples.lean

@@ -0,0 +1,10 @@
+def exampleInput :=
+"190: 10 19
+3267: 81 40 27
+83: 17 5
+156: 15 6
+7290: 6 8 6 15
+161011: 16 10 13
+192: 17 8 14
+21037: 9 7 18 13
+292: 11 6 16 20"

Aoc2024/Day07/Main.lean

@@ -0,0 +1,19 @@
+import Aoc2024.Day07.Solve
+import Aoc2024.CustomMonadLift
+
+def main : IO Unit := do
+  IO.println "Day 07"
+  IO.println ""
+  IO.println "Part 1"
+  let exampleInput <- IO.FS.readFile "Aoc2024/Day07/inputs/example.txt"
+  let puzzleInput <- IO.FS.readFile "Aoc2024/Day07/inputs/input.txt"
+  IO.println s!"Example: {<- parseAndSolvePart1 exampleInput}"
+  let answerPart1 <- parseAndSolvePart1 puzzleInput
+  IO.println s!"Puzzle: {answerPart1}"
+  assert! (answerPart1 == 66343330034722)
+  IO.println ""
+  IO.println "Part 2"
+  IO.println s!"Example: {<- parseAndSolvePart2 exampleInput}"
+  let answerPart2 <- parseAndSolvePart2 puzzleInput
+  IO.println s!"Puzzle: {answerPart2}"
+  assert! (answerPart2 == -1)

Aoc2024/Day07/Parser.lean

@@ -0,0 +1,23 @@
+import Aoc2024.Day07.Examples
+import Aoc2024.Day07.Types
+import Aoc2024.Utils
+import Std
+open Std.Internal.Parsec.String
+open Std.Internal.Parsec
+
+private def number : Parser Int := do pure (<- digits)
+
+private def equation : Parser Equation := do
+  let testValue <- number
+  let _ ← skipString ": "
+  let numbers <- sepBy number (skipChar ' ')
+  pure { testValue, numbers }
+
+private def equations : Parser (List Equation) := sepBy equation (skipChar '\n')
+
+def parseEquations : String -> Except String (List Equation) := equations.run
+
+#guard parseEquations "190: 10 19\n3267: 81 40 27" == Except.ok [
+  { testValue := 190, numbers := [10, 19] },
+  { testValue := 3267, numbers := [81, 40, 27] }
+]

Aoc2024/Day07/Solve.lean

@@ -0,0 +1,45 @@
+import Aoc2024.Utils
+import Aoc2024.Day07.Examples
+import Aoc2024.Day07.Parser
+import Aoc2024.Day07.Types
+
+-- Part 1
+
+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
+      ) h
+
+#guard evalNumbers [11, 6, 16, 20] [.add, .multiply, .add] == 292
+
+private def replicateM (n : Nat) (options : List α) : List (List α) :=
+  let rec loop (n : Nat) (acc : List (List α)) : List (List α) :=
+    match n with
+    | 0 => acc
+    | n + 1 => loop n (acc.bind λ l => options.map (λ o => o :: l))
+  loop n [[]]
+#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]
+  operators.any λ ops => evalNumbers equation.numbers ops == equation.testValue
+
+private def solvePart1 (equations : List Equation) : Int :=
+  equations.filter canEquationPossiblyBeTrue |>.sumBy (λ e => e.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
+
+def parseAndSolvePart2 (s : String): Except String Int := parseEquations s |>.map solvePart2
+
+-- #guard parseAndSolvePart2 exampleInput == Except.ok -1

Aoc2024/Day07/Types.lean

@@ -0,0 +1,11 @@
+structure Equation where
+  testValue : Int
+  numbers : List Int
+deriving Repr, BEq, Hashable, Inhabited
+
+inductive Operator where
+  | add
+  | multiply
+deriving Repr, BEq, Hashable, Inhabited
+
+def Operator.all : List Operator := [Operator.add, Operator.multiply]

Aoc2024/Day07/inputs/example.txt

@@ -0,0 +1,9 @@
+190: 10 19
+3267: 81 40 27
+83: 17 5
+156: 15 6
+7290: 6 8 6 15
+161011: 16 10 13
+192: 17 8 14
+21037: 9 7 18 13
+292: 11 6 16 20