Begin Day 11.

5 files changed, 52 insertions, 0 deletions

diff --git a/Common.lean b/Common.lean
index e5911b2..1382714 100644
--- a/Common.lean
+++ b/Common.lean
@@ -6,3 +6,4 @@ import Common.List
 import Common.Char
 import Common.Euclid
 import Common.NonEmptyList
+import Common.Parsing
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
new file mode 100644
index 0000000..a89d785
--- /dev/null
+++ b/Common/Parsing.lean
@@ -0,0 +1,46 @@
+/- This file contains various parsing helpers. Started _after_ Day10. -/
+
+namespace Parsing
+
+structure RectangularGrid (Element : Type) where
+  width : Nat
+  height : Nat
+  elements : Array Element
+  valid : elements.size = width * height
+
+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) :=
+  ⟨coordinate.x + grid.width * coordinate.y,
+    Nat.le_pred_of_lt coordinate.y.isLt
+    |> Nat.mul_le_mul_left grid.width
+    |> Nat.add_le_add_iff_right.mpr
+    |> (Nat.mul_pred grid.width grid.height).subst (motive :=λx↦grid.width * coordinate.y.val + grid.width ≤ x + grid.width)
+    |> (Nat.sub_add_cancel (Nat.le_mul_of_pos_right grid.width (Nat.zero_lt_of_lt coordinate.y.isLt))).subst
+    |> (Nat.add_comm _ _).subst (motive := λx↦x ≤ grid.width*grid.height)
+    |> Nat.le_sub_of_add_le
+    |> Nat.lt_of_lt_of_le coordinate.x.isLt
+    |> λx↦(Nat.add_lt_add_right) x (grid.width * coordinate.y.val)
+    |> (Nat.sub_add_cancel (Nat.le_of_lt ((Nat.mul_lt_mul_left (Nat.zero_lt_of_lt coordinate.x.isLt)).mpr coordinate.y.isLt))).subst⟩
+
+private 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
+    | Nat.zero => absurd ((Nat.zero_mul grid.height).subst (h.subst (motive := λx↦index<x*grid.height) this)) (Nat.not_lt_zero index.val)
+    | Nat.succ ww => Nat.succ_pos ww
+  {
+    x := ⟨index.val % grid.width, Nat.mod_lt index.val this⟩
+    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
+  simp only [RectangularGrid.Coordinate.toIndex, RectangularGrid.Coordinate.ofIndex, Nat.mod_add_div, Fin.eta]
+
+def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Element :=
+  grid.elements[coordinate.toIndex]'(grid.valid.substr coordinate.toIndex.isLt)
+
+instance : GetElem (RectangularGrid Element) (RectangularGrid.Coordinate grid) Element (λg _ ↦ g = grid) where
+  getElem := λ g c h ↦ g.Get (h▸c)
diff --git a/Day11.lean b/Day11.lean
new file mode 100644
index 0000000..d061e96
--- /dev/null
+++ b/Day11.lean
@@ -0,0 +1,3 @@
+import «Common»
+
+namespace Day11
diff --git a/Main.lean b/Main.lean
index 05f34d3..5adfb28 100644
--- a/Main.lean
+++ b/Main.lean
@@ -9,6 +9,7 @@ import «Day7»
 import «Day8»
 import «Day9»
 import «Day10»
+import «Day11»
 
 open DayPart
 
diff --git a/lakefile.lean b/lakefile.lean
index 53cb5d0..5698911 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,6 +13,7 @@ lean_lib «Day7» where
 lean_lib «Day8» where
 lean_lib «Day9» where
 lean_lib «Day10» where
+lean_lib «Day11» where
 
 lean_lib «Common» where