Day 5

Author: mdr

Aoc2024/Day05/Examples.lean

@@ -1,2 +1,29 @@
 def exampleInput :=
-"..."
+"47|53
+97|13
+97|61
+97|47
+75|29
+61|13
+75|53
+29|13
+97|29
+53|29
+61|53
+97|53
+61|29
+47|13
+75|47
+97|75
+47|61
+75|61
+47|29
+75|13
+53|13
+
+75,47,61,53,29
+97,61,53,29,13
+75,29,13
+75,97,47,61,53
+61,13,29
+97,13,75,29,47"

Aoc2024/Day05/Main.lean

@@ -10,10 +10,10 @@ def main : IO Unit := do
   IO.println s!"Example: {<- parseAndSolvePart1 exampleInput}"
   let answerPart1 <- parseAndSolvePart1 puzzleInput
   IO.println s!"Puzzle: {answerPart1}"
-  assert! (answerPart1 == -1)
+  assert! (answerPart1 == 4569)
   IO.println ""
   IO.println "Part 2"
   IO.println s!"Example: {<- parseAndSolvePart2 exampleInput}"
   let answerPart2 <- parseAndSolvePart2 puzzleInput
   IO.println s!"Puzzle: {answerPart2}"
-  assert! (answerPart2 == -1)
+  assert! (answerPart2 == 6456)

Aoc2024/Day05/Parser.lean

@@ -5,8 +5,30 @@ import Std
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec
 
-private def inputParser : Parser (List Int) := sorry
+private def number : Parser Int := do
+  let nat <- digits
+  pure nat
 
-def parseThings : String -> Except String (List Int) := inputParser.run
+private def orderingRuleParser : Parser OrderingRule := do
+  let before ← number
+  skipChar '|'
+  let after ← number
+  pure { before, after }
 
--- #guard parseReports exampleInput == Except.ok 42
+private def updateParser : Parser Update := do
+  let pages <- sepBy number (skipChar ',')
+  pure { pages }
+
+private def inputParser : Parser PuzzleInput := do
+  let rules ← many (orderingRuleParser <* skipChar '\n')
+  skipChar '\n'
+  let updates ← sepBy updateParser (skipChar '\n')
+  pure { rules := rules.toList, updates }
+
+def parseInput : String -> Except String PuzzleInput := inputParser.run
+
+#guard parseInput "1|2\n\n1,2\n3,4" == Except.ok {
+  rules := [{ before := 1, after := 2 }],
+  updates := [{ pages := [1, 2] }, { pages := [3, 4] }]
+}
+#guard parseInput exampleInput |>.isOk

Aoc2024/Day05/Solve.lean

@@ -1,15 +1,38 @@
 import Aoc2024.Utils
 import Aoc2024.Day05.Examples
 import Aoc2024.Day05.Parser
+open Std (HashSet)
 
-private def solvePart1 (things : List Int) : Int := sorry
+-- Part 1
 
-def parseAndSolvePart1 (s : String): Except String Int := parseThings s |>.map solvePart1
+private def middleElement {α} (l : List α) : Option α := l.get? (l.length / 2)
 
--- #guard parseAndSolvePart1 exampleInput == Except.ok 2
+private def middlePageNumber (update : Update) : Int := middleElement update.pages |>.getD 0
 
-private def solvePart2 (things : List Int) : Int := sorry
+private def isCorrectlyOrdered (rules : List OrderingRule) (update : Update) : Bool :=
+  let allowedPairs := rules.map (·.toPair) |>.toSet
+  update.pages.slidingPairs.toSet.isSubsetOf allowedPairs
 
-def parseAndSolvePart2 (s : String): Except String Int := parseThings s |>.map solvePart2
+private def solvePart1 (input : PuzzleInput) : Int :=
+  input.updates.filter (isCorrectlyOrdered input.rules)
+    |>.sumBy middlePageNumber
 
--- #guard parseAndSolvePart2 exampleInput == Except.ok 4
+def parseAndSolvePart1 (s : String): Except String Int := parseInput s |>.map solvePart1
+
+#guard parseAndSolvePart1 exampleInput == Except.ok 143
+
+-- Part 2
+
+private def orderCorrectly (rules : List OrderingRule) (update : Update) : Update :=
+  let allowedPairs := rules.map (·.toPair) |>.toSet
+  let reorderedPages := update.pages.mergeSort (λ p1 p2 => p1 == p2 || allowedPairs.contains (p1, p2))
+  { pages := reorderedPages }
+
+private def solvePart2 (input : PuzzleInput) : Int :=
+  input.updates.filterNot (isCorrectlyOrdered input.rules)
+    |>.map (orderCorrectly input.rules)
+    |>.sumBy middlePageNumber
+
+def parseAndSolvePart2 (s : String): Except String Int := parseInput s |>.map solvePart2
+
+#guard parseAndSolvePart2 exampleInput == Except.ok 123

Aoc2024/Day05/Types.lean

@@ -0,0 +1,18 @@
+abbrev Page := Int
+
+structure OrderingRule where
+  before : Page
+  after : Page
+deriving BEq, Hashable, Repr
+
+def OrderingRule.toPair (r : OrderingRule) : Page × Page :=
+  (r.before, r.after)
+
+structure Update where
+  pages : List Page
+deriving BEq, Hashable, Repr
+
+structure PuzzleInput where
+  rules : List OrderingRule
+  updates : List Update
+deriving BEq, Hashable, Repr

Aoc2024/Day05/inputs/example.txt

@@ -0,0 +1,28 @@
+47|53
+97|13
+97|61
+97|47
+75|29
+61|13
+75|53
+29|13
+97|29
+53|29
+61|53
+97|53
+61|29
+47|13
+75|47
+97|75
+47|61
+75|61
+47|29
+75|13
+53|13
+
+75,47,61,53,29
+97,61,53,29,13
+75,29,13
+75,97,47,61,53
+61,13,29
+97,13,75,29,47