Day 13, Part 1

5 files changed, 1555 insertions, 0 deletions

diff --git a/Common/Nat.lean b/Common/Nat.lean
index a863a49..3a605a9 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -15,3 +15,8 @@ theorem two_d_coordinate_to_index_lt_size {x y w h: Nat} (h₁ : x < w) (h₂ :
 theorem gt_of_sub_lt {a b c : Nat} (h₁ : a - b < a - c) : c < b := by omega
 
 theorem sub_lt_of_gt {a b c : Nat} (h₁ : b ≤ a) (h₂ : c < b) : a - b < a - c := by omega
+
+theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) :=
+  match b with
+  | 0 => h₁
+  | _ + 1 => /-(Nat.pred_succ a).substr $-/ Nat.lt_succ_of_lt h₁
diff --git a/Day13.lean b/Day13.lean
new file mode 100644
index 0000000..09c4403
--- /dev/null
+++ b/Day13.lean
@@ -0,0 +1,216 @@
+import «Common»
+
+namespace Day13
+
+------------------------------------------------------------------------------------
+
+inductive Tile
+| Sand : Tile
+| Rock : Tile
+deriving Repr, BEq
+
+instance : LawfulBEq Tile where
+  rfl := λ{a} ↦ by cases a <;> decide
+  eq_of_beq := by intros a b; cases a <;> cases b <;> simp <;> decide
+
+instance: ToString Tile where
+toString := λ
+| Tile.Sand => "."
+| Tile.Rock => "#"
+
+structure ParseCharError where
+  unexpectedCharacter : Char
+
+instance : ToString ParseCharError where
+toString := λc ↦ s!"Unexpected Character '{c.unexpectedCharacter}', expected '.' or '#'."
+
+private def Tile.ofChar? : Char → Except ParseCharError Tile
+| '.' => pure Tile.Sand
+| '#' => pure Tile.Rock
+| c => throw {unexpectedCharacter := c}
+
+abbrev ParsedInput := List $ Parsing.RectangularGrid Tile
+
+abbrev ParseInputError := Parsing.RectangularGrid.ParseError ParseCharError
+
+def parse (input : String) : Except ParseInputError ParsedInput :=
+  let blocks := input.toSubstring.splitOn "\n\n"
+  if blocks.isEmpty then
+    throw Parsing.RectangularGrid.ParseError.NoInput
+  else
+    blocks.mapM $ Parsing.RectangularGrid.ofSubstring Tile.ofChar?
+
+-- The things I do just to be able to #eval the parse result...
+theorem parse_not_empty_list {input : String} :
+match parse input with
+| Except.ok r => r.length > 0
+| Except.error _ => True := by
+  unfold parse
+  simp only
+  cases h₁ : (input.toSubstring.splitOn "\n\n").isEmpty
+  <;> simp only [Bool.false_eq_true, ↓reduceIte, gt_iff_lt]
+  rw[←List.mapM'_eq_mapM]
+  unfold List.mapM'
+  have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false.mp h₁
+  cases h₃ : input.toSubstring.splitOn "\n\n"
+  case false.nil => contradiction
+  case false.cons b bs =>
+    simp only [bind_pure_comp]
+    cases Parsing.RectangularGrid.ofSubstring Day13.Tile.ofChar? b
+    case error e => exact True.intro
+    case ok t =>
+      cases List.mapM' (Parsing.RectangularGrid.ofSubstring Day13.Tile.ofChar?) bs
+      case error e => exact True.intro
+      case ok ts =>
+        have h₄ := List.length_cons t ts
+        unfold bind Monad.toBind Except.instMonad
+        simp only [Except.bind, Except.map, h₄, Nat.zero_lt_succ]
+
+------------------------------------------------------------------------------------
+
+private abbrev Grid := Parsing.RectangularGrid Tile
+
+private inductive LookDirection (grid : Grid)
+| Horizontal
+| Vertical
+
+private def LookDirection.width : (LookDirection grid) → Nat
+| Horizontal => grid.width
+| Vertical => grid.height
+
+private def LookDirection.height : (LookDirection grid) → Nat
+| Horizontal => grid.height
+| Vertical => grid.width
+
+private structure LookDirection.Coordinate (lookDirection : LookDirection grid) where
+  x : Fin lookDirection.width
+  y : Fin lookDirection.height
+
+private def LookDirection.Coordinate.toGridCoordinate {grid : Grid} {lookDirection : LookDirection grid} (c : lookDirection.Coordinate) : grid.Coordinate :=
+  match lookDirection with
+  | Horizontal => {x := c.x, y := c.y}
+  | Vertical => {y := c.x, x := c.y}
+
+private def LookDirection.get {grid : Grid} {lookDirection : LookDirection grid} (coordinate : LookDirection.Coordinate lookDirection) : Tile :=
+  grid[coordinate.toGridCoordinate]
+
+private def getCoordinateOffset {ld : LookDirection grid} (mirror : Fin (ld.width - 1)) (offset : Nat) : Option (Fin ld.width × Fin ld.width) :=
+  if h : offset <= mirror ∧ mirror + offset + 1 < ld.width then
+    some (
+      ⟨mirror - offset, Nat.lt_of_le_of_lt (Nat.sub_le mirror offset) (Nat.lt_of_pred_lt mirror.isLt)⟩,
+      ⟨mirror + offset + 1, h.right⟩)
+  else
+    none
+
+private theorem LookDirection.not_empty (lookDirection : LookDirection grid) : lookDirection.width > 0 ∧ lookDirection.height > 0 := by
+  unfold width height
+  cases lookDirection <;> simp only[grid.not_empty, and_true]
+
+private def canBeMirror (lookDirection : LookDirection grid) (index : Fin (lookDirection.width - 1)) : Bool :=
+  areRowsMirrored ⟨lookDirection.height.pred, Nat.pred_lt $ Nat.ne_zero_iff_zero_lt.mpr lookDirection.not_empty.right⟩
+where
+  areRowsMirrored : Fin (lookDirection.height) → Bool := λ r ↦
+    let isCurrentRowMirrored := isRowMirrored r 0
+    match r with
+    | ⟨0,_⟩ => isCurrentRowMirrored
+    | ⟨rp + 1, h₁⟩ =>
+      isCurrentRowMirrored && areRowsMirrored ⟨rp, Nat.lt_of_succ_lt h₁⟩
+  isRowMirrored : Fin (lookDirection.height) → Nat → Bool := λr o ↦
+    match h : getCoordinateOffset index o with
+    | none => true --always consider outside as mirrored.
+    | some (i₁, i₂) =>
+      let c₁ : lookDirection.Coordinate := {x := i₁, y := r}
+      let c₂ : lookDirection.Coordinate := {x := i₂, y := r}
+      lookDirection.get c₁ == lookDirection.get c₂ && isRowMirrored r (o+1)
+    termination_by _ o => lookDirection.width - (index + o + 1)
+    decreasing_by
+      unfold getCoordinateOffset at h
+      split at h
+      case isFalse => contradiction
+      case isTrue h₁ => omega
+
+private def findMirrorPlanes (lookDirection : LookDirection grid) : List (Fin lookDirection.width.pred) :=
+  match h : lookDirection.width with
+  | 0 => absurd h $ Nat.ne_zero_iff_zero_lt.mpr lookDirection.not_empty.left
+  | 1 => []
+  | wp + 2 =>
+    have h : wp+2 = lookDirection.width := h.symm
+    have : wp < lookDirection.width.pred := Nat.pred_lt_pred (Nat.add_one_ne_zero _) $ Nat.add_one_le_iff.mp (Nat.le_of_eq h)
+    h▸(findMirrorPlanes_aux ⟨wp,this⟩ [])
+where
+  findMirrorPlanes_aux (r : Fin lookDirection.width.pred) (p : List (Fin lookDirection.width.pred)) : List (Fin lookDirection.width.pred) :=
+    let p := if canBeMirror lookDirection r then
+      r :: p
+    else
+      p
+    match r with
+    | ⟨0,_⟩ => p
+    | ⟨rp+1,isLt⟩ => findMirrorPlanes_aux ⟨rp, Nat.lt_of_succ_lt isLt⟩ p
+
+def part1 (input : ParsedInput) : Nat :=
+  let horizontalScores := input.foldl (λs g ↦
+    (findMirrorPlanes (LookDirection.Horizontal : LookDirection g)).foldl (·+·.val+1) s) 0
+  let verticalScores := input.foldl (λs g ↦
+    (findMirrorPlanes (LookDirection.Vertical : LookDirection g)).foldl (λa b ↦ a+(b.val+1)*100) s) 0
+  horizontalScores + verticalScores
+
+
+------------------------------------------------------------------------------------
+
+open DayPart
+instance : Parse ⟨13, by simp⟩ (ι := ParsedInput) where
+  parse := Except.mapError toString ∘ parse
+
+instance : Part ⟨13,_⟩ Parts.One (ι := ParsedInput) (ρ := Nat) where
+  run := some ∘ part1
+------------------------------------------------------------------------------------
+
+private def testInput := "#.##..##.
+..#.##.#.
+##......#
+##......#
+..#.##.#.
+..##..##.
+#.#.##.#.
+
+#...##..#
+#....#..#
+..##..###
+#####.##.
+#####.##.
+..##..###
+#....#..#"
+
+#eval parse testInput
+
+#eval match h : parse testInput with
+| Except.error _ => none
+| Except.ok l =>
+  have h₁ : 0 < l.length := by
+    have h₂ := parse_not_empty_list (input := testInput)
+    simp only[h] at h₂
+    exact h₂
+  let t := l[0]
+  let LD := (LookDirection t)
+  let ld : LD := LookDirection.Horizontal
+  let midx := 0
+  if h₂ : midx < ld.width - 1 then
+    ToString.toString <$> getCoordinateOffset (ld := ld) ⟨midx, h₂⟩ 1
+  else
+    none
+
+#eval match h : parse testInput with
+| Except.error _ => []
+| Except.ok l =>
+  have h₁ : 0 < l.length := by
+    have h₂ := parse_not_empty_list (input := testInput)
+    simp only[h] at h₂
+    exact h₂
+  let t := l[0]
+  let LD := (LookDirection t)
+  let ld : LD := LookDirection.Horizontal
+  ToString.toString <$> findMirrorPlanes ld
+
+#eval match parse testInput with
+| Except.error _ => 0
+| Except.ok l => part1 l
diff --git a/Main.lean b/Main.lean
index 17602fb..e7cc5da 100644
--- a/Main.lean
+++ b/Main.lean
@@ -11,6 +11,7 @@ import «Day9»
 import «Day10»
 import «Day11»
 import «Day12»
+import «Day13»
 
 open DayPart
 
@@ -47,6 +48,7 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String :=
   | ⟨11,_⟩, Parts.Two => try_run_day_part_impl ⟨11,_⟩ Parts.Two data
   | ⟨12,_⟩, Parts.One => try_run_day_part_impl ⟨12,_⟩ Parts.One data
   | ⟨12,_⟩, Parts.Two => try_run_day_part_impl ⟨12,_⟩ Parts.Two data
+  | ⟨13,_⟩, Parts.One => try_run_day_part_impl ⟨13,_⟩ Parts.One data
   | _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet."
 
 def main (parameters : List String): IO Unit := do
diff --git a/inputs/day13.input b/inputs/day13.input
new file mode 100644
index 0000000..0e5bc1d
--- /dev/null
+++ b/inputs/day13.input
@@ -0,0 +1,1331 @@
+..#####
+..#....
+..#####
+##...#.
+.#.....
+.####.#
+.####.#
+##.....
+##...#.
+..#####
+..#....
+..#####
+..#####
+
+....#..
+###....
+...#.##
+###....
+....##.
+##.#.##
+..##.##
+###.#..
+..#.###
+
+##...#####..#
+.###..#.##..#
+......#......
+##..###......
+..###.#...##.
+..#..####.##.
+....##...#..#
+..#.##..#####
+##...#.##....
+###..##..#..#
+###..#.##....
+
+##.........
+##.........
+.#.######..
+#.#...#.##.
+.##..##.###
+##...##....
+.#.##..####
+##.##.#.#.#
+.##.###..#.
+.#....#....
+#....#.#.##
+..##..#....
+..##..##...
+
+##.#..#..
+####.##..
+###.###.#
+...##.#.#
+...#####.
+..##.....
+###.#..#.
+..#.#.###
+####...##
+####...##
+..#.#.###
+###.#..#.
+..#......
+...#####.
+...##.#.#
+
+#...##...#.#...
+#...##...#.##..
+..##..##..####.
+##.####.##.#.##
+##..##..####.##
+.###..###...#.#
+.#..##..#.###.#
+
+###..#...
+.##.##.##
+#.#####..
+.#.#.##.#
+####...##
+#.#######
+#..####.#
+#..####.#
+#.#######
+####...##
+.#.#.##.#
+#.#####..
+.##.##.##
+###..#...
+###..#..#
+
+##....##...####
+#.####.#..###.#
+##.##.#######.#
+##.##.##.##...#
+#......#.....#.
+...##...#######
+#.#..#.###.#..#
+#.#..#.#...###.
+..#..#..#.#.#..
+.######.#.#..#.
+###..##########
+###..###..###.#
+..#..#...#.....
+..#..#...##....
+###..###..###.#
+
+.#.##.#.#
+##.#..#..
+..##.#...
+.##.#####
+##.##.###
+##.##.###
+.##.#####
+..##.#...
+##.#..#..
+.#.##.#.#
+...##.#.#
+
+##.....
+..####.
+..#.##.
+.#.####
+##.#..#
+.#.#..#
+..#####
+..#.##.
+.###..#
+.###..#
+..#.##.
+
+..##..####..#
+#######..####
+######....###
+#.##.##..##.#
+.####.####.##
+.####..##..##
+#.##.#....#.#
+##..##....##.
+#....######.#
+.#..#..##..#.
+..##..####..#
+.####.####.##
+#....#....#..
+#.##.##..##.#
+#....#....#..
+##..########.
+#######..####
+
+#..###...####
+....#.#..####
+####.#.#..##.
+#..##.#..#..#
+#..####...##.
+.....#...#..#
+######.###..#
+#..###.##....
+###..#.#.#..#
+
+..#...######.
+..##..#.##.#.
+.#.#..######.
+#.#...#....#.
+#..##...##...
+#..##...##...
+#.##..#....#.
+.#.#..######.
+..##..#.##.#.
+..#...######.
+..###.##..##.
+..#.#.##..##.
+.#.#.##.##.##
+#..#..######.
+..##.#......#
+...###......#
+...#.###..###
+
+..#.##.#.###.#.#.
+..#.####.###.#.#.
+#####......##.##.
+###...#.#.#.....#
+####..##.#####.#.
+....#..#.#.#...##
+#######.......##.
+
+.####.#..#.
+.####.###.#
+..##......#
+#....####.#
+......#####
+.####..##..
+#....#.#...
+#....###...
+##..###.#.#
+#.##.#...#.
+#.##.#.#.#.
+#....###.#.
+##..###.###
+#.#..###.#.
+##..######.
+#....#.###.
+#....#.###.
+
+..#.##...
+.#.#..#.#
+#..#.#...
+##.#..#..
+###.###..
+#.###....
+.#...####
+.#...####
+#.###....
+###.###..
+##.#..#..
+
+.###....#....
+##..#..#..##.
+..###.###....
+..##.#..#####
+.##.#.#.#.##.
+.#...#.##.#..
+##.#...#.....
+.###..##.####
+.###..##.####
+
+.#....#...#####..
+.######...#......
+.######...#...#..
+.#....#...#####..
+.##..##..###..#.#
+#......##.....###
+#..##..#..#.##.##
+...##...#..####..
+##.##.###....#...
+##....######....#
+..####..#.##.###.
+
+.#..#.#..##..#.
+#.##.#........#
+.#..#...#..#...
+#.##.###...####
+#....##..##..##
+#.##.##.#..#.##
+......##....##.
+
+###.#..#.
+#####.#..
+####..#.#
+####..#.#
+#####.#..
+###.#..#.
+..##.##..
+####..##.
+..###....
+...##.###
+...###.##
+...#.##.#
+.#..#.###
+..#..####
+....###.#
+
+#.#....####
+#.#....####
+##....#.##.
+.#.#.#..##.
+.##..#..##.
+..#..#..##.
+#.#.######.
+.#.#.......
+..###..#..#
+.####.#.##.
+####.###..#
+#...#.#####
+#....#.....
+
+....###...#.##.
+....###.#.#.##.
+##...#..#...###
+######........#
+##....#.#.##..#
+..#.######...#.
+....#.#..####..
+######....###..
+##.#...#.###..#
+####..#.#...#.#
+##..#..#.#.####
+##.##.####.#..#
+###..#.#.#.....
+
+.....#..##.##..
+.##.###.#####..
+.##.###..##..##
+....##.##....#.
+.##.##.##.#.###
+....#.####.##.#
+#..#.######..#.
+#..#...###..#.#
+#..#...###..#.#
+#..#.######..#.
+....#..###.##.#
+.##.##.##.#.###
+....##.##....#.
+
+#..#.#..#.#..
+....##..##...
+####......###
+...#......#..
+...#......#..
+####......###
+....##..##...
+#..#.#..#.#..
+.#.#......#.#
+####..##..###
+..###.##.###.
+###.....#..##
+#..##.##.##..
+
+........#..#.
+.#.##.#.####.
+##....###..##
+.#....#......
+...##...#..#.
+#.####.######
+.####.#.####.
+..#..#..####.
+........#..#.
+
+.##..##...##...##
+.##..##..####..##
+########.####.###
+##.##.###.##.###.
+...##....#..#....
+########..##..###
+#......###..###..
+..#..#..#....#..#
+.######..####..##
+.#.##.#........#.
+###..###...#..###
+.#.##.#..####..#.
+##....##......##.
+
+#####...####.
+##.#.########
+.#......####.
+..##..##....#
+##.#..#.#..#.
+......##....#
+###...#......
+###...#......
+......##....#
+.#.#..#.#..#.
+..##..##....#
+.#......####.
+##.#.########
+
+#.#######..
+..####.####
+.....##....
+#.#..###.##
+#.#.##.#...
+##.##..#.##
+##.##..#.#.
+##.##..#.#.
+##.##..#.##
+#.#.##.#...
+#.#..###.##
+.....##....
+..####..###
+#.#######..
+#####.#.###
+.##.#.#...#
+.##.#.#...#
+
+.###.###.####.#
+......###.##.##
+###.##....#....
+....#..###..###
+#.#.#####....##
+.....#.#..##..#
+####.#.#......#
+#.####...#..#..
+#.####...#..#..
+####.#.#......#
+.....#.#..##..#
+
+...##..####..##
+...##..####..##
+###.#.#....#.#.
+..###..####..##
+..##.#.####.#.#
+##..#.#.##.#.#.
+.#...#..##..#..
+##..#..#..#..#.
+.###...#..#...#
+#...##.#..#.##.
+.##.##......##.
+.##.#.#.##.#.#.
+....##.#.##.##.
+...##.######.##
+.....#......#..
+
+#....#.##
+...######
+..###...#
+...##.#..
+.#.######
+.#.######
+...##.#..
+
+..##.#......#.##.
+##.....#..#.....#
+..###.##..##.###.
+##..###.##.###..#
+..####.#..#.####.
+..#..#..##..#..#.
+..#..##....##..#.
+#######....######
+#####.#####..####
+..###..####..###.
+##...###..###...#
+..#.##......##.#.
+##.###..##..###.#
+
+......#..#..#..#.
+.#..#.#........#.
+.####..###..###..
+#.##......##.....
+..##..##..##..##.
+#....##.######.##
+#.##.####.##.####
+#######..#..#..##
+######..#.##.#..#
+
+.####..##
+#..#.##.#
+#.##.##.#
+.####..##
+#..#....#
+.#.#....#
+..#.####.
+...#.##.#
+#.#.#..#.
+
+......#..#.#....#
+#....####..##..##
+######..###..##..
+#....#.#...######
+.####.#.##.......
+######...##.####.
+#.##.###.##.##.#.
+
+...#####..###
+..###..####..
+###.....##...
+.#..#...##...
+##.....#..#..
+#......#..#..
+.#.##..####..
+#...####..###
+.#####.####.#
+.....########
+#......#..#..
+........##...
+#.#####....##
+.##.#########
+#.###...##...
+
+#.#.....#....#...
+##..#.#..#..##.#.
+..#...##########.
+..##.#.#.#..#.#.#
+#####.#.######.#.
+#####.#.######.#.
+..##.#.#.#..#.#.#
+..#...##########.
+##..#.#..#..##.#.
+
+.#.###.###.##..##
+.#.####..#.######
+##..#####........
+.##.#.###..##..##
+###.#.####..#..##
+.#...#.##.##.##.#
+..#...#...##.##.#
+###...####..#..#.
+##.#####...##..##
+#..####..########
+..#.###..##.####.
+.##..#.#.##.#..#.
+.###.###.#.##..##
+.###.###.#.##..##
+.##..#.#.##.#..#.
+
+#..#.##.#..#.#.
+.#.#.##.#.#.#.#
+#..######..#..#
+##..####..##.##
+.#.#....#.#.#..
+.#.#....#.#.#..
+##..####..##.##
+#..######..#..#
+.#.#.##.#.#.#.#
+#..#.##.#..#.#.
+#..######..#.#.
+............##.
+.#.#....###.##.
+##........##..#
+.####..####..##
+##..####..##..#
+#...####...#...
+
+###.#..
+...#.##
+...#.##
+#####..
+###..#.
+####...
+###.#..
+###....
+###.###
+..#.#..
+....##.
+###.###
+..#.##.
+
+.#..#.#.##.####.#
+.#.....#.#......#
+...###..#..####..
+...###..#..####..
+.#.....#.#......#
+.#..#.#.##.####.#
+#.####...########
+.#.#.##..##.##.##
+.####..###..##..#
+#...#############
+#.#..#..####..###
+.#...##..#..##..#
+.####...#........
+..#.#..##..#..#..
+###...########.##
+.#.#.##.###....##
+..##.#.###.####.#
+
+...#.#.#...##...#
+.#.#.#..##.##.##.
+##.......#....#..
+..#.#.....####...
+..#.#.###..##..##
+###...#.########.
+..#.#....#....#..
+####.##.##....##.
+##.##.#....##....
+####.....######..
+...#..##.#.##.#.#
+..#..#..###..###.
+...###.....##....
+#####..##########
+...#.##.#.#..#.#.
+###.#...########.
+...##.#.###..###.
+
+#..##..#...
+####..#.###
+....###..#.
+####..#...#
+......##.##
+.##.##.#..#
+.##.##.#..#
+......##.##
+####.##...#
+....###..#.
+####..#.###
+
+..##.#....#.##.
+..###..##..###.
+##............#
+......####....#
+##....#..#....#
+..#.##....##.#.
+..#..##..##..#.
+###.#.#..#.#.##
+##............#
+
+....###...###.#
+.###.#.....##.#
+###.#.#....#..#
+##.......######
+#####...#.###.#
+##...#########.
+###.###.#.#....
+###.###.#.#....
+##...#########.
+#####...#.###.#
+##.......######
+
+####.##...#..
+.#.....##.#.#
+....#.#....#.
+..#..#..###..
+....####..###
+..####..##...
+..####..##...
+
+..##.######.##.
+######.##.#####
+##..#.####.#..#
+.#..##.##.##..#
+#.....####.....
+#..............
+#....##..##....
+.####......####
+..#..#.##.#..#.
+#.##........##.
+.....#....#....
+
+...####.....#
+####..####...
+#..#..#..#..#
+#..#..#..###.
+....##......#
+.##.##.##...#
+.##.##.##.#..
+....##....##.
+####..#####.#
+.##.##.##.#..
+#..#..#..###.
+
+.#..#..#.###.##
+....#...##...##
+#....##.#...###
+#.##.#...#.#.##
+#.##.#..#...###
+#.##.#.....####
+.#..#...#.#.###
+..##...##.###..
+#.##.##.#...#..
+#....###...##..
+.........####..
+#######.##.#.##
+##..###.#...#..
+
+#.#.###..##.#
+.....#.....##
+..#..#.....##
+#.#.###..##.#
+##########...
+#.#.###.###..
+.####..#####.
+#....#####...
+#....#####...
+.####..#####.
+#.#.###.###..
+##########...
+#.#.###..##.#
+
+.##..##
+#..###.
+.##...#
+####...
+.##..#.
+.##.#..
+####...
+#..#.#.
+.....#.
+....#..
+....#.#
+#..#...
+.##..#.
+.##..#.
+#..##..
+
+##.....#..#..
+..####......#
+###....####..
+##.#...#..#..
+##.####....##
+..####......#
+#######..#.##
+##....#....#.
+..#.####..###
+##.##.######.
+#####.#....#.
+
+.##...#
+.##.##.
+#..#.#.
+....##.
+####.##
+####.##
+#..####
+#..####
+####.##
+####.##
+....##.
+#..#...
+.##.##.
+.##...#
+....##.
+
+..##..###..##
+######..#..#.
+#.##.#..#..#.
+##..##.#.##.#
+#.##.###.##..
+.####..#.##.#
+##..##.#....#
+
+..........##.....
+.#..#.#.######.#.
+##..###.#....#.##
+#.##.#..........#
+######..######..#
+#....#....##....#
+##..###.##..#####
+#.##.###..##..###
+.####..#..##..#..
+.####...##..##...
+#######...##...##
+#....#.#.#..#.#.#
+.#..#.#..#..#..#.
+......#.######.#.
+.#..#..#..##..#..
+#.##.#.########.#
+.####..#.#..#.#..
+
+........#..##..
+#.#.....#######
+.#####.########
+...##......##..
+..#..#.#.######
+#..#.#.###.##.#
+.#.#.#...##..##
+........#..##..
+.##.#####......
+
+#####....########
+....#..##...##...
+##..#.##.........
+...###...###..###
+....##..##......#
+...#.#..#..#..#..
+...###..###....##
+...#.####.#....#.
+######.##........
+..#.##.#.#..##..#
+###....##..####..
+#.##.#####......#
+##.#####..#....#.
+
+...##..
+###..##
+###..##
+..#..##
+###..##
+#......
+###..##
+#......
+.#....#
+.#.##.#
+.#.##.#
+.#....#
+#......
+###..##
+#......
+
+#..#..#..#.
+..##...##..
+.####..##..
+.####..##..
+...#...##..
+#..#..#..#.
+....##....#
+..###..##..
+.##...#..#.
+.##.#......
+.##..#....#
+#....#....#
+.####.#..#.
+
+#......
+##...##
+##...##
+#.#....
+.######
+..###..
+.###...
+.######
+.######
+#####..
+.....##
+###.###
+###.###
+#..##..
+#..#.##
+...####
+.######
+
+#.###.##.
+##..#.##.
+##.##.#..
+.....##..
+####.#.##
+#....####
+#..#.####
+####.#.##
+.....##..
+##.##.#..
+##..#.##.
+#.###.##.
+#.###.##.
+
+...######...#.#
+..########....#
+####.##.####..#
+#.###..###.###.
+#.#.####.#.##..
+#..#.##.#..####
+.#.#....#.#..#.
+#..#.##.#..#.##
+.###.##.###.#..
+....#..#....###
+.#..####..#..#.
+.#..##.#..#.###
+#.##....##.##..
+#...####...##.#
+.#.######.#.##.
+.#.######.#.##.
+#...####...##.#
+
+...#.#...#..#..
+...#.#...#..#..
+##.#####..##.##
+##.....####..#.
+#....#.#.#.###.
+##.#.####...###
+#######.###.###
+...###.#..###.#
+..#.#.###..##.#
+..#.#.###..##.#
+...###.#..###.#
+#######.###.###
+##.#.###....###
+#....#.#.#.###.
+##.....####..#.
+##.#####..##.##
+...#.#...#..#..
+
+##..####...#.
+####..##.#..#
+##..##..##..#
+##.....#.##..
+###....##.##.
+..##....#..#.
+....##.####..
+##.##..#..#.#
+##.##.....#.#
+....##.####..
+..##....#..#.
+###....##.##.
+##.....#.##..
+##..##..##..#
+####..##.#..#
+##..####...#.
+##......##...
+
+.#.#.#.#...
+###.####...
+###.####..#
+###.####..#
+###.####...
+.#.#.#.#...
+..#..##.###
+.###.....##
+..####..#..
+...#..#####
+..#.#.##..#
+..##.....#.
+..##.....#.
+..#.#.##..#
+...#..#####
+..####..#..
+.###..#..##
+
+..#...#..#...#.
+###...####...##
+##.#...##...#.#
+##...######..##
+###...####...##
+..#.###..###.#.
+...#.#....#.#..
+##.###.##.###.#
+..#..........#.
+##.##......##.#
+.....#....#....
+####.##..##.###
+##..#.####.#..#
+
+...####
+..###..
+.#.#..#
+......#
+..#.#.#
+..#.#.#
+......#
+.#.#..#
+..###..
+...####
+#.####.
+#..###.
+...####
+..###..
+.#.#..#
+......#
+..#.#.#
+
+....###......#.
+....###.....##.
+##..##.##..##..
+#..####....##..
+##.#....######.
+..##.###.#.....
+.#####.#...#...
+##.#...#.#...#.
+..#..##.###....
+..#.#..#.#.#..#
+#####.###..#.#.
+#####.###..#.#.
+..#.#..#.#.#..#
+..#..##.###....
+##.#...#.#...#.
+.#####.#...#...
+..##.###.#.....
+
+..#.......##.
+##.#.#.......
+####.##......
+.###..##.....
+.#####.##.##.
+..###...#....
+.##..##...##.
+.##..##...##.
+..###...#....
+.###.#.##.##.
+.###..##.....
+####.##......
+##.#.#.......
+..#.......##.
+#####.#......
+.##.###...##.
+#.#.#.##.#..#
+
+.##.#####
+.##..##.#
+#..#...#.
+.##.....#
+#..#.#.##
+#..#.#.##
+.##..#..#
+
+#..#..###.#
+#..#..###.#
+..#..#.###.
+##...##....
+##.####..#.
+##.####..#.
+##...##....
+..#..#.###.
+...#..###.#
+
+###...##..###..
+..###.##.#.####
+...####.#....##
+...####.#....##
+..###.##.#.####
+###...##..###..
+##.##.##...##..
+#..##.###..##..
+.#...#..#.###..
+#.####..#.##.##
+#..###..#####.#
+
+##..##.
+##..##.
+..##...
+#.##.#.
+##...#.
+.####.#
+..##..#
+..##...
+#....##
+##..###
+#....#.
+
+.####..##.#.#....
+#.##.#..#########
+..##...#..#..####
+......#..##..#..#
+#....#.####......
+.####.#.##..#....
+......#.#.##....#
+##..##..###.##..#
+##..###.#.###....
+#######..#..#....
+.####......#.#..#
+
+#.###..#....#####
+#.##..#.##..#...#
+#.##.##.##..#...#
+#.###..#....#####
+#.###..#....#####
+#.##.##.##..#...#
+#.##..#.##..#...#
+#.###..#....#####
+##...###.#..##.#.
+#.#####..###...##
+###.##..#..#.....
+..........#.##.#.
+.####..##..####..
+#.###....####.###
+...###..##....##.
+
+#.##..#
+###..#.
+#..#..#
+.##.##.
+#.##..#
+#.##..#
+.##.##.
+
+...#.#.....
+###.#.#..#.
+##..#######
+##.#.######
+.##..#.##.#
+.##..#.##.#
+##.#.######
+
+....##......#
+##########.#.
+.##.##.##.#.#
+##########...
+.#..##..#.##.
+.##....##..#.
+....##....##.
+.##.##.##.#.#
+.##.##.##.##.
+#..#..#..#.##
+....##......#
+
+.##.#..#.###.##..
+..#..##..#.######
+.....#.#........#
+.....#.#........#
+..#..##..#.######
+.##.#..#.###.##..
+.###.##.##...#..#
+#.#.##.#.#.#.#.##
+#..##.#..###.####
+.......#.#.######
+.......#.#.######
+#..##.#..###.####
+#.#.##.#.#.#.#.##
+.######.##...#..#
+.##.#..#.###.##..
+
+#.#.####.#.#...##
+..#.#..#.#...#..#
+..#.#..#.#...#..#
+#.#.####.#.#...##
+..#..##..#..#..##
+#....##....##...#
+##..#..#..##..#..
+....####.....#.##
+#..........#...##
+##........##..###
+..######.#..####.
+.#.##..##.#...###
+.#.#....#.#...#.#
+
+###.##.#..#.#
+####.#......#
+###.#.#....#.
+##....#....#.
+##.##...##...
+###....####..
+..###..#..#..
+##.##........
+...########.#
+
+....##.
+###.##.
+###.##.
+....##.
+#.#..#.
+##.#..#
+#......
+....##.
+#...##.
+##.....
+#..####
+
+..##.#.#..#.#
+#####.#.##.#.
+...#.###..###
+#..#.###..###
+#####.#.##.#.
+..##.#.#..#.#
+##.....####..
+.##.#.#.##.#.
+#..##..####..
+.#..##..##..#
+#...#.##..##.
+
+#.#.###..##.#....
+.###..##...##.##.
+#.###...#.....###
+..##.#.#...##..#.
+..##.#.#...##..#.
+#.###...#.....###
+.###..##...##.##.
+#.#.###..##.#....
+.##..##.#..#.#..#
+##...#######.####
+.#...##.##..##..#
+.#..###.##..##..#
+##...#######.####
+.##..##.#..#.#..#
+#.#.###..##.#....
+.###..##...##.##.
+#.###...#.....###
+
+##..#.####.#.
+.#######.##..
+.#######.##..
+##..#.####.#.
+#####.##.####
+.##...#######
+##.##...##.##
+...##..##..#.
+...##..##..#.
+##.##...##.##
+.##....######
+
+.#.##.##...
+##.#.#....#
+.#.#.#....#
+.#.#.#....#
+##.#.#....#
+.#.##.##...
+#####..#.##
+..#.##...#.
+..#...##.#.
+..#...#.##.
+...####.###
+.#..###..#.
+..##..####.
+....##..#..
+.....##.#.#
+.....##.#.#
+....##.##..
+
+..#.#....##..
+..###....##..
+######.#....#
+......#.####.
+.#####...##..
+...#...#....#
+.####........
+
+...#...#..#..###.
+###....##.#.#..#.
+###....##.#.#..#.
+...#...#..#..###.
+...###.#.......##
+...#..######...##
+###....###..#..##
+##..#.#####.##.##
+##.#....#.#..#...
+..#..#######.####
+...#.#.##...##.##
+..#...#.#....#..#
+..#..#..#.#.#....
+#####...#..#.####
+#.#..##..##....##
+
+##..#..#..#
+.####.#...#
+.####.#...#
+##..#.....#
+..##....#..
+##.#.##.###
+.####.....#
+.####.....#
+##.#.##.###
+
+..#.#..#.#....#
+.####..####..##
+.#..####..#..#.
+##.#.##.#.####.
+.#.#.##.#.#.##.
+....#..#....###
+....#..#....###
+.#.#.##.#.#.##.
+##.#.##.#.#####
+
+.#.###...
+####.####
+.##...###
+....###..
+##...#.##
+#.##.####
+#...#..##
+.###.##..
+.###..#..
+
+.....#..####..#
+.##..##########
+.###.##########
+.....#..####..#
+#.#...###..###.
+.##...##.##.##.
+#..##..##..##..
+#..##..######..
+.####.#.#..#.#.
+#..###.##..##.#
+...#####.##.###
+.#.#..##....##.
+#.##.####..####
+#.#...#.####.#.
+#.##.....##....
+
+..#.##.#...##.#
+#.#....#.###.##
+..##..##...#.#.
+.#.#..#.#....##
+..#....#..##.##
+####..######.#.
+####..######.#.
+..#....#..##.##
+.#.#..#.#.....#
+
+....###..##..##
+.....#........#
+#.##.#.##..##.#
+.#.##....##....
+####.....##....
+#....####..####
+......###..###.
+......###..###.
+##...####..####
+
+.####..#.#.
+..##..#.#..
+.......#..#
+#.##.##.###
+#######.##.
+######..#..
+......#..##
+#.##.###..#
+.####..#.##
+######..##.
+#######.#..
+#######.#..
+######...#.
+.####..#.##
+#.##.###..#
+
+###.###..#.
+.##........
+#.#####....
+###.#..#.##
+##..##.###.
+##..##.##..
+###.#..#.##
+###.#..#.##
+##..##.##..
+##..##.###.
+###.#..#.##
+
+##....###..
+......#.#..
+..#..##.###
+....#.#####
+#..####..##
+.###.####..
+..#...#.###
+#.##...####
+####...####
+
+.##..#.#.########
+######..#.##...#.
+....######..#....
+###.###..##..#.##
+##.#..#..#.##..##
+.##.###.####.#..#
+.##.###.####.#..#
+##.#..#..#.##..##
+###.###..##..####
+....######..#....
+######..#.##...#.
+.##..#.#.########
+.##..#.#.########
+######..#.##...#.
+....######..#....
+
+.....##
+###.###
+###.###
+.....##
+.#.#...
+##..##.
+..#####
+######.
+##.#.#.
+....#..
+...#..#
+
+..#..#..##..#..#.
+.######.#.....##.
+###..###..##....#
+#.#..#.##.#...###
+#.#..#.##.#...###
+###..###..##....#
+.######.#.....##.
+..#..#..##..#..##
+.#....#.###.#####
+###..###.#..##..#
+#.####.##..##....
+###..#####.##...#
+..####.....#####.
+.#....#..#.#.##..
+.######.#..#.#.#.
diff --git a/lakefile.lean b/lakefile.lean
index 143532a..0790965 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,6 +15,7 @@ lean_lib «Day9» where
 lean_lib «Day10» where
 lean_lib «Day11» where
 lean_lib «Day12» where
+lean_lib «Day13» where
 
 lean_lib «Common» where