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