theorem
Regex.VM.stepChar.subset
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{state : Fin nfa.nodes.size}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
(h : stepChar HistoryStrategy nfa wf it currentUpdates next state = (matched', next'))
:
theorem
Regex.VM.stepChar.lower_bound
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{state : Fin nfa.nodes.size}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
(h : stepChar HistoryStrategy nfa wf it currentUpdates next state = (matched', next'))
(lb : εClosure.LowerBound it.next next.states)
:
εClosure.LowerBound it.next next'.states
theorem
Regex.VM.stepChar.eq_updates_of_mem_next
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{i k : Fin nfa.nodes.size}
(h : stepChar HistoryStrategy nfa wf it currentUpdates next i = (matched', next'))
(mem : k ∈ next.states)
:
theorem
Regex.VM.stepChar.done_of_matched_some
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{state : Fin nfa.nodes.size}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
(h : stepChar HistoryStrategy nfa wf it currentUpdates next state = (matched', next'))
(isSome' : matched'.isSome = true)
:
theorem
Regex.VM.stepChar.mem_next_of_stepChar
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{i j k : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(h : stepChar HistoryStrategy nfa wf it currentUpdates next i = (matched', next'))
(lb : εClosure.LowerBound it.next next.states)
(step : nfa.CharStep it i j)
(cls : nfa.εClosure' it.next j k update)
:
theorem
Regex.VM.stepChar.write_updates_of_mem_next
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{i k : Fin nfa.nodes.size}
(h : stepChar HistoryStrategy nfa wf it currentUpdates next i = (matched', next'))
(v : it.Valid)
(notEnd : ¬it.atEnd = true)
(mem : k ∈ next'.states)
:
theorem
Regex.VM.stepChar.inv
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{it₀ : String.Iterator}
{idx : ℕ}
(hlt : idx < current.states.count)
(h : stepChar HistoryStrategy nfa wf it current.updates next current.states[idx] = (matched', next'))
(v : it.Valid)
(notEnd : ¬it.atEnd = true)
(invCurrent : SearchState.Inv nfa wf it₀ it current)
(invNext : SearchState.Inv nfa wf it₀ it.next next)
:
SearchState.Inv nfa wf it₀ it.next next'
theorem
Regex.VM.stepChar.not_done_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{currentUpdates : Vector (List (ℕ × String.Pos)) nfa.nodes.size}
{next : SearchState HistoryStrategy nfa}
{state : Fin nfa.nodes.size}
(result : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : stepChar HistoryStrategy nfa wf it currentUpdates next state = result)
(isNone : result.1 = none)
(inv : SearchState.NotDoneInv HistoryStrategy nfa next)
:
SearchState.NotDoneInv HistoryStrategy nfa result.2
theorem
Regex.VM.eachStepChar.go.lower_bound
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{idx : ℕ}
{hle : idx ≤ current.states.count}
(h : go HistoryStrategy nfa wf it current idx hle next = (matched', next'))
(lb : εClosure.LowerBound it.next next.states)
:
εClosure.LowerBound it.next next'.states
theorem
Regex.VM.eachStepChar.go.done_of_matched_some
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{idx : ℕ}
{hle : idx ≤ current.states.count}
(h : go HistoryStrategy nfa wf it current idx hle next = (matched', next'))
(isSome' : matched'.isSome = true)
:
theorem
Regex.VM.eachStepChar.go.inv
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{it₀ : String.Iterator}
{idx : ℕ}
{hle : idx ≤ current.states.count}
(h : go HistoryStrategy nfa wf it current idx hle next = (matched', next'))
(v : it.Valid)
(notEnd : ¬it.atEnd = true)
(invCurrent : SearchState.Inv nfa wf it₀ it current)
(invNext : SearchState.Inv nfa wf it₀ it.next next)
:
SearchState.Inv nfa wf it₀ it.next next'
theorem
Regex.VM.eachStepChar.go.not_done_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{idx : ℕ}
{hle : idx ≤ current.states.count}
(result : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : go HistoryStrategy nfa wf it current idx hle next = result)
(isNone : result.1 = none)
(invCurrent : SearchState.NotDoneInv HistoryStrategy nfa current)
(invNext : SearchState.NotDoneInv HistoryStrategy nfa next)
:
SearchState.NotDoneInv HistoryStrategy nfa result.2
theorem
Regex.VM.eachStepChar.go.subset
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
{idx : ℕ}
{hle : idx ≤ current.states.count}
(h : go HistoryStrategy nfa wf it current idx hle next = (matched', next'))
:
theorem
Regex.VM.eachStepChar.go.mem_of_step_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{idx : ℕ}
{hle : idx ≤ current.states.count}
(result : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : go HistoryStrategy nfa wf it current idx hle next = result)
(isNone : result.1 = none)
(notDone : SearchState.NotDoneInv HistoryStrategy nfa current)
(lb : εClosure.LowerBound it.next next.states)
(inv :
∀ (i : ℕ) (state' state'' : Fin nfa.nodes.size) (update : List (ℕ × String.Pos)) (x : i < current.states.count),
i < idx →
nfa.CharStep it current.states[i] state' →
nfa.εClosure' it.next state' state'' update → state'' ∈ result.2.states)
(state state' state'' : Fin nfa.nodes.size)
(update : List (ℕ × String.Pos))
:
theorem
Regex.VM.eachStepChar.lower_bound
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
(result : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : eachStepChar HistoryStrategy nfa wf it current next = result)
(lb : εClosure.LowerBound it.next next.states)
:
εClosure.LowerBound it.next result.2.states
theorem
Regex.VM.eachStepChar.done_of_matched_some
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{next' : SearchState HistoryStrategy nfa}
(h : eachStepChar HistoryStrategy nfa wf it current next = (matched', next'))
(isSome' : matched'.isSome = true)
:
theorem
Regex.VM.eachStepChar.inv_of_inv
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current : SearchState HistoryStrategy nfa}
{matched' : Option (List (ℕ × String.Pos))}
{it₀ : String.Iterator}
{next next' : SearchState HistoryStrategy nfa}
(h : eachStepChar HistoryStrategy nfa wf it current next = (matched', next'))
(v : it.Valid)
(notEnd : ¬it.atEnd = true)
(empty : next.states.isEmpty = true)
(inv : SearchState.Inv nfa wf it₀ it current)
:
SearchState.Inv nfa wf it₀ it.next next'
theorem
Regex.VM.eachStepChar.not_done_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
(result : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : eachStepChar HistoryStrategy nfa wf it current next = result)
(isNone : result.1 = none)
(invCurrent : SearchState.NotDoneInv HistoryStrategy nfa current)
(invNext : SearchState.NotDoneInv HistoryStrategy nfa next)
:
SearchState.NotDoneInv HistoryStrategy nfa result.2
theorem
Regex.VM.eachStepChar.mem_of_step_of_none
{nfa : NFA}
{wf : nfa.WellFormed}
{it : String.Iterator}
{current next : SearchState HistoryStrategy nfa}
(result : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : eachStepChar HistoryStrategy nfa wf it current next = result)
(isNone : result.1 = none)
(notDone : SearchState.NotDoneInv HistoryStrategy nfa current)
(lb : εClosure.LowerBound it.next next.states)
(state state' state'' : Fin nfa.nodes.size)
(update : List (ℕ × String.Pos))
: