def
Regex.VM.SearchState.refines
{nfa : NFA}
{bufferSize : ℕ}
(state' : SearchState HistoryStrategy nfa)
(state : SearchState (BufferStrategy bufferSize) nfa)
:
Equations
Instances For
inductive
Regex.VM.εStack.refines
{nfa : NFA}
{bufferSize : ℕ}
:
εStack HistoryStrategy nfa → εStack (BufferStrategy bufferSize) nfa → Prop
- nil {nfa : NFA} {bufferSize : ℕ} : refines [] []
- cons {nfa : NFA} {bufferSize : ℕ} {update : List (ℕ × String.Pos)} {state' : Fin nfa.nodes.size} {tail' : εStack HistoryStrategy nfa} {buffer : Vector (Option String.Pos) bufferSize} {state : Fin nfa.nodes.size} {tail : εStack (BufferStrategy bufferSize) nfa} (h₁ : Strategy.materializeUpdates bufferSize update = buffer) (h₂ : state' = state) (rest : tail'.refines tail) : refines ((update, state') :: tail') ((buffer, state) :: tail)
Instances For
@[simp]
theorem
Regex.VM.εStack.refines_cons
{nfa : NFA}
{bufferSize : ℕ}
{update : HistoryStrategy.Update}
{state' : Fin nfa.nodes.size}
{tail' : List (HistoryStrategy.Update × Fin nfa.nodes.size)}
{stack : εStack (BufferStrategy bufferSize) nfa}
:
refines ((update, state') :: tail') stack ↔ ∃ (buffer : (BufferStrategy bufferSize).Update) (state : Fin nfa.nodes.size) (tail :
List ((BufferStrategy bufferSize).Update × Fin nfa.nodes.size)),
stack = (buffer, state) :: tail ∧ Strategy.materializeUpdates bufferSize update = buffer ∧ state' = state ∧ refines tail' tail
theorem
Regex.VM.εClosure.pushNext.refines
{nfa : NFA}
{bufferSize : ℕ}
{it : String.Iterator}
{stack : εStack (BufferStrategy bufferSize) nfa}
{stack' : εStack HistoryStrategy nfa}
{state : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
{buffer : Vector (Option String.Pos) bufferSize}
(wf : nfa.WellFormed)
(h₁ : Strategy.materializeUpdates bufferSize update = buffer)
(h₂ : stack'.refines stack)
:
(pushNext HistoryStrategy nfa it nfa[state] ⋯ update stack').refines
(pushNext (BufferStrategy bufferSize) nfa it nfa[state] ⋯ buffer stack)
theorem
Regex.VM.εClosure.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{matched : Option (Buffer bufferSize)}
{matched' : Option (List (ℕ × String.Pos))}
{next : SearchState (BufferStrategy bufferSize) nfa}
{next' : SearchState HistoryStrategy nfa}
{stack : εStack (BufferStrategy bufferSize) nfa}
{stack' : εStack HistoryStrategy nfa}
(result : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(result' : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : εClosure (BufferStrategy bufferSize) nfa wf it matched next stack = result)
(h' : εClosure HistoryStrategy nfa wf it matched' next' stack' = result')
(refMatched : Strategy.refineUpdateOpt matched' matched)
(refState : next'.refines next)
(refStack : stack'.refines stack)
:
theorem
Regex.VM.stepChar.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{next : SearchState (BufferStrategy bufferSize) nfa}
{next' : SearchState HistoryStrategy nfa}
{currentUpdates : Vector (BufferStrategy bufferSize).Update nfa.nodes.size}
{currentUpdates' : Vector HistoryStrategy.Update nfa.nodes.size}
{state : Fin nfa.nodes.size}
(result : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(result' : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : stepChar (BufferStrategy bufferSize) nfa wf it currentUpdates next state = result)
(h' : stepChar HistoryStrategy nfa wf it currentUpdates' next' state = result')
(refUpdates : Strategy.refineUpdates currentUpdates' currentUpdates)
(refState : next'.refines next)
:
theorem
Regex.VM.eachStepChar.go.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{next : SearchState (BufferStrategy bufferSize) nfa}
{next' : SearchState HistoryStrategy nfa}
{current : SearchState (BufferStrategy bufferSize) nfa}
{current' : SearchState HistoryStrategy nfa}
{i : ℕ}
{hle : i ≤ current.states.count}
{hle' : i ≤ current'.states.count}
(result : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(result' : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : go (BufferStrategy bufferSize) nfa wf it current i hle next = result)
(h' : go HistoryStrategy nfa wf it current' i hle' next' = result')
(refCurrent : current'.refines current)
(refNext : next'.refines next)
:
theorem
Regex.VM.eachStepChar.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{next : SearchState (BufferStrategy bufferSize) nfa}
{next' : SearchState HistoryStrategy nfa}
{current : SearchState (BufferStrategy bufferSize) nfa}
{current' : SearchState HistoryStrategy nfa}
(result : Option (BufferStrategy bufferSize).Update × SearchState (BufferStrategy bufferSize) nfa)
(result' : Option HistoryStrategy.Update × SearchState HistoryStrategy nfa)
(h : eachStepChar (BufferStrategy bufferSize) nfa wf it current next = result)
(h' : eachStepChar HistoryStrategy nfa wf it current' next' = result')
(refCurrent : current'.refines current)
(refNext : next'.refines next)
:
theorem
Regex.VM.captureNext.go.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
{matched : Option (Buffer bufferSize)}
{matched' : Option (List (ℕ × String.Pos))}
{next : SearchState (BufferStrategy bufferSize) nfa}
{next' : SearchState HistoryStrategy nfa}
{current : SearchState (BufferStrategy bufferSize) nfa}
{current' : SearchState HistoryStrategy nfa}
{result : Option (BufferStrategy bufferSize).Update}
{result' : Option HistoryStrategy.Update}
(h : go (BufferStrategy bufferSize) nfa wf it matched current next = result)
(h' : go HistoryStrategy nfa wf it matched' current' next' = result')
(refMatched : Strategy.refineUpdateOpt matched' matched)
(refCurrent : current'.refines current)
(refNext : next'.refines next)
:
Strategy.refineUpdateOpt result' result
theorem
Regex.VM.captureNext.refines
{nfa : NFA}
{wf : nfa.WellFormed}
{bufferSize : ℕ}
{it : String.Iterator}
:
Strategy.refineUpdateOpt (captureNext HistoryStrategy nfa wf it) (captureNext (BufferStrategy bufferSize) nfa wf it)