Begin Day16

7 files changed, 332 insertions, 0 deletions

diff --git a/Common.lean b/Common.lean
index db5d064..becafd3 100644
--- a/Common.lean
+++ b/Common.lean
@@ -9,3 +9,4 @@ import Common.NonEmptyList
 import Common.Parsing
 import Common.Nat
 import Common.Substring
+import Common.BitVec
diff --git a/Common/BitVec.lean b/Common/BitVec.lean
new file mode 100644
index 0000000..ad46efb
--- /dev/null
+++ b/Common/BitVec.lean
@@ -0,0 +1,11 @@
+def BitVec.setBitTrue {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n :=
+  a ||| BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])
+
+def BitVec.setBitFalse {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n :=
+  a &&& BitVec.not (BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]))
+
+def BitVec.setBit {n : Nat} (i : Fin n) (v : Bool) (a : BitVec n) : BitVec n :=
+  if v then
+    a.setBitTrue i
+  else
+    a.setBitFalse i
diff --git a/Common/Nat.lean b/Common/Nat.lean
index 9d0ee29..bc66a09 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -23,3 +23,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) :=
 
 theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) :=
   Nat.lt_of_le_of_lt (Nat.pred_le a) h₁
+
+theorem le_of_add_le {a b c d : Nat} (h₁ : a ≤ b + c) (h₂ : c ≤ d) : a ≤ b + d :=
+  Nat.le_trans h₁ (Nat.add_le_add_left h₂ b)
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index c811319..348db25 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -21,6 +21,12 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
   x : Fin grid.width
   y : Fin grid.height
 
+instance {grid : RectangularGrid Element} : BEq grid.Coordinate where
+  beq := λa b ↦ a.x == b.x && a.y == b.y
+
+instance {grid : RectangularGrid Element} : Hashable grid.Coordinate where
+  hash := λa ↦ Hashable.hash (a.x, a.y)
+
 instance : ToString (RectangularGrid.Coordinate grid) where
   toString := λx ↦ s!"x: {x.x}/{grid.width}, y : {x.y}/{grid.height}"
 
diff --git a/Day16.lean b/Day16.lean
new file mode 100644
index 0000000..28e398f
--- /dev/null
+++ b/Day16.lean
@@ -0,0 +1,200 @@
+import Common
+
+namespace Day16
+
+------------------------------------------------------------------------------------
+
+inductive MirrorDirection
+| BottomLeftTopRight
+| BottomRightTopLeft
+
+inductive SplitterDirection
+| Horizontal
+| Vertical
+
+inductive OpticsElement where
+| EmptySpace : OpticsElement
+| Mirror : MirrorDirection → OpticsElement
+| Splitter : SplitterDirection → OpticsElement
+
+inductive ParseCharError
+| InvalidCharacter : Char → ParseCharError
+
+instance : ToString ParseCharError where
+toString := λ
+| ParseCharError.InvalidCharacter c => s!"Cannot parse character {c}, expected '.', '/', '\\', '|', or '-'."
+
+instance : ToString OpticsElement where
+toString := λ
+| OpticsElement.EmptySpace => "."
+| OpticsElement.Mirror MirrorDirection.BottomLeftTopRight => "/"
+| OpticsElement.Mirror MirrorDirection.BottomRightTopLeft => "\\"
+| OpticsElement.Splitter SplitterDirection.Horizontal => "-"
+| OpticsElement.Splitter SplitterDirection.Vertical => "|"
+
+private def parseCharacter : Char → Except ParseCharError OpticsElement
+| '.' => Except.ok $ OpticsElement.EmptySpace
+| '/' => Except.ok $ OpticsElement.Mirror MirrorDirection.BottomLeftTopRight
+| '\\' => Except.ok $ OpticsElement.Mirror MirrorDirection.BottomRightTopLeft
+| '-' => Except.ok $ OpticsElement.Splitter SplitterDirection.Horizontal
+| '|' => Except.ok $ OpticsElement.Splitter SplitterDirection.Vertical
+| c => Except.error $ ParseCharError.InvalidCharacter c
+
+private abbrev OpticsTable := Parsing.RectangularGrid OpticsElement
+
+open Parsing in
+def parse : (input : String) → Except (RectangularGrid.ParseError ParseCharError) OpticsTable :=
+  RectangularGrid.ofString parseCharacter
+
+
+------------------------------------------------------------------------------------
+
+private inductive EnterDirection
+| FromTop
+| FromLeft
+| FromRight
+| FromBottom
+
+private inductive ExitDirection
+| ToTop
+| ToLeft
+| ToRight
+| ToBottom
+
+private def OpticsElement.outputDirections : OpticsElement → EnterDirection → List ExitDirection
+| OpticsElement.EmptySpace, EnterDirection.FromTop => [ExitDirection.ToBottom]
+| OpticsElement.EmptySpace, EnterDirection.FromLeft => [ExitDirection.ToRight]
+| OpticsElement.EmptySpace, EnterDirection.FromBottom => [ExitDirection.ToTop]
+| OpticsElement.EmptySpace, EnterDirection.FromRight => [ExitDirection.ToLeft]
+| OpticsElement.Mirror MirrorDirection.BottomLeftTopRight, EnterDirection.FromTop => [ExitDirection.ToLeft]
+| OpticsElement.Mirror MirrorDirection.BottomLeftTopRight, EnterDirection.FromLeft => [ExitDirection.ToTop]
+| OpticsElement.Mirror MirrorDirection.BottomLeftTopRight, EnterDirection.FromBottom => [ExitDirection.ToRight]
+| OpticsElement.Mirror MirrorDirection.BottomLeftTopRight, EnterDirection.FromRight => [ExitDirection.ToBottom]
+| OpticsElement.Mirror MirrorDirection.BottomRightTopLeft, EnterDirection.FromTop => [ExitDirection.ToRight]
+| OpticsElement.Mirror MirrorDirection.BottomRightTopLeft, EnterDirection.FromLeft => [ExitDirection.ToBottom]
+| OpticsElement.Mirror MirrorDirection.BottomRightTopLeft, EnterDirection.FromBottom => [ExitDirection.ToLeft]
+| OpticsElement.Mirror MirrorDirection.BottomRightTopLeft, EnterDirection.FromRight => [ExitDirection.ToTop]
+| OpticsElement.Splitter SplitterDirection.Horizontal, EnterDirection.FromTop => [ExitDirection.ToLeft, ExitDirection.ToRight]
+| OpticsElement.Splitter SplitterDirection.Horizontal, EnterDirection.FromLeft => [ExitDirection.ToRight]
+| OpticsElement.Splitter SplitterDirection.Horizontal, EnterDirection.FromBottom => [ExitDirection.ToLeft, ExitDirection.ToRight]
+| OpticsElement.Splitter SplitterDirection.Horizontal, EnterDirection.FromRight => [ExitDirection.ToLeft]
+| OpticsElement.Splitter SplitterDirection.Vertical, EnterDirection.FromTop => [ExitDirection.ToBottom]
+| OpticsElement.Splitter SplitterDirection.Vertical, EnterDirection.FromLeft => [ExitDirection.ToTop, ExitDirection.ToBottom]
+| 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 :=
+  match outDirection with
+  | ExitDirection.ToBottom =>
+    if h : coordinate.y.succ < table.height then
+      some {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⟩}
+    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⟩}
+    else
+      none
+  | ExitDirection.ToRight =>
+    if h : coordinate.x.succ < table.width then
+      some {coordinate with x := ⟨coordinate.x.succ, h⟩}
+    else
+      none
+
+private abbrev SeenExitDirection := BitVec 4
+
+private def SeenExitDirection.top (a : SeenExitDirection) : Bool := a[0]
+private def SeenExitDirection.right (a : SeenExitDirection) : Bool := a[1]
+private def SeenExitDirection.bottom (a : SeenExitDirection) : Bool := a[2]
+private def SeenExitDirection.left (a : SeenExitDirection) : Bool := a[3]
+
+private def SeenExitDirection.setTop : SeenExitDirection → SeenExitDirection := BitVec.setBitTrue 0
+private def SeenExitDirection.setRight : SeenExitDirection → SeenExitDirection := BitVec.setBitTrue 1
+private def SeenExitDirection.setBottom : SeenExitDirection → SeenExitDirection := BitVec.setBitTrue 2
+private def SeenExitDirection.setLeft : SeenExitDirection → SeenExitDirection := BitVec.setBitTrue 3
+
+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 structure SeenExitDirections (table : OpticsTable) extends Parsing.RectangularGrid SeenExitDirection where
+  sameWidth : width = table.width
+  sameHeight : height = table.height
+
+private def SeenExitDirections.empty (table : OpticsTable) : SeenExitDirections table :=
+  {
+    width := table.width
+    height := table.height
+    elements := Array.mkArray (table.width * table.height) default
+    not_empty := table.not_empty
+    size_valid := Array.size_mkArray _ _
+    sameHeight := rfl
+    sameWidth := rfl
+  }
+
+private theorem List.foldl_add_bounded (l : List α) (f : α → Fin n) (h₁ : 0 < n) (init : Nat) : l.foldl (λn e ↦ n + (f e).val) init ≤ n.pred * l.length + init := by
+  unfold List.foldl
+  split
+  case h_1 => exact Nat.le_add_left _ _
+  case h_2 v ll =>
+    have h₂ := List.foldl_add_bounded ll f h₁ (init + (f v).val)
+    rw[List.length_cons, Nat.mul_succ]
+    have h₃ : (f v).val ≤ n.pred := (Nat.le_pred_iff_lt h₁).mpr (f v).isLt
+    rw[←Nat.add_assoc] at h₂
+    have h₄ := Nat.le_of_add_le h₂ h₃
+    rw[Nat.add_assoc] at h₄
+    rw(config := {occs := .pos [3]})[Nat.add_comm] at h₄
+    rw[←Nat.add_assoc] at h₄
+    assumption
+
+/-- For termination proof -/
+private def SeenExitDirections.countExitDirections {table : OpticsTable} (seenDirections : SeenExitDirections table) : Fin (4 * table.width * table.height + 1) :=
+  let c := seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0
+  have h₁ : c ≤ 4 * seenDirections.width * seenDirections.height := by
+    have : c = seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0 := (rfl : c = seenDirections.elements.foldl (λn e ↦ n + e.countDirection.val) 0)
+    rw[this, Array.foldl_eq_foldl_toList]
+    have : seenDirections.elements.toList.length = seenDirections.elements.size :=  Array.length_toList
+    rw[seenDirections.size_valid] at this
+    rw[Nat.mul_assoc,←this]
+    apply (List.foldl_add_bounded seenDirections.elements.toList SeenExitDirection.countDirection (Nat.succ_pos _)) 0
+  have h₂ : (4 * table.width * table.height + 1) = (4 * seenDirections.width * seenDirections.height + 1) := by
+    apply congrArg Nat.succ
+    rw[Nat.mul_assoc, Nat.mul_assoc]
+    apply congrArg
+    rw[seenDirections.sameHeight, seenDirections.sameWidth]
+  Fin.cast h₂.symm ⟨c,Nat.lt_succ_of_le h₁⟩
+
+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
+  --         mark them as seen.
+  -- step 3: recurse
+  -- step 4: profit
+
+  sorry
+
+------------------------------------------------------------------------------------
+
+
+private def testInput := r".|...\....
+|.-.\.....
+.....|-...
+........|.
+..........
+.........\
+..../.\\..
+.-.-/..|..
+.|....-|.\
+..//.|...."
+
+#eval parse testInput
diff --git a/inputs/day16.input b/inputs/day16.input
new file mode 100644
index 0000000..b8e87c8
--- /dev/null
+++ b/inputs/day16.input
@@ -0,0 +1,110 @@
+\........../.......-........|....\.......-..\/....|................\........../.|..././........\.........../..
+...............\..\................/............\................./................../.........\..|....|/|-...
+.../..........................\.....|.............-.......././.......-.|..../|.....-\........-....../.........
+|..........................-..........-......./............................-..|................-..............
+.....|......../...../.......-.\..............................-........|............|/.../../........./........
+..\...|..-......\.........-\.||........|./................\....\........-..\..................../..\....-...|.
+.|...........|............-........./.-.................|.|....../...............|..../..-..-...\...........|.
+..............\............................................................./......................./\....-...
+./........|...\.\..|..-....\............................|........./.................|/...............-........
+\....\./.............../................../....|......./........../.\......./........-....\......../....../|..
+./......--..........\..|.--........-...../......./........\.....|/..................|//...........|.........-.
+.......|.....\-.\..-......-.........|.....................-/\.....-..........|.............-....\.....\.-.....
+..--...\....-..|..................................-......-......\......-................\...../..-/....--.....
+....-.........................\.\............|...............|.....-...\....|-................................
+.................-..|.\..\....-..........|...../.....-...-.-../.............../................-..............
+-..-......|..............................\.....\........|...../........\.................../..................
+..............-.....-.|..........|.\..................|........|...........\.\...|........-...................
+..\............/...\\........../...-..\.../.........\..|................../......\..-.../....................\
+..................|...\......................./...|......../..............-./...\........\......./|...\..-..-.
+.................................................-................|.........................................\.
+......-...............................|./............./...........................-\/..../......\..........\..
+......\....|..........................\.-|..........................|....................\.....\/...-.........
+..\..-|...|.....-...../......./....|...............\................|..|.......\...........................-..
+..\......-.......\.........\................|...........|....../...../..........-./...-|..................../.
+................./.......\...|.....\....-................./......../..\...........-...|.../|................\.
+..|..\./.........\.\.......................-......|....-..../.../................-.......\../.../...../.......
+........../........./..|..-....................\\............\........................-......-......|.........
+.../-....\..\..........\....\\......................................./........\...-.................\.........
+................................../.................|..\.-..|................|/....-.........................|
+...-.................||..../....................-..........................................|.-................
+..//.\..........................|.....|-.............\.\......-....\.\.......\............-..............\-...
+.......|.|..-........./..|........-.....|........................-...................-......\................-
+..-..|..........|....-.............|.|/...../../..................\...\................../......|....|........
+........\..././.............../.............../....-../.....|....\................|/.../.....|.|-..|..........
+......|..........\...-./........-...............................\..........|.............|..\..|......./.....|
+.............................-................................................|................/......\.../..-
+......-........\..........-..../...............\............/.....\......|........................-.|.../.....
+...\...............-....-........-............-...../....|.\.../.......\..-....................|........|.....
+.............................-...\....|...|.......\............................-............\.................
+....................|...-........-.........-..\................/....................../.|.......-.............
+......\.........................../....-....|...........................................\...-.........|......\
+.............\../\..............|\.\..........|\.../..................../\...................|\.......\.......
+/.................../.\\.........................../...........-...-..........-..-............................
+............\......../........-.........../........./.................-................./...........|.........
+.........\.......|.......\........./.....................\..............\\....../...|-....\..|..-.....|.......
+.|....-.............\.........\.\../.......-...........................\./..........................--\......\
+........./..../................./.................\............................................./../.\........
+.....-..............-.-...\/..|....-........./.....................\................./.\..........-...|....|..
+........|...|.-.......|.......-............\.../....|...\............../............-.........................
+........................|.....\........................./\/.........................|.........................
+....\..././..........|.....\......................-................./.....|...............................|-..
+.../.........../.-......\..../.................-...\.....-......\.....\..............//.|..............-..-...
+....../............./-/.\...........\...\..|/........................-...../......\........-./\..........||...
+.................................../............|....................../..|.....\......\............/.........
+.....|....\...|.-./............................./..-....|.\.......................-../.-..-.........\.........
+..........\...|../.......-|............-........../...../..........-......-../.-......|..../.-.../............
+.-.........-............|/.......-........|...................-.........-........../.-........\..........|/...
+.........\.........\....../....|...\\......-..........-................\................................-.....
+............-...../......|...//........\-....|......../........./..................-................../....--.
+...............|.................................|.../...\....................\................|...\.|........
+..............\.........\.........\....|.-.......\.\........-.........../...|.....|..............\.......\....
+........-.-.....|.../......-\..|.....-.........|.-................\......./....\...-.....\..|/...............|
+....|.....................-...................\......\......-.......................-...../........./....\....
+..|...|.......\./..-..............\.............................................\../....|.....................
+..................-../........|.....-\.../................................................./..\...|......-...-
+.....\......\........\.....................|...|../......../....../.\........./...............................
+............../........../...........\..\/..|.\...|..........-................................\-..............
+/...............\...|......\............/|...................|....././...\............................-.|.....
+...........|................/-......\.....-.........-.............../......./............../|.................
+..-...........|..\.............\....|/...............|..../..............\...............|./......|........./.
+.....\\..|......\....\.......-.................\.-......................|........./...|.........|...|...-.....
+-...../....|....../............./.......|/../\.............../...../-\.../-.......|........../..............\\
+..........\....................../.................|...--../..................................................
+.\.................../......|......-.............................//......|.../|.|....\.............\..........
+.\-...........-.........|..................................../........|......../...-............\....-...-....
+......\......|................-...../....|........-..\.....-........//................../.....|.........-.....
+.....-..........-.|/.........-....................../......|.|./........................................./\\|.
+...\................|.........../..-....|..-..........|........../....-....../......./.....-..\.....\\..../...
+.....\.....-..................-...-..../....|....|.................|...\./.............../.......|.\/...../...
+.||......../........../.-...|...........\.................\........-........|........................-...|....
+........./......\......|...............\.\.................................................\.................|
+..........................|....................|..../-...............|....|......../....-..................|..
+.-........\.|......../...|...................|.........|............\.....|.......\........./.................
+................-........................\...........|................../................-.............\......
+.......\..........|.............../...|.-......................../....\.............-.......\./...............
+..........\...........................................-........|.......\........./...-........\...............
+../......./...\|...............-........\................./...\...................../.....-.-....-...........-
+.\../......../....-\................................|.....-..|...............................-................
+..........................\.....|................/.....\......../.............|..............\......./-..|....
+|.........-.|............./......-.................|.......|...\/...........|...........................\\....
+-..................|.........................-.............-.....|..../.........\...-/.....|............/\....
+.........\.\....\...........|....-.../..............|.....|-.......\.............-......./......././.......\..
+..../.....-...........................................\.../..\.|.......................-..//....-......|......
+./-..................\..\....................................\......./.\....|.................................
+...../....................................-....-/........................-/.........-.\...|......./..-.\......
+.....|.............-.......|-..-.................................|-...........................\.|.....|.......
+.........\-.............\.............../....-....|....-.|..........\............|.\...|.....-................
+............/.......-....|./....|../..../......./..\.................-..................|.....................
+../....-........./.....\...............\......-....|...\........../.....|........................\............
+...../.\.............\.........................-..|.......|......-......|................./......./-..........
+...\..........\.......................\.-..././.........|..\..................\...../...|.......|............-
+........./............-..................................|.....................-..............................
+........................|.....\.........\..............-..\..........||...../.\\./....../.....................
+.................-.............\.../...........\...\......--................\.....\.............\....-........
+.../-..........\.\............-.......-.............\..\.\...../........|...-..-..|..........\................
+\.|..\......\-......./.........||..\.........................................................-...../..........
+....|..........................................\......-..........\.../...\-........|..........................
+.......-.......\..//./....|...............\.\..-...\....|....................-......\......\..-......../......
+/..../../....-../....-....-......................\........./..........-/..\......./..\-.../..........|........
+.|....\\........./....\.............-......--\...........|.........|..\...................../........./.\.....
diff --git a/lakefile.lean b/lakefile.lean
index b324bc8..1d653ed 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -18,6 +18,7 @@ lean_lib «Day12» where
 lean_lib «Day13» where
 lean_lib «Day14» where
 lean_lib «Day15» where
+lean_lib «Day16» where
 
 lean_lib «Common» where