From 898e58a116a17b8606b05ecfefa68a7880b20eec Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 19 Sep 2024 18:01:11 +0200
Subject: Continue a bit with Day 11 Part 1

---
 Day11.lean | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 69 insertions(+), 1 deletion(-)

(limited to 'Day11.lean')

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
-- 
cgit v1.2.3