Theorem: Regex.VM.captureNext_spec.go
Proof state before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
next atEnd =>
  split at h
  next h' =>
    subst h
    exact eqs ▸ inv.acceptOfLastMatch
  next =>
    if hm : lastMatch.isNone then
      generalize he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored at h
      let (_, current', saveSlots') := explored
      simp [hm] at h
      have mem_current'_iff := exploreεClosure_spec.mem_next_iff he inv.currentClosure
      generalize hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped at h
      let (matched', next', saveSlots'') := stepped
      simp at h
      have currentPath'  (k : Fin nfa.nodes.size) (hk : k ∈ next') :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
        have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
        have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
        cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
        | inl mem_current =>
          have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
          have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
          subst hr
          exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
        | inr cls' =>
          have ⟨l, r, iv⟩ := v.validFor
          have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
          subst hr
          let startPos : String.Pos := ⟨String.utf8Len l⟩
          refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
          . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
          . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
          . have prev : nfa.reaches current'[i] [] := .nil cls'
            exact prev.snoc step cls
      have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
        cases matched' with
        | none =>
          simp at h
          exact eqs ▸ inv.acceptOfLastMatch h
        | some =>
          have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
          have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
          have eqs' := iv.toString
          simp [String.Iterator.next, List.reverseAux_eq] at eqs'
          exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
      have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
        ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
      exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
    else
      simp [hm] at h
      generalize hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped at h
      let (matched', next', saveSlots'') := stepped
      simp at h
      have currentPath' (k : Fin nfa.nodes.size) (hk : k ∈ next') :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
        have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
        have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
        have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current[i] (SparseSet.mem_get isLt)
        have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
        subst hr
        exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
      have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
        cases matched' with
        | none =>
          simp at h
          exact eqs ▸ inv.acceptOfLastMatch h
        | some =>
          have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
          have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
          have eqs' := iv.toString
          simp [String.Iterator.next, List.reverseAux_eq] at eqs'
          exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
      have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
        ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
      exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
Proof state after:
no goals