Theorem: Regex.VM.captureNext_spec.go
Proof state before:
case some
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
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.next.s = { data := (m.reverse ++ l.reverse).reverseAux r }
⊢ ∃ 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:
simp [String.Iterator.next, List.reverseAux_eq] at eqs'
Proof state after:
case some
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
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done