diff options
| -rw-r--r-- | Common/Parsing.lean | 9 | ||||
| -rw-r--r-- | Day11.lean | 70 |
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 := @@ -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 |