From 793bc1538543bbfb48704bab071c6719c6da4aa6 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 29 Nov 2024 22:23:40 +0100
Subject: Day14 Part 2

---
 Day14.lean | 249 ++++++++++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 179 insertions(+), 70 deletions(-)

(limited to 'Day14.lean')

diff --git a/Day14.lean b/Day14.lean
index bbaa616..d0acf6b 100644
--- a/Day14.lean
+++ b/Day14.lean
@@ -1,4 +1,6 @@
 import «Common»
+import Lean.Data.HashMap
+import Lean.Data.HashSet
 
 namespace Day14
 
@@ -41,15 +43,6 @@ def parse : String → Except ParseInputError ControlPanel :=
 
 ------------------------------------------------------------------------------------
 
-/-
-there's probably a better way, but I'm too lazy, so I'll just move them row-by-row.
-pseudocode
-for(row)
-  for(column)
-    if(tile == Round)
-      moveTileAsFarNorthAsPossible
--/
-
 /-- Finds the northmost free space reachable from start. Does not look at start. -/
 private def findNorthmostFreeTile {controlPanel : ControlPanel} (start : controlPanel.Coordinate) : controlPanel.Coordinate :=
   if start.y > ⟨0,controlPanel.not_empty.right⟩ then
@@ -71,70 +64,12 @@ private def moveTileNorth {controlPanel : ControlPanel} (position : controlPanel
     intermediate.set northMost Tile.Round
 
 private theorem moveTileNorth_same_size {controlPanel : ControlPanel} (position : controlPanel.Coordinate) : (moveTileNorth position).width = controlPanel.width ∧ (moveTileNorth position).height = controlPanel.height := by
-  constructor
-  all_goals
-    unfold moveTileNorth
-    match controlPanel[position] with
-    | Tile.Space | Tile.Cube => trivial
-    | Tile.Round =>
-      simp only[Parsing.RectangularGrid.set_same_size]
-
-/-
--- Old solution, without do-notation. Proven to terminate, but needs a lot more code...
-
-/- had to move this to top level function to be able to prove stuff with it... "Declaration contains metavariables" -/
-private def moveAllTilesNorth_handleColumns (cp : ControlPanel) (row : Fin cp.height) (column : Fin cp.width) : ControlPanel :=
-    let intermediate := moveTileNorth {x := column, y := row : cp.Coordinate}
-    let nextIndex := column.val + 1
-    if h : nextIndex < intermediate.width then
-      have h₁ : intermediate.height = cp.height := (moveTileNorth_same_size {x := column, y := row : cp.Coordinate}).right
-      moveAllTilesNorth_handleColumns intermediate (h₁▸row) ⟨nextIndex,h⟩
-    else
-      intermediate
-  termination_by cp.width - column
-  decreasing_by
-    have h₂ := (moveTileNorth_same_size { x := column, y := row }).left
-    rw[h₂] at h ⊢
-    exact Nat.sub_lt_of_gt (Nat.le_of_lt h) (Nat.lt_succ.mpr $ Nat.le_refl _)
-
-private theorem moveAllTilesNorth_handleColumns_same_height (cp : ControlPanel) (row : Fin cp.height) (column : Fin cp.width) : (moveAllTilesNorth_handleColumns cp row column).height = cp.height := by
-  unfold moveAllTilesNorth_handleColumns
-  simp
-  have h₂ := (moveTileNorth_same_size { x := column, y := row }).right
-  split
-  case isFalse => exact h₂
-  case isTrue =>
-    have := moveAllTilesNorth_handleColumns_same_height (Day14.moveTileNorth { x := column, y := row }) (h₂ ▸ row) ⟨↑column + 1, by assumption⟩
-    simp[h₂] at this
-    assumption
-  termination_by cp.width - column
-  decreasing_by
-    have h₂ := (moveTileNorth_same_size { x := column, y := row }).left
-    rename_i h
-    rw[h₂] at h ⊢
-    exact Nat.sub_lt_of_gt (Nat.le_of_lt h) (Nat.lt_succ.mpr $ Nat.le_refl _)
-
-private def moveAllTilesNorth (controlPanel : ControlPanel) : ControlPanel :=
-  handleRows (controlPanel) ⟨0,controlPanel.not_empty.right⟩
-where
-  handleRows (cp : ControlPanel) (row : Fin cp.height) : ControlPanel :=
-    let intermediate := moveAllTilesNorth_handleColumns cp row ⟨0,cp.not_empty.left⟩
-    let nextIndex := row.val + 1
-    if h : nextIndex < intermediate.height then
-      handleRows intermediate ⟨nextIndex, h⟩
-    else
-      intermediate
-    termination_by cp.height - row
-    decreasing_by
-      have h₁ : intermediate.height = cp.height :=
-        moveAllTilesNorth_handleColumns_same_height cp row ⟨0,_⟩
-      rw[h₁] at h ⊢
-      exact Nat.sub_lt_of_gt (Nat.le_of_lt h) (Nat.lt_succ.mpr $ Nat.le_refl _)
--/
+  unfold moveTileNorth
+  constructor <;> split <;> rfl
 
 private def moveAllTilesNorth (controlPanel : ControlPanel) : ControlPanel := Id.run do
   let mut result : ((c : ControlPanel) ×' (c.width = controlPanel.width ∧ c.height = controlPanel.height)) := ⟨controlPanel, ⟨rfl,rfl⟩⟩
-  for hr :row in [:controlPanel.height] do
+  for hr : row in [:controlPanel.height] do
     for hc : column in [:controlPanel.width] do
       let x : Fin result.fst.width := Fin.cast result.snd.left.symm ⟨column,hc.upper⟩
       let y : Fin result.fst.height := Fin.cast result.snd.right.symm ⟨row,hr.upper⟩
@@ -157,6 +92,175 @@ def part1 : (input : ControlPanel) → Nat := weightOnNorthSupport ∘ moveAllTi
 
 ------------------------------------------------------------------------------------
 
+/-- Finds the westmost free space reachable from start. Does not look at start. -/
+private def findWestmostFreeTile {controlPanel : ControlPanel} (start : controlPanel.Coordinate) : controlPanel.Coordinate :=
+  if start.x > ⟨0,controlPanel.not_empty.left⟩ then
+    let westNeighbour := { start with x := ⟨start.x - 1,Nat.lt_imp_pred_lt start.x.isLt⟩ }
+    match controlPanel[westNeighbour] with
+    | Tile.Space => findWestmostFreeTile westNeighbour
+    | Tile.Round | Tile.Cube => start
+  else
+    start
+termination_by start.x
+
+/-- Finds the southmost free space reachable from start. Does not look at start. -/
+private def findSouthmostFreeTile {controlPanel : ControlPanel} (start : controlPanel.Coordinate) : controlPanel.Coordinate :=
+  if h : start.y.val.succ < controlPanel.height then
+    let southNeighbour := { start with y := ⟨start.y.val.succ,h⟩ }
+    match controlPanel[southNeighbour] with
+    | Tile.Space => findSouthmostFreeTile southNeighbour
+    | Tile.Round | Tile.Cube => start
+  else
+    start
+
+/-- Finds the eastmost free space reachable from start. Does not look at start. -/
+private def findEastmostFreeTile {controlPanel : ControlPanel} (start : controlPanel.Coordinate) : controlPanel.Coordinate :=
+  if h : start.x.val.succ < controlPanel.width then
+    let eastNeighbour := { start with x := ⟨start.x.val.succ,h⟩ }
+    match controlPanel[eastNeighbour] with
+    | Tile.Space => findEastmostFreeTile eastNeighbour
+    | Tile.Round | Tile.Cube => start
+  else
+    start
+
+private def moveTileInDirection (direction : {c : ControlPanel} → c.Coordinate → c.Coordinate) {controlPanel : ControlPanel} (position : controlPanel.Coordinate) : ControlPanel :=
+   match controlPanel[position] with
+  | Tile.Space | Tile.Cube => controlPanel
+  | Tile.Round =>
+    let intermediate := controlPanel.set position Tile.Space
+    let positionInIntermediate : intermediate.Coordinate := {x := position.x, y := position.y} -- how? well, I won't complain
+    let northMost := direction positionInIntermediate
+    intermediate.set northMost Tile.Round
+
+private theorem moveTileInDirection_same_size (direction : {c : ControlPanel} → c.Coordinate → c.Coordinate) {controlPanel : ControlPanel} (position : controlPanel.Coordinate) : (moveTileInDirection direction position).width = controlPanel.width ∧ (moveTileInDirection direction position).height = controlPanel.height := by
+  unfold moveTileInDirection
+  constructor <;> split <;> rfl
+
+private def moveTileWest : {controlPanel : ControlPanel} → controlPanel.Coordinate → ControlPanel :=
+  moveTileInDirection findWestmostFreeTile
+private def moveTileSouth : {controlPanel : ControlPanel} → controlPanel.Coordinate → ControlPanel :=
+  moveTileInDirection findSouthmostFreeTile
+private def moveTileEast : {controlPanel : ControlPanel} → controlPanel.Coordinate → ControlPanel :=
+  moveTileInDirection findEastmostFreeTile
+
+private theorem moveTileWest_same_size : {controlPanel : ControlPanel} → (position : controlPanel.Coordinate) → (moveTileWest position).width = controlPanel.width ∧ (moveTileWest position).height = controlPanel.height :=
+  moveTileInDirection_same_size findWestmostFreeTile
+private theorem moveTileEast_same_size : {controlPanel : ControlPanel} → (position : controlPanel.Coordinate) → (moveTileEast position).width = controlPanel.width ∧ (moveTileEast position).height = controlPanel.height :=
+  moveTileInDirection_same_size findEastmostFreeTile
+private theorem moveTileSouth_same_size : {controlPanel : ControlPanel} → (position : controlPanel.Coordinate) → (moveTileSouth position).width = controlPanel.width ∧ (moveTileSouth position).height = controlPanel.height :=
+  moveTileInDirection_same_size findSouthmostFreeTile
+
+private def moveAllTilesWest (controlPanel : ControlPanel) : ControlPanel := Id.run do
+  let mut result : ((c : ControlPanel) ×' (c.width = controlPanel.width ∧ c.height = controlPanel.height)) := ⟨controlPanel, ⟨rfl,rfl⟩⟩
+  for hr : row in [:controlPanel.height] do
+    for hc : column in [:controlPanel.width] do
+      let x : Fin result.fst.width := Fin.cast result.snd.left.symm ⟨column,hc.upper⟩
+      let y : Fin result.fst.height := Fin.cast result.snd.right.symm ⟨row,hr.upper⟩
+      let coordinate : result.fst.Coordinate := {x, y}
+      have : (moveTileWest coordinate).width = controlPanel.width ∧ (moveTileWest coordinate).height = controlPanel.height :=
+        (moveTileWest_same_size coordinate).right.substr $ (moveTileWest_same_size coordinate).left.substr result.snd
+      result := ⟨moveTileWest coordinate, this⟩
+  result.fst
+
+private def moveAllTilesSouth (controlPanel : ControlPanel) : ControlPanel := Id.run do
+  let mut result : ((c : ControlPanel) ×' (c.width = controlPanel.width ∧ c.height = controlPanel.height)) := ⟨controlPanel, ⟨rfl,rfl⟩⟩
+  for row in [:controlPanel.height] do
+    for hc : column in [:controlPanel.width] do
+      let x : Fin result.fst.width := Fin.cast result.snd.left.symm ⟨column,hc.upper⟩
+      have : controlPanel.height - 1 - row < controlPanel.height :=
+        Nat.lt_of_le_of_lt (Nat.sub_le _ _) (Nat.pred_lt (Nat.pos_iff_ne_zero.mp controlPanel.not_empty.right))
+      let y : Fin result.fst.height := Fin.cast result.snd.right.symm ⟨controlPanel.height - 1 - row,this⟩
+      let coordinate : result.fst.Coordinate := {x, y}
+      have : (moveTileSouth coordinate).width = controlPanel.width ∧ (moveTileSouth coordinate).height = controlPanel.height :=
+        (moveTileSouth_same_size coordinate).right.substr $ (moveTileSouth_same_size coordinate).left.substr result.snd
+      result := ⟨moveTileSouth coordinate, this⟩
+  result.fst
+
+private def moveAllTilesEast (controlPanel : ControlPanel) : ControlPanel := Id.run do
+  let mut result : ((c : ControlPanel) ×' (c.width = controlPanel.width ∧ c.height = controlPanel.height)) := ⟨controlPanel, ⟨rfl,rfl⟩⟩
+  for hr : row in [:controlPanel.height] do
+    for column in [:controlPanel.width] do
+      have : controlPanel.width - 1 - column < controlPanel.width :=
+        Nat.lt_of_le_of_lt (Nat.sub_le _ _) (Nat.pred_lt (Nat.pos_iff_ne_zero.mp controlPanel.not_empty.left))
+      let x : Fin result.fst.width := Fin.cast result.snd.left.symm ⟨controlPanel.width - 1 - column,this⟩
+      let y : Fin result.fst.height := Fin.cast result.snd.right.symm ⟨row,hr.upper⟩
+      let coordinate : result.fst.Coordinate := {x, y}
+      have : (moveTileEast coordinate).width = controlPanel.width ∧ (moveTileEast coordinate).height = controlPanel.height :=
+        (moveTileEast_same_size coordinate).right.substr $ (moveTileEast_same_size coordinate).left.substr result.snd
+      result := ⟨moveTileEast coordinate, this⟩
+  result.fst
+
+private def cycle (controlPanel : ControlPanel) : ControlPanel :=
+  let n := moveAllTilesNorth controlPanel
+  let w := moveAllTilesWest n
+  let s := moveAllTilesSouth w
+  moveAllTilesEast s
+
+private def compareControlPanels (a b : ControlPanel) : Bool :=
+  if h₁ : a.width = b.width ∧ a.height = b.height then
+    Id.run do
+    for hr : row in [:a.height] do
+      for hc : column in [:a.width] do
+        let ca : a.Coordinate := {x := ⟨column, hc.upper⟩, y := ⟨row, hr.upper⟩}
+        let cb : b.Coordinate := {x := ⟨column, h₁.left.subst hc.upper⟩, y := ⟨row, h₁.right.subst hr.upper⟩}
+        if !(a[ca] == b[cb]) then
+          return false
+    return true
+  else
+    false
+
+/-- (Bad) Hash-Function for ControlPanel. It's good enough for this riddle, but that's about it. -/
+private def hashControlPanel (p : ControlPanel) : UInt64 := Id.run do
+  let mut hash : UInt64 := mixHash ⟨Fin.ofNat' _ p.width⟩ ⟨Fin.ofNat' _ p.height⟩
+  for hi : index in [:p.elements.size] do
+    match p.elements[index] with
+    | Tile.Round => hash := mixHash hash ⟨Fin.ofNat' _ index⟩
+    | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat' _ (index + p.elements.size)⟩
+    | Tile.Space => continue
+  hash
+
+private instance : BEq ControlPanel where
+beq := compareControlPanels
+
+private instance : Hashable ControlPanel where
+hash := hashControlPanel
+
+structure Part2Memory where
+  seenHashes : Std.HashSet UInt64 -- If this becomes too large, it could be replaced by a Bloom Filter
+  recordedPanels : Std.HashMap ControlPanel Nat
+deriving Inhabited
+
+private def runCycles (cycleCount : Nat) (controlPanel : ControlPanel) : StateM (Part2Memory) ControlPanel :=
+  match cycleCount with
+  | 0 => pure controlPanel
+  | p+1 => do
+    let r := cycle controlPanel
+    let s ← get
+    let (seen, seenHashes) := s.seenHashes.containsThenInsert (hash r)
+    set {s with seenHashes}
+    if seen then
+      let s ← get
+      let (maybePreviousCount, recordedPanels) := s.recordedPanels.getThenInsertIfNew? r p
+      set {s with recordedPanels}
+      if let some previousCount := maybePreviousCount then
+        let period := previousCount - p
+        let remaining := p % period
+        runCycles remaining r
+      else
+        runCycles p r
+    else
+      runCycles p r
+termination_by cycleCount
+decreasing_by
+  exact Nat.lt_succ_of_le $ Nat.mod_le _ _
+  exact Nat.le_refl _
+
+def part2 (input : ControlPanel) : Nat :=
+  let r := StateT.run' (runCycles 1000000000 input) Inhabited.default
+  weightOnNorthSupport r
+
+------------------------------------------------------------------------------------
+
 open DayPart
 instance : Parse ⟨14, by simp⟩ (ι := ControlPanel) where
   parse := Except.mapError toString ∘ parse
@@ -164,6 +268,9 @@ instance : Parse ⟨14, by simp⟩ (ι := ControlPanel) where
 instance : Part ⟨14,_⟩ Parts.One (ι := ControlPanel) (ρ := Nat) where
   run := some ∘ part1
 
+instance : Part ⟨14,_⟩ Parts.Two (ι := ControlPanel) (ρ := Nat) where
+  run := some ∘ part2
+
 ------------------------------------------------------------------------------------
 
 private def testInput := "O....#....
@@ -180,3 +287,5 @@ O.#..O.#.#
 #eval parse testInput
 
 #eval (weightOnNorthSupport ∘ moveAllTilesNorth) <$> parse testInput
+
+#eval part2 <$> parse testInput
-- 
cgit v1.2.3