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