From e51fe8383dd629470d3468ed37a9dba09c881b6b Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Thu, 19 Sep 2024 20:25:02 +0200 Subject: Day11 --- Day11.lean | 91 +++++++++++++++++++++++++++++++++++++++++++++++++------------- Main.lean | 2 ++ 2 files changed, 74 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)) diff --git a/Main.lean b/Main.lean index 5adfb28..0f87cc0 100644 --- a/Main.lean +++ b/Main.lean @@ -42,6 +42,8 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String := | ⟨9,_⟩, Parts.Two => try_run_day_part_impl ⟨9,_⟩ Parts.Two data | ⟨10,_⟩, Parts.One => try_run_day_part_impl ⟨10,_⟩ Parts.One data | ⟨10,_⟩, Parts.Two => try_run_day_part_impl ⟨10,_⟩ Parts.Two data + | ⟨11,_⟩, Parts.One => try_run_day_part_impl ⟨11,_⟩ Parts.One data + | ⟨11,_⟩, Parts.Two => try_run_day_part_impl ⟨11,_⟩ Parts.Two data | _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet." def main (parameters : List String): IO Unit := do -- cgit v1.2.3