day 10

Aoc2024/Day09/Parser.lean

@@ -5,9 +5,7 @@ import Std
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec
 
-private def digitToNat (b : Char) : Nat := b.toNat - '0'.toNat
-
-private def diskMapParser : Parser (List Nat) := Array.toList <$> many (digitToNat <$> digit)
+private def diskMapParser : Parser (List Nat) := Array.toList <$> many (charDigitToNat <$> digit)
 
 def parseDiskMap : String -> Except String (List Nat) := diskMapParser.run
 

Aoc2024/Day10/Examples.lean

@@ -1,2 +1,9 @@
 def exampleInput :=
-"..."
+"89010123
+78121874
+87430965
+96549874
+45678903
+32019012
+01329801
+10456732"

Aoc2024/Day10/Main.lean

@@ -7,13 +7,13 @@ def main : IO Unit := do
   IO.println "Part 1"
   let exampleInput <- IO.FS.readFile "Aoc2024/Day10/inputs/example.txt"
   let puzzleInput <- IO.FS.readFile "Aoc2024/Day10/inputs/input.txt"
-  IO.println s!"Example: {<- parseAndSolvePart1 exampleInput}"
-  let answerPart1 <- parseAndSolvePart1 puzzleInput
+  IO.println s!"Example: {parseAndSolvePart1 exampleInput}"
+  let answerPart1 := parseAndSolvePart1 puzzleInput
   IO.println s!"Puzzle: {answerPart1}"
-  assert! (answerPart1 == -1)
+  assert! (answerPart1 == 461)
   IO.println ""
   IO.println "Part 2"
-  IO.println s!"Example: {<- parseAndSolvePart2 exampleInput}"
-  let answerPart2 <- parseAndSolvePart2 puzzleInput
+  IO.println s!"Example: {parseAndSolvePart2 exampleInput}"
+  let answerPart2 := parseAndSolvePart2 puzzleInput
   IO.println s!"Puzzle: {answerPart2}"
-  assert! (answerPart2 == -1)
+  assert! (answerPart2 == 875)

Aoc2024/Day10/Parser.lean

@@ -2,11 +2,19 @@ import Aoc2024.Day10.Examples
 import Aoc2024.Day10.Types
 import Aoc2024.Utils
 import Std
-open Std.Internal.Parsec.String
-open Std.Internal.Parsec
+open Std (HashMap)
 
-private def inputParser : Parser (List Int) := sorry
+private def decorateWithCoordinates (s: String): List (Point × Char) := do
+  let (y, line) <- s.splitOn "\n" |> .enum
+  let (x, c) <- line.toList.enum
+  pure ⟨⟨x, y⟩, c⟩
 
-def parseInput : String -> Except String (List Int) := inputParser.run
-
--- #guard parseInput exampleInput == Except.ok 42
+def parseHeightMap (s : String): PuzzleInput :=
+  let decoratedChars := decorateWithCoordinates s
+  let (xs, ys) := decoratedChars.map (·.1.toPair) |>.unzip
+  let width := xs.max?.map (· + 1 |>.toNat) |>.getD 0
+  let height := ys.max?.map (· + 1 |>.toNat) |>.getD 0
+  let bounds: Rectangle := { topLeft := Point.origin, width, height }
+  let heights: HashMap Point Height :=
+    decoratedChars.foldl (init := HashMap.empty) λ m ⟨p, c⟩ => m.insert p (charDigitToNat c)
+  { bounds, heights }

Aoc2024/Day10/Solve.lean

@@ -2,19 +2,51 @@ import Aoc2024.Utils
 import Aoc2024.Day10.Examples
 import Aoc2024.Day10.Parser
 import Aoc2024.Day10.Types
+open Std (HashSet HashMap)
 
 -- Part 1
 
-private def solvePart1 (input : List Int) : Int := sorry
+private def Point.orthogonalNeighbours (p : Point): List Point :=
+  let ⟨x, y⟩ := p
+  [⟨x, y - 1⟩, ⟨x + 1, y⟩, ⟨x, y + 1⟩, ⟨x - 1, y⟩]
+
+private def solvePart1 (input : PuzzleInput) : Int :=
+  let heights := input.heights
+  let trailheads := heights.invert.getD 0 []
+  let getNeighbours (p : Point) (height : Height): List Point :=
+    p.orthogonalNeighbours.filter (λ neighbour => heights.get? neighbour == some height)
+  let score (trailhead : Point): Int :=
+    let rec findReachablePeaks (p : Point) : Nat -> List Point
+      | 0 => [p]
+      | n + 1 =>
+        let targetHeight := 9 - n
+        let neighbours := getNeighbours p targetHeight
+        neighbours.flatMap (findReachablePeaks · n)
+    findReachablePeaks trailhead 9 |>.toSet.size
+  trailheads.sumBy score
+
+def parseAndSolvePart1 (s : String): Int := parseHeightMap s |> solvePart1
+
+#guard parseAndSolvePart1 exampleInput == 36
 
-def parseAndSolvePart1 (s : String): Except String Int := parseInput s |>.map solvePart1
+-- Part 2
 
--- #guard parseAndSolvePart1 exampleInput == Except.ok -1
+private def getNeighbours (heights : HashMap Point Height) (p : Point) (height : Height): List Point :=
+    p.orthogonalNeighbours.filter (λ neighbour => heights.get? neighbour == some height)
 
--- Part 2
+private partial def countPaths (heights : HashMap Point Height) (p : Point) (currentHeight : Height): Int :=
+  match currentHeight with
+  | 9 => 1
+  | _ =>
+    let nextHeight := currentHeight + 1
+    getNeighbours heights p nextHeight |>.sumBy (countPaths heights · nextHeight)
 
-private def solvePart2 (input : List Int) : Int := sorry
+private def solvePart2 (input : PuzzleInput) : Int :=
+  let heights := input.heights
+  let trailheads := heights.invert.getD 0 []
+  let score (trailhead : Point): Int := countPaths heights trailhead 0
+  trailheads.sumBy score
 
-def parseAndSolvePart2 (s : String): Except String Int := parseInput s |>.map solvePart2
+def parseAndSolvePart2 (s : String): Int := parseHeightMap s |> solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == Except.ok -1
+#guard parseAndSolvePart2 exampleInput == 81

Aoc2024/Day10/Types.lean

@@ -1 +1,10 @@
 import Aoc2024.Utils
+import Std
+open Std (HashMap)
+
+abbrev Height := Nat
+
+structure PuzzleInput where
+  bounds : Rectangle
+  heights : HashMap Point Height
+deriving Repr, Inhabited

Aoc2024/Day10/inputs/example.txt

@@ -0,0 +1,8 @@
+89010123
+78121874
+87430965
+96549874
+45678903
+32019012
+01329801
+10456732

Aoc2024/Day10/inputs/input.txt

@@ -0,0 +1,40 @@
+6541001098012789610347890107654656710323
+7832102127643898701256521218323465891410
+8996543034556789650987434309012534892565
+3887689678965876501874345892105621763676
+4305678563456903416765676756898760654980
+5214107852107812321254382347872108901221
+6543236943056921010341291078963457654338
+7896545987045430010980012569454968983549
+3217830656189899121676101430356879892678
+2106921043210778234585232321267898761432
+3478854430345665056798743410456901050501
+4569763521012552143895654501345012347670
+3654012678903443212104309690432167898981
+2783656987654874908765218781201254012567
+1092347897893965889034765670387063013498
+1001298756102456776121874989496122110901
+2310891043201307655430923876565434325892
+3456780103011218967649810189410145456743
+2561078212320989858236702107320236787654
+1232569343423874749145893678741199899873
+0343454358514565632098704569632087684562
+0456789969609034501347612189323456893001
+1499876878798123101256543079012548762110
+2387905462687678871212344568187659450223
+3456012301056549960305650127691098321054
+3456732102345832154454781034540107650169
+2369847898738981023763692321121256743278
+1078456654567670119832103400012349894361
+0012387763456543208041076510123412765010
+7650196892565454589107889623296503854321
+8943256781074303673236908774387654983432
+8912965890985210984365219985345015676541
+7607834187866789875434308776236723498650
+6506543045679012766923105698109894567743
+5410432134988703457810014567056210754892
+0322345028767845893456723459847349889701
+1201276719454936712679801210738256776545
+2450989805103221604589752345629145480230
+2347823456012120113298943238710076591121
+1056910147893012320107654109656789432012

Aoc2024/Utils.lean

@@ -169,10 +169,23 @@ namespace Std.HashSet
   def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=
     xs.all ys.contains
 
+  #guard [1, 3].toSet.isSubsetOf [1, 2, 3].toSet == true
+  #guard [1, 2, 3].toSet.isSubsetOf [1, 3].toSet == false
+
 end Std.HashSet
 
-#guard [1, 3].toSet.isSubsetOf [1, 2, 3].toSet == true
-#guard [1, 2, 3].toSet.isSubsetOf [1, 3].toSet == false
+namespace Std.HashMap
+
+  def foldl [BEq α] [Hashable α] (m : HashMap α β) (init : γ) (f : γ -> α -> β -> γ) : γ :=
+    m.toList.foldl (init := init) λ acc (k, v) => f acc k v
+
+  def invert [BEq β] [Hashable β] [BEq α] [Hashable α] (m : HashMap α β) : HashMap β (List α) :=
+    m.foldl (init := HashMap.empty) λ acc k v =>
+      match acc.get? v with
+      | some ks => acc.insert v (k :: ks)
+      | none => acc.insert v [k]
+
+end Std.HashMap
 
 namespace String
   def lines (s : String) : List String := s.splitOn "\n"
@@ -252,3 +265,5 @@ def Rectangle.allPoints (r : Rectangle) : List Point := do
   return { x := x, y := y }
 #guard Rectangle.allPoints { topLeft := Point.origin, width := 2, height := 2 } ==
   [{ x := 0, y := 0 }, { x := 0, y := 1 }, { x := 1, y := 0 }, { x := 1, y := 1 }]
+
+def charDigitToNat (c : Char) : Nat := c.toNat - '0'.toNat