Day11

1 files changed, 72 insertions, 19 deletions

diff --git a/Day11.lean b/Day11.lean
index 26205f7..c8ba675 100644
--- a/Day11.lean
+++ b/Day11.lean
@@ -55,26 +55,78 @@ private def sortGalaxiesByRow_wellDefinedLE : BinaryHeap.TotalAndTransitiveLe (s
   omega
   omega
 
+private def sortGalaxiesByColumn (a b : PixelPos p) : Bool :=
+  a.x ≤ b.x
 
-/--
-  SORTED FROM LARGEST TO SMALLEST VOID! That's what is easiest to use during expansion.
-  Also, does not include voids after the last galaxy.
- -/
+private def sortGalaxiesByColumn_wellDefinedLE : BinaryHeap.TotalAndTransitiveLe (sortGalaxiesByColumn (p := picture)) := by
+  unfold sortGalaxiesByColumn
+  unfold BinaryHeap.TotalAndTransitiveLe BinaryHeap.transitive_le BinaryHeap.total_le
+  simp only [decide_eq_true_eq, and_imp]
+  constructor
+  omega
+  omega
+
+/-- Output is from highest to lowest index! -/
 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 ↦
+  let rec worker : {n : Nat} → List (Fin p.height)→ Fin p.height → BinaryHeap (PixelPos p) sortGalaxiesByRow n → List (Fin p.height) := λ {n : Nat} previous currentIndex remainingGalaxies ↦
     match n with
-    | 0 => []
+    | 0 => previous
     | _+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
+        worker (currentIndex :: previous) ⟨currentIndex + 1,this⟩ remainingGalaxies
       else if h₂ : currentIndex = next.y ∧ currentIndex + 1 < p.height then
-        worker ⟨currentIndex+1, h₂.right⟩ (remainingGalaxies.pop.snd)
+        worker previous ⟨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)
+        worker previous currentIndex (remainingGalaxies.pop.snd)
+  termination_by n _ ci => (p.height - ci) + n
+  worker [] ⟨0,p.not_empty.right⟩ (BinaryHeap.ofList sortGalaxiesByRow_wellDefinedLE galaxies)
+
+/-- Output is from highest to lowest index! -/
+def verticalVoids (galaxies : List (PixelPos p)) : List (Fin p.width) :=
+    let rec worker : {n : Nat} → List (Fin p.width) → Fin p.width → BinaryHeap (PixelPos p) sortGalaxiesByColumn n → List (Fin p.width) := λ {n : Nat} previous currentIndex remainingGalaxies ↦
+    match n with
+    | 0 => previous
+    | _+1 =>
+      let next := remainingGalaxies.tree.root'
+      if h : currentIndex < next.x then
+        have : currentIndex + 1 < p.width := Nat.lt_of_le_of_lt (Nat.succ_le.mpr h) next.x.isLt
+        worker (currentIndex :: previous) ⟨currentIndex + 1,this⟩ remainingGalaxies
+      else if h₂ : currentIndex = next.x ∧ currentIndex + 1 < p.width then
+        worker previous ⟨currentIndex+1, h₂.right⟩ (remainingGalaxies.pop.snd)
+      else
+        worker previous currentIndex (remainingGalaxies.pop.snd)
+  termination_by n _ ci => (p.width - ci) + n
+  worker [] ⟨0,p.not_empty.left⟩ (BinaryHeap.ofList sortGalaxiesByColumn_wellDefinedLE galaxies)
+
+-- could use Fin here, but why?
+structure ExpandedUniverseGalaxyCoordinate where
+  x : Nat
+  y : Nat
+deriving Repr
+
+def ExpandedUniverseGalaxyCoordinate.dist (a b : ExpandedUniverseGalaxyCoordinate) : Nat :=
+  let dx := if a.x > b.x then a.x-b.x else b.x-a.x
+  let dy := if a.y > b.y then a.y-b.y else b.y-a.y
+  dx+dy
+
+def expand (expansion : Nat) (galaxies : List (PixelPos p)) : List ExpandedUniverseGalaxyCoordinate :=
+  let vVoids := verticalVoids galaxies
+  let hVoids := horizontalVoids galaxies
+  let horizontallyExpanded := galaxies.map λg ↦ vVoids.foldl (λc v ↦ if v.val ≤ c.x then {c with x := c.x+expansion} else c) (ExpandedUniverseGalaxyCoordinate.mk g.x g.y)
+  horizontallyExpanded.map λg ↦ hVoids.foldl (λc h ↦ if h.val ≤ c.y then {c with y := c.y+expansion} else c) g
+
+def part (expansion : Nat) (p : TelescopePicture) : Nat :=
+  let g := galaxies p
+  let e := expand expansion g
+  let rec distances := λ d cs ↦
+    match cs with
+    | [] => d
+    | c :: cs =>
+      let d := cs.foldl (λa cc ↦ a + (cc.dist c)) d
+      distances d cs
+  distances 0 e
 
 ------------------------------------------------------------------------------------------
 
@@ -82,9 +134,16 @@ open DayPart
 instance : Parse ⟨11, by simp⟩ (ι := TelescopePicture) where
   parse := Except.mapError toString ∘ (Parsing.RectangularGrid.ofString parseCharacter)
 
+instance : Part ⟨11,_⟩ Parts.One (ι := TelescopePicture) (ρ := Nat) where
+  run := some ∘ (part 1)
+
+instance : Part ⟨11,_⟩ Parts.Two (ι := TelescopePicture) (ρ := Nat) where
+  run := some ∘ (part (1000000 - 1))
+
 ------------------------------------------------------------------------------------------
 
-private def testData := "...#......
+private def testData := "
+...#......
 .......#..
 #.........
 ..........
@@ -98,10 +157,4 @@ private def 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
+  data.map (part (1000000 - 1))