Day 16 Part 2

3 files changed, 76 insertions, 0 deletions

diff --git a/Common/List.lean b/Common/List.lean
index 1c029e7..704f8b2 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -70,3 +70,45 @@ def drop_while_length_le (list : List α) (f : α → Bool) : (list.dropWhile f)
     case h_1 a as _  _ =>
       have := drop_while_length_le as f
       exact Nat.le_trans this (Nat.le_succ as.length)
+
+def mapWithProof {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) : List β :=
+  worker list f []
+where
+  worker : (list : List α) → ((e : α) → (e ∈ list) → β) → List β → List β
+  | [], _, bs => bs.reverse
+  | a :: as, f, bs =>
+    let g : (e : α) → (e ∈ as) → β := λ e h ↦ f e (List.mem_cons_of_mem a h)
+    worker as g (f a (List.mem_cons_self _ _) :: bs)
+
+protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) (acc : List β) : list.length + acc.length = (List.mapWithProof.worker list f acc).length := by
+  induction list generalizing acc
+  case nil => unfold mapWithProof.worker; simp only [length_nil, Nat.zero_add, length_reverse]
+  case cons l ls hi =>
+    unfold mapWithProof.worker
+    have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc)
+    simp_arith[←hi]
+
+theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length :=
+  List.length_mapWithProof_Aux list f []
+
+theorem mapWithProof_nil {α : Type u} {β : Type v} {f : (e : α) → (e ∈ []) → β} : [].mapWithProof f = [] := rfl
+
+theorem mapWithProof_neNilIffNeNil {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list ≠ [] ↔ (list.mapWithProof f) ≠ [] :=
+  ⟨
+    λh₁ ↦ List.length_pos.mp $ length_mapWithProof.subst (List.length_pos.mpr h₁),
+    λh₁ ↦ List.length_pos.mp $ length_mapWithProof.substr (List.length_pos.mpr h₁)
+  ⟩
+
+theorem map_ne_nil {α : Type u} {β : Type v} {list : List α} {f : α → β} : list ≠ [] ↔ list.map f ≠ [] :=
+  ⟨
+    λh₁ ↦ λh₂ ↦ absurd (List.map_eq_nil_iff.mp h₂) h₁,
+    λh₁ ↦ λh₂ ↦ absurd (List.map_eq_nil_iff.mpr h₂) h₁,
+  ⟩
+
+def min [Min α] (l : List α) (_h : l ≠ []) : α :=
+  match l with
+  | a :: as => as.foldl Min.min a
+
+def max [Max α] (l : List α) (_h : l ≠ []) : α :=
+  match l with
+  | a :: as => as.foldl Max.max a
diff --git a/Day16.lean b/Day16.lean
index 1dd5ff8..d91f6ad 100644
--- a/Day16.lean
+++ b/Day16.lean
@@ -348,6 +348,32 @@ def part1 (table : OpticsTable) : Nat :=
 
 
 ------------------------------------------------------------------------------------
+
+def part2 (table : OpticsTable) : Nat :=
+  let run := curry $ SeenExitDirections.countEnergizedTiles ∘ table.followPath (SeenExitDirections.empty table) ∘ ([·])
+  let runFromTop := run EnterDirection.FromTop
+  let runFromLeft := run EnterDirection.FromLeft
+  let runFromBottom := run EnterDirection.FromBottom
+  let runFromRight := run EnterDirection.FromRight
+  -- this would be way easier with for-loops, but I want to use lists for fun. Also, check my List.mapWithProof function.
+  let topRow : List table.Coordinate := (List.range table.width).mapWithProof λcol hc ↦ {x := ⟨col,List.mem_range.mp hc⟩, y := ⟨0,table.not_empty.right⟩ : table.Coordinate}
+  let bottomRow : List table.Coordinate := (List.range table.width).mapWithProof λcol hc ↦ {x := ⟨col,List.mem_range.mp hc⟩, y := ⟨table.height.pred,Nat.pred_lt_of_lt table.not_empty.right⟩ : table.Coordinate}
+  let leftColumn : List table.Coordinate := (List.range table.height).mapWithProof λrow hr ↦ {x := ⟨0,table.not_empty.left⟩, y := ⟨row,List.mem_range.mp hr⟩ : table.Coordinate}
+  let rightColumn : List table.Coordinate := (List.range table.height).mapWithProof λrow hr ↦ {x := ⟨table.width.pred,Nat.pred_lt_of_lt table.not_empty.left⟩, y := ⟨row,List.mem_range.mp hr⟩ : table.Coordinate}
+  let topScores := runFromTop <$> topRow
+  let bottomScores := runFromBottom <$> bottomRow
+  let leftScores := runFromLeft <$> leftColumn
+  let rightScores := runFromRight <$> rightColumn
+  have h₁ := λ{c : Nat} (h₁ : c > 0) (f : (n : Nat) → (n ∈ List.range c) → table.Coordinate) (g : table.Coordinate → Nat) ↦ (List.map_ne_nil (f := g)).mp $ ((List.mapWithProof_neNilIffNeNil (f := f)).mp (List.range_ne_nil.mpr $ Nat.pos_iff_ne_zero.mp h₁))
+  [
+    topScores.max $ h₁ table.not_empty.left _ _,
+    bottomScores.max $ h₁ table.not_empty.left _ _,
+    leftScores.max $ h₁ table.not_empty.right _ _,
+    rightScores.max $ h₁ table.not_empty.right _ _
+  ].max (List.cons_ne_nil _ _)
+
+------------------------------------------------------------------------------------
+
 open DayPart
 instance : Parse ⟨16, by simp⟩ (ι := OpticsTable) where
   parse := (Except.mapError ToString.toString) ∘ parse
@@ -355,6 +381,9 @@ instance : Parse ⟨16, by simp⟩ (ι := OpticsTable) where
 instance : Part ⟨16,_⟩ Parts.One (ι := OpticsTable) (ρ := Nat) where
   run := λc ↦ some (part1 c)
 
+instance : Part ⟨16,_⟩ Parts.Two (ι := OpticsTable) (ρ := Nat) where
+  run := λc ↦ some (part2 c)
+
 ------------------------------------------------------------------------------------
 
 
@@ -379,3 +408,7 @@ private def testInput := r".|...\....
 #eval match parse testInput with
 | Except.error e => s!"Error: {e}"
 | Except.ok ot => ToString.toString $ part1 ot
+
+#eval match parse testInput with
+| Except.error e => s!"Error: {e}"
+| Except.ok ot => ToString.toString $ part2 ot
diff --git a/Main.lean b/Main.lean
index 29e7314..cea5348 100644
--- a/Main.lean
+++ b/Main.lean
@@ -58,6 +58,7 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String :=
   | ⟨15,_⟩, Parts.One => try_run_day_part_impl ⟨15,_⟩ Parts.One data
   | ⟨15,_⟩, Parts.Two => try_run_day_part_impl ⟨15,_⟩ Parts.Two data
   | ⟨16,_⟩, Parts.One => try_run_day_part_impl ⟨16,_⟩ Parts.One data
+  | ⟨16,_⟩, Parts.Two => try_run_day_part_impl ⟨16,_⟩ Parts.Two data
   | _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet."
 
 def main (parameters : List String): IO Unit := do