Day 10 Parsing. If I don' want to prove the inverse, it's done.

1 files changed, 100 insertions, 6 deletions

diff --git a/Day10.lean b/Day10.lean
index a9bc129..a679425 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -7,7 +7,18 @@ structure Coordinate (width : Nat) (height : Nat) where
   y : Fin height
 
 def Coordinate.toIndex {w h : Nat} (c : Coordinate w h) : Fin (w*h) :=
-  Fin.mk (c.x.val * c.y.val) (Nat.mul_lt_mul_of_lt_of_lt c.x.isLt c.y.isLt)
+  Fin.mk (c.x.val + w * c.y.val) (
+    Nat.le_pred_of_lt c.y.isLt
+      |> Nat.mul_le_mul_left w
+      |> Nat.add_le_add_iff_right.mpr
+      |> (Nat.mul_pred w h).subst (motive :=λx↦w * c.y.val + w ≤ x + w)
+      |> (Nat.sub_add_cancel (Nat.le_mul_of_pos_right w (Nat.zero_lt_of_lt c.y.isLt))).subst
+      |> (Nat.add_comm _ _).subst (motive := λx↦x ≤ w*h)
+      |> Nat.le_sub_of_add_le
+      |> Nat.lt_of_lt_of_le c.x.isLt
+      |> λx↦(Nat.add_lt_add_right) x (w * c.y.val)
+      |> (Nat.sub_add_cancel (Nat.le_of_lt ((Nat.mul_lt_mul_left (Nat.zero_lt_of_lt c.x.isLt)).mpr c.y.isLt))).subst
+  )
 
 def Coordinate.fromIndex {w h : Nat} (index : Fin (w*h)) : Coordinate w h :=
   have : w > 0 :=
@@ -20,6 +31,9 @@ def Coordinate.fromIndex {w h : Nat} (index : Fin (w*h)) : Coordinate w h :=
     y := ⟨index.val / w, Nat.div_lt_of_lt_mul index.isLt⟩
   }
 
+theorem Coordinate.toIndex_inv_fromIndex {w h : Nat} (index : Fin (w*h)) : Coordinate.toIndex (Coordinate.fromIndex index) = index := by
+  simp only [toIndex, fromIndex, Nat.mod_add_div, Fin.eta]
+
 inductive Pipe
 | NS : Pipe
 | WE : Pipe
@@ -76,6 +90,9 @@ structure Area where
   fields : Array Tile
   size_invariant : fields.size = width * height
   start_invariant : fields[start.toIndex] = Tile.start
+  -- It would also be possible to prove the inverse - that having an index that gives Tile.start
+  -- implies that this index is equal to start.toIndex, but that is not needed in the solution
+  -- I have a half-finished proof on a local branch.
 
 inductive Area.ParseError
 | NoInput
@@ -360,11 +377,6 @@ private theorem Except.get_unfold' {α : Type u1} {ε : Type u2} {e : Except ε
 
 private theorem Except.get_pure {α : Type u1} (ε : Type u2) (v : α) : Except.get (α := α) (ε := ε) (pure v) (rfl) = v := rfl
 
-private theorem Option.get_unfold {α : Type u} {v : α} : (some v).get (rfl) = v := rfl
-
-private theorem Option.get_unfold' {α : Type u} {o : Option α} {v : α} (h₁ : o = some v) (h₂ : o.isSome) : o.get h₂ = v := by
-  simp[h₁]
-
 private theorem Array.getElem!_eq_getElem {α : Type u} [Inhabited α] {a : Array α} {index : Nat} (h : index < a.size ): a[index] = a[index]! := by
   unfold getElem getElem! instGetElem?OfGetElemOfDecidable Array.instGetElemNatLtSize decidableGetElem?
   simp
@@ -581,3 +593,85 @@ private theorem Area.ParseRaw_start_position :
     simp_all
     rw[←this]
     apply Array.getElem!_eq_getElem
+
+-- Finally.
+private def Area.parse (input : String) : Except Area.ParseError Area :=
+  let raw := Area.parseRaw input
+  match he : raw with
+  | Except.error e => throw e
+  | Except.ok vraw =>
+    match hs : vraw.start with
+    | .none => throw Area.ParseError.NoStart
+    | .some s =>
+      have except_ok := (Except.isOk_exists.mpr ⟨vraw, he⟩)
+      have hw : (Day10.Except.get (Day10.Area.parseRaw input) except_ok).width = vraw.width := by have : raw = Day10.Area.parseRaw input := rfl; simp[←this]; rw[Except.get_unfold' he]
+      have hh : (Day10.Except.get (Day10.Area.parseRaw input) except_ok).height = vraw.height := by have : raw = Day10.Area.parseRaw input := rfl; simp[←this]; rw[Except.get_unfold' he]
+      have finc : vraw.width * vraw.height = (Day10.Except.get (Day10.Area.parseRaw input) except_ok).width * (Day10.Except.get (Day10.Area.parseRaw input) except_ok).height := by rw[hh,hw]
+      have is_some : (Day10.Except.get (Day10.Area.parseRaw input) except_ok).start.isSome := by
+        have : raw = Day10.Area.parseRaw input := rfl
+        unfold Except.get
+        split
+        simp_all
+        rename_i d _ _ _ _
+        subst d
+        simp[hs]
+      have as := Area.ParseRaw_array_size input (Except.isOk_exists.mpr ⟨vraw, he⟩)
+      have as : vraw.fields.size = vraw.width * vraw.height := (Except.get_unfold' he except_ok).subst (motive := λx↦ x.fields.size = x.width * x.height) as
+      have sp := ParseRaw_start_position input (Except.isOk_exists.mpr ⟨vraw, he⟩) is_some
+      have sp : vraw.fields[(Coordinate.fromIndex s).toIndex] = Tile.start := by
+        simp[Except.get_unfold' he except_ok] at sp
+        simp[Coordinate.toIndex_inv_fromIndex]
+        rw[Array.getElem!_eq_getElem] at sp ⊢
+        have : ((Day10.Except.get (Day10.Area.parseRaw input) _).start.get is_some).val = s.val := by
+          unfold Option.get
+          split
+          rename_i s₂ _ h₁ _
+          have : (Day10.Except.get (Day10.Area.parseRaw input) except_ok) = vraw := by
+            rw[Except.get_unfold']
+            exact he
+          subst this
+          simp[hs] at h₁
+          exact Fin.ext_iff.mp h₁.symm
+        rw[this] at sp
+        exact sp
+
+      Except.ok {
+        width := vraw.width --: Nat
+        height := vraw.height --: Nat
+        start := Coordinate.fromIndex s -- Coordinate width height
+        fields := vraw.fields--: Array Tile
+        size_invariant := as --: fields.size = width * height
+        start_invariant := sp --: fields[start.toIndex] = Tile.start
+      }
+
+
+------------------------------------------------------------------------------------------------------------
+
+def Area.getTile (area : Area) (c : Coordinate area.width area.height) : Tile :=
+  area.fields[c.toIndex]'(area.size_invariant.substr c.toIndex.is_lt)
+
+def Area.can_connect_to (area : Area) (current : Coordinate area.width area.height) (other : Coordinate area.width area.height) : Prop :=
+  -- North is negative y, South positive y
+  -- West is negative x, East positive x
+  let is_succ := λ {n : Nat} (a b : Fin n) ↦ if h: a.succ.val < n then b = Fin.castLT a.succ h else False
+  match area.getTile current with
+  | .ground => False
+  | .start => False
+  | .pipe .NE => (is_succ current.x other.x ∧ current.y = other.y) ∨ (is_succ other.y current.y ∧ current.x = other.x)
+  | .pipe .ES => (is_succ current.x other.x ∧ current.y = other.y) ∨ (is_succ current.y other.y ∧ current.x = other.x)
+  | .pipe .SW => (is_succ other.x current.x ∧ current.y = other.y) ∨ (is_succ current.y other.y ∧ current.x = other.x)
+  | .pipe .WN => (is_succ other.x current.x ∧ current.y = other.y) ∨ (is_succ other.y current.y ∧ current.x = other.x)
+  | .pipe .WE => (is_succ current.x other.x ∧ current.y = other.y) ∨ (is_succ other.x current.x ∧ current.y = other.y)
+  | .pipe .NS => (is_succ other.y current.y ∧ current.x = other.x) ∨ (is_succ current.y other.y ∧ current.x = other.x)
+
+def Area.are_connected (area : Area) (current : Coordinate area.width area.height) (previous : Coordinate area.width area.height) : Prop :=
+  area.can_connect_to current previous ∧ area.can_connect_to previous current
+
+structure Area.PathHead where
+  area : Area
+  current : Coordinate area.width area.height
+  previous : Coordinate area.width area.height
+  current_can_connect_to_previous : area.can_connect_to current previous
+
+def Area.nextPathStep (last_step : Area.PathHead) : Option (Area.PathHead) :=
+  sorry