Refactor path equivalence proofs

Author: pandaman64

correctness/RegexCorrectness/NFA/Semantics/Equivalence/CapturesOfPath.lean

@@ -23,46 +23,11 @@ theorem captures_of_path.group {tag} (eq : nfa.pushRegex next (.group tag e) = r
   ∃ groups, EquivUpdate groups update ∧ (Expr.group tag e).Captures pos pos' groups := by
   open Compile.ProofData Group in
   let pd := Group.intro eq
-  simp [pd.eq_result eq] at path
-
-  cases path with
-  | last step =>
-    have ⟨eqnext, _, _⟩ := step_start_iff.mp step
-    have ge := ge_pushRegex_start (result := nfaExpr) rfl
-    simp [←eqnext, nfaClose] at ge
-    have : next < pd.nfa.size := next_lt
-    omega
-  | @more i pos j posm k pos'' update updates step rest  =>
-    have ⟨hj, hpos, hupdate⟩ := step_start_iff.mp step
-    simp [hupdate]
-    simp [hj, hpos] at rest
-
-    have rest := castToExpr wf next_lt rest
-    have next_lt_close : next < nfaClose.size := by
-      simp [nfaClose]
-      exact Nat.lt_trans next_lt (Nat.lt_add_one _)
-    have ge_expr_start : nfaClose.size ≤ nfaExpr.start := ge_pushRegex_start rfl
-    have ne_next : next ≠ nfaClose.start := by
-      simp [nfaClose]
-      exact Nat.ne_of_lt next_lt
-    have ⟨posm, updateExpr, updateClose, equ, pathExpr, pathClose⟩ :=
-      rest.path_next_of_ne (result := nfaExpr) rfl next_lt_close ge_expr_start ne_next
-
-    have wfClose := wfClose wf next_lt
-    have ⟨groupExpr, eqv, c⟩ := ih (result := nfaExpr) rfl wfClose wfClose.start_lt pathExpr
-
-    have : nfaExpr[nfaClose.start]'(by grind) = nfa'[nfaClose.start]'(by grind) := by
-      grind
-    cases pathClose with
-    | last step =>
-      have ⟨_, hpos, hupdate⟩ := step_close_iff.mp (step.cast this)
-      rw [←hpos] at c
-      simp [equ, hupdate, ←hpos]
-      exact ⟨.group tag pos pos' groupExpr, .group eqv, .group c⟩
-    | more step rest =>
-      have ⟨hj, _, _⟩ := step_close_iff.mp (step.cast this)
-      have : nfa.size ≤ next := show nfa.size ≤ pd.next from hj ▸ rest.ge
-      omega
+  simp only [pd.eq_result eq] at path
+  obtain ⟨updates, rfl, pathExpr⟩ := (pd.path_start_iff wf next_lt).mp path
+  have wfClose := pd.wfClose wf next_lt
+  have ⟨groups, eqv, c⟩ := ih rfl wfClose wfClose.start_lt pathExpr
+  exact ⟨.group tag pos pos' groups, .group eqv, .group c⟩
 
 theorem captures_of_path.alternate {e₁ e₂} (eq : nfa.pushRegex next (.alternate e₁ e₂) = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -80,39 +45,16 @@ theorem captures_of_path.alternate {e₁ e₂} (eq : nfa.pushRegex next (.altern
   ∃ groups, EquivUpdate groups update ∧ (Expr.alternate e₁ e₂).Captures pos pos' groups := by
   open Compile.ProofData Alternate in
   let pd := Alternate.intro eq
-  simp [pd.eq_result eq] at path
-
+  simp only [pd.eq_result eq] at path
+  obtain path := (pd.path_start_iff wf next_lt).mp path
   cases path with
-  | last step =>
-    have := step_start_iff.mp step
-    have : next < nfa₁.start := Nat.lt_of_lt_of_le next_lt (ge_pushRegex_start rfl)
-    have : next < nfa₂.start := Nat.lt_of_lt_of_le (Nat.lt_trans next_lt nfa₁_property) (ge_pushRegex_start rfl)
-    omega
-  | @more i pos j posm k pos'' update updates step rest =>
-    have ⟨hj, hpos, hupdate⟩ := step_start_iff.mp step
-    simp [hupdate]
-    cases hj with
-    | inl hj =>
-      simp [hj, hpos] at rest
-      have rest := castTo₁ wf next_lt rest
-      have ⟨groups, eqv, c⟩ := ih₁ rfl wf next_lt rest
-      exact ⟨groups, eqv, .alternateLeft c⟩
-    | inr hj =>
-      simp [hj, hpos] at rest
-
-      have rest := castTo₂ wf next_lt rest
-      have rest : nfa₂.Path nfa₁.size nfa₂.start pos next pos' updates := by
-        apply rest.liftBound' (ge_pushRegex_start rfl)
-        intro i pos j pos' update gei gej step
-        cases (step.liftBound' gei).eq_or_ge_of_pushRegex with
-        | inl eq =>
-          have : nfa.size ≤ next := show nfa.size ≤ pd.next from eq ▸ gej
-          omega
-        | inr ge => exact ge
-
-      have wf₁ := wf₁ wf next_lt
-      have ⟨groups, eqv, c⟩ := ih₂ rfl wf₁ (Nat.lt_trans next_lt nfa₁_property) rest
-      exact ⟨groups, eqv, .alternateRight c⟩
+  | inl path₁ =>
+    have ⟨groups, eqv, c⟩ := ih₁ rfl wf next_lt path₁
+    exact ⟨groups, eqv, .alternateLeft c⟩
+  | inr path₂ =>
+    have wf₁ := wf₁ wf next_lt
+    have ⟨groups, eqv, c⟩ := ih₂ rfl wf₁ (by grind) path₂
+    exact ⟨groups, eqv, .alternateRight c⟩
 
 theorem captures_of_path.concat {e₁ e₂} (eq : nfa.pushRegex next (.concat e₁ e₂) = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -130,19 +72,15 @@ theorem captures_of_path.concat {e₁ e₂} (eq : nfa.pushRegex next (.concat e
   ∃ groups, EquivUpdate groups update ∧ (Expr.concat e₁ e₂).Captures pos pos' groups := by
   open Compile.ProofData Concat in
   let pd := Concat.intro eq
-  simp [pd.eq_result eq] at path
-  have next_lt₂ : next < nfa₂.size := Nat.lt_trans next_lt nfa₂_property
-  have ge_start : nfa₂.size ≤ nfa'.start := ge_pushRegex_start rfl
-  have ne_next : next ≠ nfa₂.start := Nat.ne_of_lt (Nat.lt_of_lt_of_le next_lt (ge_pushRegex_start rfl))
-  have ⟨itm, update₁, update₂, equ, path₁, path₂⟩ := path.path_next_of_ne rfl next_lt₂ ge_start ne_next
-
+  simp only [pd.eq_result eq] at path
+  obtain ⟨pm, updates₁, updates₂, rfl, path₁, path₂⟩ := (pd.path_start_iff wf next_lt).mp path
   have wf₂ := wf₂ wf next_lt
-  have ⟨group₁, eqv₁, c₁⟩ := ih₁ rfl wf₂ wf₂.start_lt path₁
-  have ⟨group₂, eqv₂, c₂⟩ := ih₂ rfl wf next_lt (castTo₂ wf next_lt path₂)
-  exact ⟨.concat group₁ group₂, equ ▸ .concat eqv₁ eqv₂, .concat c₁ c₂⟩
+  have ⟨groups₁, eqv₁, c₁⟩ := ih₁ rfl wf₂ wf₂.start_lt path₁
+  have ⟨groups₂, eqv₂, c₂⟩ := ih₂ rfl wf next_lt path₂
+  exact ⟨.concat groups₁ groups₂, .concat eqv₁ eqv₂, .concat c₁ c₂⟩
 
 open Compile.ProofData Star in
-theorem captures_of_path.star_of_loop [Star] {greedy} (loop : Loop pos pos' update)
+theorem captures_of_path.star_of_loop [Star] {greedy : Bool} (loop : Loop pos pos' update)
   (ih : ∀ {pos pos' : Pos s} {update},
     nfa'.Path nfaPlaceholder.size nfaExpr.start pos nfaPlaceholder.start pos' update →
     ∃ groups, EquivUpdate groups update ∧ e.Captures pos pos' groups) :
@@ -165,23 +103,20 @@ theorem captures_of_path.star {greedy e} (eq : nfa.pushRegex next (.star greedy
   ∃ groups, EquivUpdate groups update ∧ (Expr.star greedy e).Captures pos pos' groups := by
   open Compile.ProofData Star in
   let pd := Star.intro eq
-  simp [pd.eq_result eq] at path
-  cases path with
-  | last step =>
-    obtain ⟨_, rfl, rfl⟩ := step_start_iff.mp step
+  simp only [pd.eq_result eq] at path
+  have h := (pd.path_start_iff next_lt).mp path
+  match h with
+  | .inl ⟨hp, hupdate⟩ =>
+    subst pos' update
     exact ⟨.empty, .empty, .starEpsilon⟩
-  | @more _ _ i pos'' _ _ _ updates step rest =>
-    obtain ⟨eqi, rfl, rfl⟩ := step_start_iff.mp step
-    cases eqi with
-    | inl eqi =>
-      have loop := Loop.intro wf next_lt (eqi ▸ rest)
-      apply captures_of_path.star_of_loop (greedy := greedy) loop
+  | .inr path =>
+    have loop := Loop.intro wf next_lt path
+    apply captures_of_path.star_of_loop loop
 
-      intro pos pos' update path
-      have path := castToExpr wf path
-      have wfPlaceholder := wfPlaceholder wf
-      exact ih (by grind) wfPlaceholder wfPlaceholder.start_lt path
-    | inr eqi => grind
+    intro pos pos' update path
+    have path := castToExpr wf path
+    have wfPlaceholder := wfPlaceholder wf
+    exact ih (by grind) wfPlaceholder wfPlaceholder.start_lt path
 
 public theorem captures_of_path (eq : nfa.pushRegex next e = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -191,27 +126,27 @@ public theorem captures_of_path (eq : nfa.pushRegex next e = result)
   induction e generalizing nfa next result pos pos' update with
   | empty =>
     let pd := Empty.intro eq
-    simp [pd.eq_result eq] at path
+    simp only [pd.eq_result eq] at path
     exact absurd path pd.not_path_start
   | epsilon =>
     let pd := Epsilon.intro eq
-    simp [pd.eq_result eq] at path
+    simp only [pd.eq_result eq] at path
     have := (pd.path_start_iff next_lt).mp path
     simp [this]
     exact ⟨.empty, .empty, .epsilon⟩
   | anchor a =>
     let pd := Anchor.intro eq
-    simp [pd.eq_result eq] at path
+    simp only [pd.eq_result eq] at path
     obtain ⟨_, rfl, rfl, test⟩:= (pd.path_start_iff next_lt).mp path
     exact ⟨.empty, .empty, .anchor test⟩
   | char c =>
     let pd := Char.intro eq
-    simp [pd.eq_result eq] at path
+    simp only [pd.eq_result eq] at path
     obtain ⟨_, rfl, ne, rfl, rfl⟩ := (pd.path_start_iff next_lt).mp path
     exact ⟨.empty, .empty, .char ne rfl⟩
   | classes cs =>
     let pd := Classes.intro eq
-    simp [pd.eq_result eq] at path
+    simp only [pd.eq_result eq] at path
     obtain ⟨_, rfl, ne, rfl, mem⟩ := (pd.path_start_iff next_lt).mp path
     exact ⟨.empty, .empty, .sparse ne mem⟩
   | group tag e ih => exact captures_of_path.group eq wf next_lt path ih

correctness/RegexCorrectness/NFA/Semantics/Equivalence/PathOfCaptures.lean

@@ -21,24 +21,15 @@ theorem path_of_captures.group {tag} (eq : nfa.pushRegex next (.group tag e) = r
   ∃ update, EquivUpdate (.group tag pos pos' groups) update ∧ result.Path nfa.size result.start pos next pos' update := by
   open Compile.ProofData Group in
   let pd := Group.intro eq
-  simp [eq_result eq]
+  simp only [eq_result eq]
 
   have wfClose := wfClose wf next_lt
-  have ⟨update, eqv, path⟩ := ih (result := nfaExpr) rfl wfClose wfClose.start_lt
-  exists (2 * tag, pos) :: update ++ [(2 * tag + 1, pos')], .group eqv
-
-  have stepOpen : nfa'.Step nfa.size nfa'.start pos nfaExpr.start pos (.some (2 * tag, pos)) := by
-    apply step_start_iff.mpr
-    exact ⟨rfl, rfl, rfl⟩
-  have path := castFromExpr path
-  have path : nfa'.Path nfa.size nfaExpr.start pos nfaClose.start pos' update :=
-    path.liftBound (by simp [Group.nfaClose]; exact Nat.le_succ _)
-  have pathClose : nfa'.Path nfa.size nfaClose.start pos' next pos' [(2 * tag + 1, pos')] := by
-    have stepClose : nfa'.Step nfa.size nfaClose.start pos' next pos' (.some (2 * tag + 1, pos')) := by
-      apply step_close_iff.mpr
-      exact ⟨rfl, rfl, rfl⟩
-    exact .last stepClose
-  exact .more stepOpen (path.trans pathClose)
+  have ⟨updates, eqv, path⟩ := ih (show nfaClose.pushRegex nfaClose.start e' = nfaExpr from rfl) wfClose wfClose.start_lt
+  exact ⟨
+    (2 * tag, pos) :: updates ++ [(2 * tag + 1, pos')],
+    .group eqv,
+    (pd.path_start_iff wf next_lt).mpr (by grind)
+  ⟩
 
 theorem path_of_captures.alternateLeft {e₁ e₂} (eq : nfa.pushRegex next (.alternate e₁ e₂) = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -49,16 +40,10 @@ theorem path_of_captures.alternateLeft {e₁ e₂} (eq : nfa.pushRegex next (.al
   ∃ update, EquivUpdate groups update ∧ result.Path nfa.size result.start pos next pos' update := by
   open Compile.ProofData Alternate in
   let pd := Alternate.intro eq
-  simp [eq_result eq]
+  simp only [eq_result eq]
 
-  have ⟨update, eqv, path⟩ := ih (result := nfa₁) rfl wf next_lt
-  exists update, eqv
-
-  have step : nfa'.Step nfa.size nfa'.start pos nfa₁.start pos .none := by
-    apply step_start_iff.mpr
-    simp
-  have path := castFrom₁ path
-  exact .more step path
+  have ⟨update, eqv, path⟩ := ih (show nfa.pushRegex next e₁ = nfa₁ from rfl) wf next_lt
+  exact ⟨update, eqv, (pd.path_start_iff wf next_lt).mpr (by grind)⟩
 
 theorem path_of_captures.alternateRight {e₁ e₂} (eq : nfa.pushRegex next (.alternate e₁ e₂) = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -69,17 +54,11 @@ theorem path_of_captures.alternateRight {e₁ e₂} (eq : nfa.pushRegex next (.a
   ∃ update, EquivUpdate groups update ∧ result.Path nfa.size result.start pos next pos' update := by
   open Compile.ProofData Alternate in
   let pd := Alternate.intro eq
-  simp [eq_result eq]
+  simp only [eq_result eq]
 
   have wf₁ := wf₁ wf next_lt
-  have ⟨update, eqv, path⟩ := ih (result := nfa₂) rfl wf₁ (Nat.lt_trans next_lt nfa₁_property)
-  exists update, eqv
-
-  have step : nfa'.Step nfa.size nfa'.start pos nfa₂.start pos .none := by
-    apply step_start_iff.mpr
-    simp
-  have path := castFrom₂ (path.liftBound (Nat.le_of_lt nfa₁_property))
-  exact .more step path
+  have ⟨update, eqv, path⟩ := ih (show nfa₁.pushRegex next e₂ = nfa₂ from rfl) wf₁ (Nat.lt_trans next_lt nfa₁_property)
+  exact ⟨update, eqv, (pd.path_start_iff wf next_lt).mpr (by grind)⟩
 
 theorem path_of_captures.concat {pos'' e₁ e₂ groups₁ groups₂} (eq : nfa.pushRegex next (.concat e₁ e₂) = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -94,15 +73,12 @@ theorem path_of_captures.concat {pos'' e₁ e₂ groups₁ groups₂} (eq : nfa.
   ∃ update, EquivUpdate (.concat groups₁ groups₂) update ∧ result.Path nfa.size result.start pos next pos'' update := by
   open Compile.ProofData Concat in
   let pd := Concat.intro eq
-  simp [pd.eq_result eq]
+  simp only [pd.eq_result eq]
 
   have wf₂ := wf₂ wf next_lt
   have ⟨update₁, eqv₁, path₁⟩ := ih₁ eq_push.symm wf₂ wf₂.start_lt
-  have ⟨update₂, eqv₂, path₂⟩ := ih₂ (result := nfa₂) rfl wf next_lt
-  exists update₁ ++ update₂, .concat eqv₁ eqv₂
-
-  have path₂ := castFrom₂ path₂
-  exact (path₁.liftBound (Nat.le_of_lt nfa₂_property)).trans path₂
+  have ⟨update₂, eqv₂, path₂⟩ := ih₂ (show nfa.pushRegex next e₂ = nfa₂ from rfl) wf next_lt
+  exact ⟨update₁ ++ update₂, .concat eqv₁ eqv₂, (pd.path_start_iff wf next_lt).mpr (by grind)⟩
 
 theorem path_of_captures.starConcat {pos'' greedy e groups₁ groups₂} (eq : nfa.pushRegex next (.star greedy e) = result)
   (wf : nfa.WellFormed) (next_lt : next < nfa.size)
@@ -117,24 +93,19 @@ theorem path_of_captures.starConcat {pos'' greedy e groups₁ groups₂} (eq : n
   ∃ update, EquivUpdate (.concat groups₁ groups₂) update ∧ result.Path nfa.size result.start pos next pos'' update := by
   open Compile.ProofData Star in
   let pd := Star.intro eq
-  simp [pd.eq_result eq]
+  simp only [pd.eq_result eq]
 
   have wfPlaceholder := wfPlaceholder wf
-  have ⟨update₁, eqv₁, path₁⟩ := ih₁ (result := nfaExpr) (by grind only [= nfaPlaceholder,
-    = Star.intro, = nfaExpr, = pushNode_start]) wfPlaceholder wfPlaceholder.start_lt
-  have ⟨update₂, eqv₂, path₂⟩ := ih₂ (result := nfa') rfl wf next_lt
-  exists update₁ ++ update₂, .concat eqv₁ eqv₂
-
-  have wf' : nfa'.WellFormed := pushRegex_wf wf next_lt
-
-  have path₁ : nfa'.Path nfa.size nfaExpr.start pos nfaPlaceholder.start pos' update₁ :=
-    (castFromExpr path₁).liftBound (by grind only [nfaPlaceholder, Star.intro, = pushNode_size])
-  have step : nfa'.Step nfa.size nfa'.start pos nfaExpr.start pos .none :=
-    step_start_iff.mpr ⟨.inl rfl, rfl, rfl⟩
-  have path₁ : nfa'.Path nfa.size nfa'.start pos nfaPlaceholder.start pos' update₁ :=
-    .more step path₁
-
-  have path₂ : nfa'.Path nfa.size nfaPlaceholder.start pos' next pos'' update₂ := by
+  have ⟨updates₁, eqv₁, path₁⟩ :=
+    ih₁ (show nfaPlaceholder.pushRegex nfaPlaceholder.start e = nfaExpr by grind) wfPlaceholder wfPlaceholder.start_lt
+  have ⟨updates₂, eqv₂, path₂⟩ := ih₂ (show nfa.pushRegex next (.star greedy e) = nfa' from rfl) wf next_lt
+  exists updates₁ ++ updates₂, .concat eqv₁ eqv₂
+  apply (pd.path_start_iff next_lt).mpr (.inr ?_)
+
+  have path₁ : nfa'.Path nfa.size nfaExpr.start pos nfaPlaceholder.start pos' updates₁ :=
+    (castFromExpr path₁).liftBound (by grind)
+  have path₂ : nfa'.Path nfa.size nfaPlaceholder.start pos' next pos'' updates₂ := by
+    have wf' : nfa'.WellFormed := pushRegex_wf wf next_lt
     apply path₂.castHead
     . simp [pd.get_placeholder_start, pd.get_start]
     . grind only [nfaPlaceholder, Star.intro, = start.eq_1, = pushNode_start]
@@ -152,25 +123,25 @@ public theorem path_of_captures (eq : nfa.pushRegex next e = result)
   | char ne hc =>
     let pd := Char.intro eq
     exists [], .empty
-    simp [pd.eq_result eq]
+    simp only [pd.eq_result eq]
     apply (pd.path_start_iff next_lt).mpr
     exact ⟨rfl, rfl, ne, rfl, hc⟩
   | sparse ne mem =>
     let pd := Classes.intro eq
     exists [], .empty
-    simp [pd.eq_result eq]
+    simp only [pd.eq_result eq]
     apply (pd.path_start_iff next_lt).mpr
     exact ⟨rfl, rfl, ne, rfl, mem⟩
   | epsilon =>
     let pd := Epsilon.intro eq
     exists [], .empty
-    simp [pd.eq_result eq]
+    simp only [pd.eq_result eq]
     apply (pd.path_start_iff next_lt).mpr
     trivial
   | anchor h =>
     let pd := Anchor.intro eq
     exists [], .empty
-    simp [pd.eq_result eq]
+    simp only [pd.eq_result eq]
     apply (pd.path_start_iff next_lt).mpr
     trivial
   | group c ih => exact path_of_captures.group eq wf next_lt ih
@@ -180,12 +151,8 @@ public theorem path_of_captures (eq : nfa.pushRegex next e = result)
   | @starEpsilon pos _ _ =>
     let pd := Star.intro eq
     exists [], .empty
-    simp [pd.eq_result eq]
-
-    have step : nfa'.Step nfa.size nfa'.start pos next pos .none := by
-      apply (pd.step_start_iff).mpr
-      exact ⟨.inr rfl, rfl, rfl⟩
-    exact .last step
+    simp only [pd.eq_result eq]
+    exact (pd.path_start_iff next_lt).mpr (.inl ⟨rfl, rfl⟩)
   | starConcat c₁ _ ih₁ ih₂ => exact path_of_captures.starConcat eq wf next_lt ih₁ ih₂
 
 public theorem path_of_captures_compile (eq : compile e = nfa) (c : e.Captures pos pos' groups) :