Day 14, Part 1.

2 files changed, 14 insertions, 0 deletions

diff --git a/Common/Nat.lean b/Common/Nat.lean
index 3a605a9..9d0ee29 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -20,3 +20,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) :=
   match b with
   | 0 => h₁
   | _ + 1 => /-(Nat.pred_succ a).substr $-/ Nat.lt_succ_of_lt h₁
+
+theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) :=
+  Nat.lt_of_le_of_lt (Nat.pred_le a) h₁
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 3c5887a..c811319 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -47,6 +47,17 @@ def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coor
 instance : GetElem (RectangularGrid Element) (RectangularGrid.Coordinate grid) Element (λg _ ↦ g = grid) where
   getElem := λ g c h ↦ g.Get (h▸c)
 
+def RectangularGrid.set {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : RectangularGrid Element :=
+  let index := (Fin.cast grid.size_valid.symm coordinate.toIndex)
+  {
+    grid with
+      elements := grid.elements.set index value
+      size_valid := (grid.elements.size_set index value).substr grid.size_valid
+  }
+
+theorem RectangularGrid.set_same_size {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : (grid.set coordinate value).width = grid.width ∧ (grid.set coordinate value).height = grid.height :=
+  ⟨rfl,rfl⟩
+
 instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where
   toString := λe ↦ Id.run do
     let mut r := s!"Width: {e.width}, Height: {e.height}"