diff options
| -rw-r--r-- | Common.lean | 1 | ||||
| -rw-r--r-- | Common/BitVec.lean | 11 | ||||
| -rw-r--r-- | Common/Nat.lean | 3 | ||||
| -rw-r--r-- | Common/Parsing.lean | 6 | ||||
| -rw-r--r-- | Day16.lean | 200 | ||||
| -rw-r--r-- | inputs/day16.input | 110 | ||||
| -rw-r--r-- | lakefile.lean | 1 |
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 |