def
Regex.VM.MatchedInv
(nfa : NFA)
(wf : nfa.WellFormed)
(it₀ : String.Iterator)
(matched : Option (List (ℕ × String.Pos)))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Regex.VM.captureNext.go.inv
{nfa : NFA}
{wf : nfa.WellFormed}
{it₀ it : String.Iterator}
{matched : Option HistoryStrategy.Update}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option HistoryStrategy.Update}
(h : go HistoryStrategy nfa wf it matched current next = matched')
(v : it.Valid)
(eqs : it.toString = it₀.toString)
(le : it₀.pos ≤ it.pos)
(curr_inv : SearchState.Inv nfa wf it₀ it current)
(empty : next.states.isEmpty = true)
(matched_inv : MatchedInv nfa wf it₀ matched)
:
MatchedInv nfa wf it₀ matched'
theorem
Regex.VM.captureNext.path_done_of_matched
{nfa : NFA}
{wf : nfa.WellFormed}
{it₀ : String.Iterator}
{matched' : Option HistoryStrategy.Update}
(h : captureNext HistoryStrategy nfa wf it₀ = matched')
(v : it₀.Valid)
(isSome' : matched'.isSome = true)
:
If captureNext returns some, the returned list corresponds to the updates of a path from
nfa.start to a .done state.
theorem
Regex.VM.SearchState.NotDoneInv.preserves
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
(stepped expanded : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h₁ : eachStepChar HistoryStrategy nfa wf it current next = stepped)
(h₂ : εClosure HistoryStrategy nfa wf it.next none stepped.2 [([], ⟨nfa.start, ⋯⟩)] = expanded)
(isNone₁ : stepped.1 = none)
(isNone₂ : expanded.1 = none)
(invCurrent : NotDoneInv HistoryStrategy nfa current)
(invNext : NotDoneInv HistoryStrategy nfa next)
:
NotDoneInv HistoryStrategy nfa expanded.2
theorem
Regex.VM.SearchState.MemOfPathInv.preserves
{nfa : NFA}
{wf : nfa.WellFormed}
{it₀ it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
(stepped expanded : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h₁ : eachStepChar HistoryStrategy nfa wf it current next = stepped)
(h₂ : εClosure HistoryStrategy nfa wf it.next none stepped.2 [([], ⟨nfa.start, ⋯⟩)] = expanded)
(isNone : stepped.1 = none)
(v : it.Valid)
(ndinv : NotDoneInv HistoryStrategy nfa current)
(lb : εClosure.LowerBound it.next next.states)
(inv : MemOfPathInv nfa wf it₀ it current)
:
MemOfPathInv nfa wf it₀ it.next expanded.2
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Regex.VM.NeDoneOfPathInv.preserves
{nfa : NFA}
{wf : nfa.WellFormed}
{it₀ it : String.Iterator}
{expanded : Option (List (ℕ × String.Pos)) × SearchState HistoryStrategy nfa}
(eqs : it.toString = it₀.toString)
(v : it.Valid)
(notDone : SearchState.NotDoneInv HistoryStrategy nfa expanded.2)
(memOfPath : SearchState.MemOfPathInv nfa wf it₀ it.next expanded.2)
(inv : NeDoneOfPathInv nfa wf it₀ it)
:
NeDoneOfPathInv nfa wf it₀ it.next
theorem
Regex.VM.captureNext.go.some_of_some
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{matched : Option HistoryStrategy.Update}
{current next : SearchState HistoryStrategy nfa}
(result : Option HistoryStrategy.Update)
(h : go HistoryStrategy nfa wf it matched current next = result)
(isSome : matched.isSome = true)
:
theorem
Regex.VM.captureNext.go.ne_done_of_path_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it₀ it : String.Iterator}
{matched : Option HistoryStrategy.Update}
{current next : SearchState HistoryStrategy nfa}
(h : go HistoryStrategy nfa wf it matched current next = none)
(eqs : it.toString = it₀.toString)
(v : it.Valid)
(isEmpty : next.states.isEmpty = true)
(ndinv : SearchState.NotDoneInv HistoryStrategy nfa current)
(mopInv : SearchState.MemOfPathInv nfa wf it₀ it current)
(inv : NeDoneOfPathInv nfa wf it₀ it)
(it' : String.Iterator)
(state : Fin nfa.nodes.size)
(update : List (ℕ × String.Pos))
:
nfa.VMPath wf it₀ it' state update → nfa[state] ≠ NFA.Node.done
theorem
Regex.VM.captureNext.ne_done_of_path_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
(h : captureNext HistoryStrategy nfa wf it = none)
(v : it.Valid)
(it' : String.Iterator)
(state : Fin nfa.nodes.size)
(update : List (ℕ × String.Pos))
:
nfa.VMPath wf it it' state update → nfa[state] ≠ NFA.Node.done
If captureNext returns .none, then there is no path from nfa.start to a .done state after it.