diff options
| -rw-r--r-- | Common/List.lean | 42 | ||||
| -rw-r--r-- | Day16.lean | 33 | ||||
| -rw-r--r-- | Main.lean | 1 |
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 @@ -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 @@ -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 |