Continue a bit with Day 11 Part 1

2 files changed, 75 insertions, 4 deletions

diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index d0e9427..3c5887a 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -21,10 +21,13 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
   x : Fin grid.width
   y : Fin grid.height
 
-private def RectangularGrid.Coordinate.toIndex {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Fin (grid.width * grid.height) :=
+instance : ToString (RectangularGrid.Coordinate grid) where
+  toString := λx ↦ s!"x: {x.x}/{grid.width}, y : {x.y}/{grid.height}"
+
+def RectangularGrid.Coordinate.toIndex {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Fin (grid.width * grid.height) :=
   ⟨coordinate.x + grid.width * coordinate.y, Nat.two_d_coordinate_to_index_lt_size coordinate.x.isLt coordinate.y.isLt⟩
 
-private def RectangularGrid.Coordinate.ofIndex (grid : RectangularGrid Element) (index : Fin (grid.width * grid.height)) : grid.Coordinate :=
+def RectangularGrid.Coordinate.ofIndex {grid : RectangularGrid Element} (index : Fin (grid.width * grid.height)) : grid.Coordinate :=
   have : grid.width > 0 :=
     have := index.isLt
     match h : grid.width with
@@ -35,7 +38,7 @@ private def RectangularGrid.Coordinate.ofIndex (grid : RectangularGrid Element)
     y := ⟨index.val / grid.width, Nat.div_lt_of_lt_mul index.isLt⟩
   }
 
-theorem Coordinate.toIndex_inv_fromIndex {grid : RectangularGrid Element} (index : Fin (grid.width * grid.height)) : RectangularGrid.Coordinate.toIndex (RectangularGrid.Coordinate.ofIndex grid index) = index := by
+theorem RectangularGrid.Coordinate.toIndex_inv_fromIndex {grid : RectangularGrid Element} (index : Fin (grid.width * grid.height)) : RectangularGrid.Coordinate.toIndex (RectangularGrid.Coordinate.ofIndex index) = index := by
   simp only [RectangularGrid.Coordinate.toIndex, RectangularGrid.Coordinate.ofIndex, Nat.mod_add_div, Fin.eta]
 
 def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Element :=
diff --git a/Day11.lean b/Day11.lean
index da36989..26205f7 100644
--- a/Day11.lean
+++ b/Day11.lean
@@ -1,4 +1,5 @@
 import «Common»
+import «BinaryHeap»
 
 namespace Day11
 
@@ -22,6 +23,65 @@ def parseCharacter : Char → Except ParseCharError Pixel
 | '#' => Except.ok Pixel.galaxy
 | foundChar => Except.error {foundChar}
 
+abbrev TelescopePicture := Parsing.RectangularGrid Pixel
+abbrev PixelPos := Parsing.RectangularGrid.Coordinate (Element := Pixel)
+
+------------------------------------------------------------------------------------------
+
+def galaxies (p : TelescopePicture) : List (PixelPos p) :=
+  let rec worker := λ(index : Fin (p.width * p.height)) ↦
+    match p.elements[index]'(p.size_valid.substr index.isLt) with
+    | .void =>
+      if h : index + 1 < p.width * p.height then
+        worker ⟨index + 1, h⟩
+      else
+        []
+    | .galaxy =>
+      (Parsing.RectangularGrid.Coordinate.ofIndex index) ::
+        if h : index + 1 < p.width * p.height then
+          worker ⟨index + 1, h⟩
+        else
+          []
+  worker ⟨0,Nat.mul_pos p.not_empty.left p.not_empty.right⟩
+
+private def sortGalaxiesByRow (a b : PixelPos p) : Bool :=
+  a.y ≤ b.y
+
+private def sortGalaxiesByRow_wellDefinedLE : BinaryHeap.TotalAndTransitiveLe (sortGalaxiesByRow (p := picture)) := by
+  unfold sortGalaxiesByRow
+  unfold BinaryHeap.TotalAndTransitiveLe BinaryHeap.transitive_le BinaryHeap.total_le
+  simp only [decide_eq_true_eq, and_imp]
+  constructor
+  omega
+  omega
+
+
+/--
+  SORTED FROM LARGEST TO SMALLEST VOID! That's what is easiest to use during expansion.
+  Also, does not include voids after the last galaxy.
+ -/
+def horizontalVoids (galaxies : List (PixelPos p)) : List (Fin p.height) :=
+  let rec worker : {n : Nat} → Fin p.height → BinaryHeap (PixelPos p) sortGalaxiesByRow n → List (Fin p.height) := λ {n : Nat} currentIndex remainingGalaxies ↦
+    match n with
+    | 0 => []
+    | _+1 =>
+      let next := remainingGalaxies.tree.root'
+      if h : currentIndex < next.y then
+        have : currentIndex + 1 < p.height := Nat.lt_of_le_of_lt (Nat.succ_le.mpr h) next.y.isLt
+        currentIndex :: worker ⟨currentIndex + 1,this⟩ remainingGalaxies
+      else if h₂ : currentIndex = next.y ∧ currentIndex + 1 < p.height then
+        worker ⟨currentIndex+1, h₂.right⟩ (remainingGalaxies.pop.snd)
+      else
+        worker currentIndex (remainingGalaxies.pop.snd)
+  termination_by n ci => (p.height - ci) + n
+  worker ⟨0,p.not_empty.right⟩ (BinaryHeap.ofList sortGalaxiesByRow_wellDefinedLE galaxies)
+
+------------------------------------------------------------------------------------------
+
+open DayPart
+instance : Parse ⟨11, by simp⟩ (ι := TelescopePicture) where
+  parse := Except.mapError toString ∘ (Parsing.RectangularGrid.ofString parseCharacter)
+
 ------------------------------------------------------------------------------------------
 
 private def testData := "...#......
@@ -36,4 +96,12 @@ private def testData := "...#......
 #...#.....
 "
 
-#eval Parsing.RectangularGrid.ofString parseCharacter testData
+#eval
+  let data := DayPart.Parse.parse ⟨11,_⟩ testData
+  match data with
+  | .error _ => none
+  | .ok picture =>
+    let gs := galaxies picture
+    let gs := horizontalVoids gs
+    let gs := gs.map Fin.val
+    some gs