From 3a125fab0a8e6a92ae55e534d4ea446ad01815e5 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 15 Dec 2024 21:39:35 +0100 Subject: Day 16, part 1 --- Day16.lean | 195 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--- Main.lean | 2 + 2 files changed, 190 insertions(+), 7 deletions(-) diff --git a/Day16.lean b/Day16.lean index 28e398f..1dd5ff8 100644 --- a/Day16.lean +++ b/Day16.lean @@ -83,26 +83,26 @@ private def OpticsElement.outputDirections : OpticsElement → EnterDirection | OpticsElement.Splitter SplitterDirection.Vertical, EnterDirection.FromBottom => [ExitDirection.ToTop] | OpticsElement.Splitter SplitterDirection.Vertical, EnterDirection.FromRight => [ExitDirection.ToTop, ExitDirection.ToBottom] -private def OpticsTable.neighbour? {table : OpticsTable} (outDirection : ExitDirection) (coordinate : table.Coordinate) : Option table.Coordinate := +private def OpticsTable.neighbour? {table : OpticsTable} (outDirection : ExitDirection) (coordinate : table.Coordinate) : Option (EnterDirection × table.Coordinate) := match outDirection with | ExitDirection.ToBottom => if h : coordinate.y.succ < table.height then - some {coordinate with y := ⟨coordinate.y.succ, h⟩} + some (EnterDirection.FromTop, {coordinate with y := ⟨coordinate.y.succ, h⟩}) else none | ExitDirection.ToLeft => if 0 < coordinate.x.val then - some {coordinate with x := ⟨coordinate.x.val.pred,Nat.lt_of_le_of_lt (Nat.pred_le _) coordinate.x.isLt⟩} + some (EnterDirection.FromRight,{coordinate with x := ⟨coordinate.x.val.pred,Nat.lt_of_le_of_lt (Nat.pred_le _) coordinate.x.isLt⟩}) else none | ExitDirection.ToTop => if 0 < coordinate.y.val then - some {coordinate with y := ⟨coordinate.y.val.pred, Nat.lt_of_le_of_lt (Nat.pred_le _) coordinate.y.isLt⟩} + some (EnterDirection.FromBottom, {coordinate with y := ⟨coordinate.y.val.pred, Nat.lt_of_le_of_lt (Nat.pred_le _) coordinate.y.isLt⟩}) else none | ExitDirection.ToRight => if h : coordinate.x.succ < table.width then - some {coordinate with x := ⟨coordinate.x.succ, h⟩} + some (EnterDirection.FromLeft, {coordinate with x := ⟨coordinate.x.succ, h⟩}) else none @@ -118,16 +118,83 @@ private def SeenExitDirection.setRight : SeenExitDirection → SeenExitDirection private def SeenExitDirection.setBottom : SeenExitDirection → SeenExitDirection := BitVec.setBitTrue 2 private def SeenExitDirection.setLeft : SeenExitDirection → SeenExitDirection := BitVec.setBitTrue 3 +private def SeenExitDirection.contains (d : SeenExitDirection) : ExitDirection → Bool +| ExitDirection.ToTop => d.top +| ExitDirection.ToRight => d.right +| ExitDirection.ToBottom => d.bottom +| ExitDirection.ToLeft => d.left + +private def SeenExitDirection.setDirection (d : SeenExitDirection) : ExitDirection → SeenExitDirection +| ExitDirection.ToTop => d.setTop +| ExitDirection.ToRight => d.setRight +| ExitDirection.ToBottom => d.setBottom +| ExitDirection.ToLeft => d.setLeft + +instance : ToString SeenExitDirection where + toString := λc ↦ + match h : c with + | 0b0000#4 => "." + | 0b0001#4 => "↑" + | 0b0010#4 => "→" + | 0b0011#4 => "└" + | 0b0100#4 => "↓" + | 0b0101#4 => "↕" + | 0b0110#4 => "┌" + | 0b0111#4 => "├" + | 0b1000#4 => "←" + | 0b1001#4 => "┘" + | 0b1010#4 => "↔" + | 0b1011#4 => "┴" + | 0b1100#4 => "┐" + | 0b1101#4 => "┤" + | 0b1110#4 => "┬" + | 0b1111#4 => "┼" + | ⟨x+16,_⟩ => + -- above Fin 15 exhaustive matches are not auto-detected, see https://github.com/leanprover/lean4/issues/5181 and Contradiction.Config.searchFuel + False.elim (absurd c.isLt (Nat.not_lt_of_ge $ h.substr $ Nat.le_add_left 16 x)) + private def SeenExitDirection.countDirection (a : SeenExitDirection) : Fin 5 := ⟨ a.top.toNat + a.right.toNat + a.bottom.toNat + a.left.toNat, Nat.lt_succ_of_le $ Nat.add_le_add (Nat.add_le_add (Nat.add_le_add (Bool.toNat_le _) (Bool.toNat_le _)) (Bool.toNat_le _)) (Bool.toNat_le _) ⟩ +private def SeenExitDirection.isEnergized : SeenExitDirection → Bool +| 0b0000#4 => false +| _ => true + +private theorem SeenExitDirection.setDirection_increasesCountDirection (a : SeenExitDirection) (e : ExitDirection) (h₁ : a.contains e = false) : a.countDirection < (a.setDirection e).countDirection := by + have Fin.val_three : ∀(n : Nat), (3 : Fin (n + 4)).val = 3 := λx↦rfl + cases e + all_goals + unfold contains at h₁ + simp[countDirection, setDirection, setTop, setLeft, setRight, setBottom, left, right, bottom, top] at h₁ ⊢ + simp[h₁, BitVec.setBitTrue, Fin.val_three] + unfold getElem BitVec.instGetElemNatBoolLt BitVec.getLsb' Nat.testBit + simp + private structure SeenExitDirections (table : OpticsTable) extends Parsing.RectangularGrid SeenExitDirection where sameWidth : width = table.width sameHeight : height = table.height +instance {table : OpticsTable} : ToString (SeenExitDirections table) where + toString := λes ↦ Id.run do + let mut result := "" + for hl: line in [:es.height] do + for hc: column in [:es.width] do + result := result.append $ ToString.toString (es.toRectangularGrid[{x := ⟨column, hc.upper⟩, y := ⟨line, hl.upper⟩ : es.Coordinate}]) + result := result.append "\n" + result + +instance {table : OpticsTable} : Repr (SeenExitDirections table) where + reprPrec t _ := ToString.toString t + +private def SeenExitDirections.set {table : OpticsTable} {d : SeenExitDirections table} (c : d.Coordinate) (v : SeenExitDirection) : SeenExitDirections table := + { + d with + toRectangularGrid := d.toRectangularGrid.set c v + } + private def SeenExitDirections.empty (table : OpticsTable) : SeenExitDirections table := { width := table.width @@ -171,17 +238,122 @@ private def SeenExitDirections.countExitDirections {table : OpticsTable} (seenDi rw[seenDirections.sameHeight, seenDirections.sameWidth] Fin.cast h₂.symm ⟨c,Nat.lt_succ_of_le h₁⟩ +/-- Factored out to work around that annoying "generalize failed, result is not type correct" errror -/ +private theorem SeenExitDirections.countExitDirections_increasesWhenSet_Aux (l : List SeenExitDirection) (i : Nat) (h₁ : i < l.length) (direction : ExitDirection) (h₂ : l[i].contains direction = false) (prev: Nat) : List.foldl (fun n e => n + e.countDirection.val) prev l < List.foldl (fun n e => n + e.countDirection.val) prev (l.set i (l[i].setDirection direction)) := by + cases i + case zero => + unfold List.set + split; case h_2 | h_3 => contradiction + case h_1 r1 r2 r3 d ds r4 => + clear r1 r2 r3 r4 + simp at h₂ ⊢ + simp only [←List.foldl_map] + rewrite[Nat.add_comm] + rewrite(config:={occs := .pos [2]})[Nat.add_comm] + simp[List.foldl_assoc] + -- f-ing finally + exact SeenExitDirection.setDirection_increasesCountDirection _ _ h₂ + case succ j => + match l with + | a :: as => + simp at h₁ h₂ ⊢ + apply countExitDirections_increasesWhenSet_Aux + assumption + +private theorem SeenExitDirections.countExitDirections_increasesWhenSet {table : OpticsTable} (seenDirections : SeenExitDirections table) (index : seenDirections.Coordinate) (direction : ExitDirection) (h₁ : seenDirections.toRectangularGrid[index].contains direction = false) : (seenDirections.countExitDirections) < (seenDirections.set index $ seenDirections.toRectangularGrid[index].setDirection direction).countExitDirections := by + unfold countExitDirections SeenExitDirections.set Parsing.RectangularGrid.set getElem Parsing.instGetElemRectangularGridCoordinateEq Parsing.RectangularGrid.Get + unfold getElem Parsing.instGetElemRectangularGridCoordinateEq Parsing.RectangularGrid.Get at h₁ + simp at h₁ ⊢ + unfold Parsing.RectangularGrid.Coordinate.toIndex at h₁ ⊢ + unfold Array.set + simp[Array.foldl_eq_foldl_toList] at h₁ ⊢ + rw[Array.getElem_eq_getElem_toList] at h₁ ⊢ + apply countExitDirections_increasesWhenSet_Aux + assumption + +private def OpticsTable.findFirstExitDirectionNotSeenInQueue {table : OpticsTable} (seenDirections : SeenExitDirections table) (beams : List (EnterDirection × table.Coordinate)) : Option (table.Coordinate × ExitDirection × List (EnterDirection × table.Coordinate)) := + match beams with + | [] => none + | b :: bs => + let opticsElement := table[b.snd] + let outputDirections := opticsElement.outputDirections b.fst + let sdCoordinate : seenDirections.Coordinate := { + x := Fin.cast seenDirections.sameWidth.symm b.snd.x + y := Fin.cast seenDirections.sameHeight.symm b.snd.y + } + let seenExitDirections := seenDirections.toRectangularGrid[sdCoordinate] + let notSeenOutputDirections := outputDirections.filter λd ↦ not $ seenExitDirections.contains d + match notSeenOutputDirections with + | [] => findFirstExitDirectionNotSeenInQueue seenDirections bs + | a :: [] => some (b.snd, a, bs) + | a :: _ => some (b.snd, a, b :: bs) + +private theorem OpticsTable.findFirstExitDirectionNotSeenInQueue_notContains {table : OpticsTable} (seenDirections : SeenExitDirections table) (beams : List (EnterDirection × table.Coordinate)) {result : table.Coordinate × ExitDirection × List (EnterDirection × table.Coordinate)} (h₁ : OpticsTable.findFirstExitDirectionNotSeenInQueue seenDirections beams = some result) : seenDirections.toRectangularGrid[{x := Fin.cast seenDirections.sameWidth.symm result.fst.x, y := Fin.cast seenDirections.sameHeight.symm result.fst.y : seenDirections.Coordinate}].contains result.snd.fst = false := by + unfold findFirstExitDirectionNotSeenInQueue at h₁ + split at h₁ + case h_1 => contradiction + case h_2 del b bs => + clear del + simp at h₁ + split at h₁ + case h_1 => + exact findFirstExitDirectionNotSeenInQueue_notContains seenDirections bs h₁ + case' h_2 ed heq | h_3 ed eds _ heq => + have h₂ := Option.some.inj h₁ + subst result + generalize { x := Fin.cast _ b.snd.x, y := Fin.cast _ b.snd.y : seenDirections.Coordinate } = c at * + have h₂ : ed ∈ List.filter (fun d => !seenDirections.toRectangularGrid[c].contains d) (OpticsElement.outputDirections table[b.snd] b.fst) := by simp only [heq, List.mem_singleton, List.mem_cons, true_or] + exact (Bool.not_eq_true' _).mp (List.mem_filter.mp h₂).right + private def OpticsTable.followPath {table : OpticsTable} (seenDirections : SeenExitDirections table) (beams : List (EnterDirection × table.Coordinate)) : SeenExitDirections table := -- step 1: discard all beams from the beginning of the list -- that do not yield at least one not-yet-seen exit-direction. -- step 2a: if no beams are left, done. -- step 2: for the first beam that yields new exit directions, - -- add those exit directions at the end of the beams list and + -- add those exit directions at the start of the beams list and -- mark them as seen. -- step 3: recurse -- step 4: profit + match _h₁ : table.findFirstExitDirectionNotSeenInQueue seenDirections beams with + | none => seenDirections + | some (coordinate, exitDirection, remainingBeams) => + let sdCoordinate : seenDirections.Coordinate := { + x := Fin.cast seenDirections.sameWidth.symm coordinate.x + y := Fin.cast seenDirections.sameHeight.symm coordinate.y + } + let newSeenDirections := seenDirections.set sdCoordinate + (seenDirections.toRectangularGrid[sdCoordinate].setDirection exitDirection) + match table.neighbour? exitDirection coordinate with + | none => + -- no neighbour, but we still need to note down the exit direction as seen + OpticsTable.followPath newSeenDirections remainingBeams + | some cd => + OpticsTable.followPath newSeenDirections (cd :: remainingBeams) +termination_by 4 * table.width * table.height - seenDirections.countExitDirections +decreasing_by + all_goals + apply Nat.sub_lt_of_gt + case h₁ => + exact Nat.le_of_lt_succ $ Fin.isLt _ + case h₂ => + apply SeenExitDirections.countExitDirections_increasesWhenSet + exact OpticsTable.findFirstExitDirectionNotSeenInQueue_notContains seenDirections beams _h₁ + +private def SeenExitDirections.countEnergizedTiles {table : OpticsTable} (seenDirections : SeenExitDirections table) : Nat := + seenDirections.elements.foldl (λc ed ↦ c + ed.isEnergized.toNat) 0 + +def part1 (table : OpticsTable) : Nat := + let seenDirections := table.followPath (SeenExitDirections.empty table) [(EnterDirection.FromLeft, {x := ⟨0,table.not_empty.left⟩, y := ⟨0,table.not_empty.right⟩})] + seenDirections.countEnergizedTiles - sorry + +------------------------------------------------------------------------------------ +open DayPart +instance : Parse ⟨16, by simp⟩ (ι := OpticsTable) where + parse := (Except.mapError ToString.toString) ∘ parse + +instance : Part ⟨16,_⟩ Parts.One (ι := OpticsTable) (ρ := Nat) where + run := λc ↦ some (part1 c) ------------------------------------------------------------------------------------ @@ -198,3 +370,12 @@ private def testInput := r".|...\.... ..//.|...." #eval parse testInput + +#eval match parse testInput with +| Except.error e => s!"Error: {e}".toFormat +| Except.ok ot => + Repr.reprPrec (ot.followPath (SeenExitDirections.empty ot) [(EnterDirection.FromLeft, {x := ⟨0,ot.not_empty.left⟩, y := ⟨0,ot.not_empty.right⟩})]) 0 + +#eval match parse testInput with +| Except.error e => s!"Error: {e}" +| Except.ok ot => ToString.toString $ part1 ot diff --git a/Main.lean b/Main.lean index 0dab65a..29e7314 100644 --- a/Main.lean +++ b/Main.lean @@ -14,6 +14,7 @@ import «Day12» import «Day13» import «Day14» import «Day15» +import «Day16» open DayPart @@ -56,6 +57,7 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String := | ⟨14,_⟩, Parts.Two => try_run_day_part_impl ⟨14,_⟩ Parts.Two data | ⟨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 | _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet." def main (parameters : List String): IO Unit := do -- cgit v1.2.3