Parser for Day10, maybe done.

3 files changed, 138 insertions, 14 deletions

diff --git a/Day10.lean b/Day10.lean
index d2ebec2..a9bc129 100644
--- a/Day10.lean
+++ b/Day10.lean
@@ -29,12 +29,42 @@ inductive Pipe
 | WN : Pipe
 deriving BEq
 
+instance : LawfulBEq Pipe where
+  eq_of_beq := by
+    intros a b
+    cases a <;> cases b
+    <;> simp
+    all_goals rfl
+  rfl := by
+    intro a
+    cases a
+    all_goals rfl
+
+
 inductive Tile
 | pipe : Pipe → Tile
 | ground : Tile
 | start : Tile
 deriving BEq
 
+instance : LawfulBEq Tile where
+  eq_of_beq := by
+    intros a b
+    cases a <;> cases b
+    <;> simp
+    all_goals try rfl
+    case pipe.pipe =>
+      intros h
+      exact eq_of_beq h
+  rfl := by
+    intro a
+    cases a
+    all_goals try rfl
+    case pipe =>
+      rename_i p
+      cases p
+      <;> rfl
+
 instance : Inhabited Tile where
   default := Tile.ground
 
@@ -335,11 +365,111 @@ private theorem Option.get_unfold {α : Type u} {v : α} : (some v).get (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
+  split
+  <;> rename_i blah
+  <;> simp[h] at blah
+  assumption
+
+private theorem Array.get_push {α : Type u} (arr : Array α) (v : α) (index : Nat) (h₁ : index < arr.size) : arr[index] = (arr.push v)[index]'(by simp[Nat.lt_succ.mpr (Nat.le_of_lt h₁)]) := by
+  cases arr
+  unfold Array.push getElem Array.instGetElemNatLtSize Array.get
+  simp
+  rw[List.getElem_append]
+
 private theorem Area.ParseLine_leaves_start_if_some (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) {res : (Nat × Area.Raw)} (h₂ : (Area.parseLine previous pos line h₁) = Except.ok res) (h₃ : previous.start.isSome) : Fin.val <$> res.2.start = Fin.val <$> previous.start := by
-  sorry
+  unfold Area.parseLine at h₂
+  split at h₂
+  case isTrue => simp at h₂; rw[←h₂]
+  case isFalse h₄ =>
+    split at h₂ ; exact h₂.rec
+    case isFalse h₅ =>
+      unfold bind Monad.toBind Except.instMonad Except.bind at h₂
+      simp at h₂
+      split at h₂; simp at h₂
+      case h_2 d1 tile _ =>
+        clear d1
+        split at h₂; exact h₂.rec
+        exact Area.ParseLine_leaves_start_if_some  { width := previous.width, height := previous.height, start := previous.start, fields := previous.fields.push tile } (pos + 1) (line.drop 1) h₁ h₂ h₃
+termination_by previous.width - pos
 
 private theorem Area.ParseLine_only_adds_to_fields (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) {res : (Nat × Area.Raw)} (h₂ : (Area.parseLine previous pos line h₁) = Except.ok res) (index : Fin (previous.fields.size)) : previous.fields[index.val]! = res.2.fields[index.val]! := by
-  sorry
+  unfold Area.parseLine at h₂
+  split at h₂
+  case isTrue => simp at h₂; rw[←h₂]
+  case isFalse h₃ =>
+    split at h₂; exact h₂.rec
+    case isFalse h₄ =>
+      unfold bind Monad.toBind Except.instMonad Except.bind at h₂
+      simp at h₂
+      split at h₂; simp at h₂
+      case h_2 d1 tile _ =>
+        clear d1
+        split at h₂
+        case' isFalse =>
+          have h₅ := Area.ParseLine_only_adds_to_fields { width := previous.width, height := previous.height, start := previous.start, fields := previous.fields.push tile } (pos + 1) (line.drop 1) h₁ h₂ (Fin.castLE (by simp) index)
+        case' isTrue =>
+          split at h₂; exact h₂.rec
+          have h₅ := Area.ParseLine_only_adds_to_fields { width := previous.width, height := previous.height, start := some ⟨previous.width * (previous.height - 1) + pos, _⟩, fields := previous.fields.push tile } (pos + 1) (line.drop 1) h₁ h₂ (Fin.castLE (by simp) index)
+        all_goals
+          simp at h₅
+          rw[←h₅]
+          have h₆ : ↑index < (previous.fields.push tile).size := by simp; exact Nat.lt_succ.mpr (Nat.le_of_lt index.isLt)
+          simp[←Array.getElem!_eq_getElem]
+          simp[←Array.getElem!_eq_getElem h₆]
+          apply Array.get_push
+termination_by previous.width - pos
+
+private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) (line : Substring) (h₁ : previous.height > 0) (h₂ : previous.fields.size = previous.width * (previous.height - 1) + pos) (h₃ : previous.start = none) {res : Area.Raw} {added : Nat} (h₄ : (Area.parseLine previous pos line h₁) = Except.ok (added, res)) : match res.start with | none => True | some s => res.fields[s]! = Tile.start := by
+  split; trivial
+  case h_2 d1 index hindex =>
+    clear d1
+    unfold Area.parseLine at h₄
+    simp at h₄
+    split at h₄
+    case isTrue => simp at h₄; rw[h₄.right] at h₃; rw[hindex] at h₃; contradiction
+    case isFalse d2 =>
+      clear d2
+      split at h₄
+      case isTrue => exact h₄.rec
+      case isFalse h₅ =>
+        unfold bind Monad.toBind Except.instMonad Except.bind at h₄
+        simp at h₄
+        split at h₄; contradiction
+        case h_2 d3 t ht =>
+          clear d3
+          split at h₄
+          case isTrue h₆ =>
+            split at h₄; exact h₄.rec
+            case isFalse h₇ =>
+              have h₈ : (previous.fields.push t)[previous.width * (previous.height - 1) + pos]! = t := by
+                have := Array.get_push_eq previous.fields t
+                simp[h₂, Array.getElem!_eq_getElem] at this
+                assumption
+              have : t = Tile.start := (beq_iff_eq t Tile.start).mp h₆
+              subst t
+              have : previous.width * (previous.height - 1) + pos < previous.width * previous.height := by
+                have := Nat.mul_pred previous.width previous.height
+                simp only [Nat.pred_eq_sub_one] at this
+                rw[this]
+                have : previous.width ≤ previous.width*previous.height := Nat.le_mul_of_pos_right _ h₁
+                rw[←Nat.sub_add_comm this]
+                omega
+              have h₉ := Area.ParseLine_only_adds_to_fields { width := previous.width, height := previous.height, start := some ⟨previous.width * (previous.height - 1) + pos, this⟩, fields := previous.fields.push Tile.start } (pos + 1) (line.drop 1) h₁ h₄ ⟨previous.width * (previous.height - 1) + pos, (by simp_all)⟩
+              simp at h₉
+              have h₁₀ := Area.ParseLine_leaves_start_if_some { width := previous.width, height := previous.height, start := some ⟨previous.width * (previous.height - 1) + pos, this⟩, fields := previous.fields.push Tile.start } (pos + 1) (line.drop 1) h₁ h₄ rfl
+              simp[hindex] at h₁₀
+              simp[←h₁₀] at h₉ h₈
+              simp[←h₉]
+              assumption
+          case isFalse =>
+            have : (previous.fields.push t).size = previous.width * (previous.height - 1) + (pos + 1) := by simp_arith[h₂]
+            have h₆ := Area.ParseLine_start_at_tile { width := previous.width, height := previous.height, start := previous.start, fields := previous.fields.push t } (pos + 1) (line.drop 1) h₁ this h₃ h₄
+            simp[hindex] at h₆
+            assumption
+termination_by previous.width - pos
 
 private theorem Area.ParseLines_start_position (input : Area.Raw) (lines : List String) (h₁ : (Area.parseLines input lines).isOk) (h₀ : input.fields.size = input.width * input.height) (h₂ : match input.start with | .some i => input.fields[i]! = Tile.start | .none => True) :
   match (Except.get (Area.parseLines input lines) h₁).start with
@@ -400,7 +530,9 @@ private theorem Area.ParseLines_start_position (input : Area.Raw) (lines : List
                   rw[hlo₂.right]
                   exact h₂
               case none =>
-                sorry
+                have h₆ := Area.ParseLine_start_at_tile { width := input.width, height := input.height + 1, start := Option.map (Fin.castLE (Nat.mul_le_succ_right _ _)) input.start, fields := input.fields } 0 l.toSubstring (Nat.succ_pos _) h₀ (by simp[his]) h₃
+                simp[ho] at h₆
+                assumption
             rw[←h₅ this]
             rfl
 
@@ -426,7 +558,7 @@ private theorem Area.ParseRaw_start_position_aux :
       case isFalse => rw[←hr] at h₁; contradiction
       case isTrue =>
         rename_i hs _
-        have : 0 < (String.splitTrim (fun x => x == '\n') input).length := by simp at hs; unfold List.isEmpty at hs; split at hs; contradiction; rename_i hx; simp[hx]
+        have : 0 < (String.splitTrim (fun x => x == '\n') input).length := by let hs := List.isEmpty_eq_false.mpr hs; unfold List.isEmpty at hs; split at hs; contradiction; rename_i hx; simp[hx]
         have := Area.ParseLines_start_position { width := (String.splitTrim (fun x => x == '\n') input)[0].length, height := 0, start := none, fields := #[] } (String.splitTrim (fun x => x == '\n') input) (hr.substr h₁)
         simp at this
         subst r
@@ -438,14 +570,6 @@ private theorem Area.ParseRaw_start_position_aux :
           subst index₂
           exact this
 
-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
-  split
-  <;> rename_i blah
-  <;> simp[h] at blah
-  assumption
-
 private theorem Area.ParseRaw_start_position :
   ∀ (input : String), (h₁ : (Area.parseRaw input).isOk) → (h₂ : (Except.get (Area.parseRaw input) h₁).start.isSome) → (Except.get (Area.parseRaw input) h₁).fields[(Except.get (Area.parseRaw input) h₁).start.get h₂]'((Area.ParseRaw_array_size input h₁).substr ((Except.get (Area.parseRaw input) h₁).start.get h₂).isLt) = Tile.start := by
   intros input h₁ h₂
diff --git a/lakefile.lean b/lakefile.lean
index 212cf0e..e659681 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -25,4 +25,4 @@ lean_exe «aoc-2023» where
   supportInterpreter := true
 
 require BinaryHeap from git
-  "https://github.com/soulsource/BinaryHeap"@"v0.1.0"
+  "https://github.com/soulsource/BinaryHeap"@"v0.1.1"
diff --git a/lean-toolchain b/lean-toolchain
index a020eb9..7beb578 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.10.0
+leanprover/lean4:4.11.0