theorem
Regex.VM.εClosure.subset
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
(h : εClosure σ nfa wf pos matched next stack = (matched', next'))
:
theorem
Regex.VM.εClosure.mem_next_of_mem_stack
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
{entry : σ.Update × Fin nfa.nodes.size}
(h : εClosure σ nfa wf pos matched next stack = (matched', next'))
(mem_stack : entry ∈ stack)
:
theorem
Regex.VM.εClosure.eq_updates_of_mem_next
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
{i : Fin nfa.nodes.size}
(h : εClosure σ nfa wf pos matched next stack = (matched', next'))
(mem' : i ∈ next.states)
:
theorem
Regex.VM.εClosure.eq_matched_some
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
(h : εClosure σ nfa wf pos matched next stack = (matched', next'))
(isSome : matched.isSome = true)
:
theorem
Regex.VM.εClosure.matched_inv
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
(h : εClosure σ nfa wf pos matched next stack = (matched', next'))
(inv :
∀ (isSome : matched.isSome = true), ∃ i ∈ next.states, nfa[i] = NFA.Node.done ∧ next.updates[i] = matched.get isSome)
(isSome' : matched'.isSome = true)
:
theorem
Regex.VM.εClosure.not_done_of_none
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
(result : Option σ.Update × SearchState σ nfa)
(h : εClosure σ nfa wf pos matched next stack = result)
(isNone : result.1 = none)
(inv : SearchState.NotDoneInv σ nfa next)
:
SearchState.NotDoneInv σ nfa result.2
def
Regex.VM.εClosure.LowerBoundStep
{s : String}
{nfa : NFA}
(pos : s.ValidPos)
(states : Data.SparseSet nfa.nodes.size)
:
Equations
Instances For
def
Regex.VM.εClosure.LowerBound
{s : String}
{nfa : NFA}
(pos : s.ValidPos)
(states : Data.SparseSet nfa.nodes.size)
:
Equations
Instances For
theorem
Regex.VM.εClosure.LowerBound.of_empty
{s : String}
{nfa : NFA}
{pos : s.ValidPos}
{states : Data.SparseSet nfa.nodes.size}
(h : states.isEmpty = true)
:
LowerBound pos states
theorem
Regex.VM.εClosure.LowerBound.of_step
{s : String}
{nfa : NFA}
{pos : s.ValidPos}
{states : Data.SparseSet nfa.nodes.size}
(h : LowerBoundStep pos states)
:
LowerBound pos states
theorem
Regex.VM.εClosure.LowerInvStep.preserves'
{s : String}
{σ : Strategy s}
{nfa : NFA}
{pos : s.ValidPos}
{stack : εStack σ nfa}
{states : Data.SparseSet nfa.nodes.size}
{entry : σ.Update × Fin nfa.nodes.size}
{stack' : εStack σ nfa}
(hmem : entry.2 ∉ states)
(nextEntries : εStack σ nfa)
(hstack : stack' = nextEntries ++ stack)
(h :
∀ (j : Fin nfa.nodes.size) (update : Option (ℕ × s.ValidPos)),
nfa.εStep' pos entry.2 j update → ∃ (update' : σ.Update), (update', j) ∈ nextEntries)
(inv : LowerInvStep pos states (entry :: stack))
:
LowerInvStep pos (states.insert entry.2 hmem) stack'
theorem
Regex.VM.εClosure.LowerInvStep.preserves
{s : String}
{σ : Strategy s}
{nfa : NFA}
{pos : s.ValidPos}
{stack : εStack σ nfa}
{states : Data.SparseSet nfa.nodes.size}
{entry : σ.Update × Fin nfa.nodes.size}
(wf : nfa.WellFormed)
(hmem : entry.2 ∉ states)
(inv : LowerInvStep pos states (entry :: stack))
:
LowerInvStep pos (states.insert entry.2 hmem) (pushNext σ nfa pos nfa[entry.2] ⋯ entry.1 stack)
theorem
Regex.VM.εClosure.lower_bound_step
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{stack : εStack σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
{pos : s.ValidPos}
(h : εClosure σ nfa wf pos matched next stack = (matched', next'))
(inv : LowerInvStep pos next.states stack)
:
LowerBoundStep pos next'.states
theorem
Regex.VM.εClosure.lower_bound
{s : String}
{σ : Strategy s}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option σ.Update}
{next : SearchState σ nfa}
{matched' : Option σ.Update}
{next' : SearchState σ nfa}
{i : Fin nfa.nodes.size}
{update : σ.Update}
(h : εClosure σ nfa wf pos matched next [(update, i)] = (matched', next'))
(lb : LowerBound pos next.states)
:
LowerBound pos next'.states
structure
Regex.VM.εClosure.UpperInv
{s : String}
{nfa : NFA}
(states₀ : Data.SparseSet nfa.nodes.size)
(pos₀ : s.ValidPos)
(i₀ : Fin nfa.nodes.size)
(update₀ : List (ℕ × s.ValidPos))
(next : SearchState (HistoryStrategy s) nfa)
(stack : εStack (HistoryStrategy s) nfa)
:
Intuition: given that we reached i₀ (from nfa.start) with pos₀ and update₀, the εClosure
traversal first puts states reachable from i₀ into the stack with an appropriate update list.
Next, the traversal pops the states from the stack and writes them to next, recording the update
list to updates for the necessary states. Since we only care about ε-transitions, the position
doesn't change during the traversal.
At the end of the traversal, we can guarantee that all states in next were already in states₀ or
they are reachable from i₀ with the updates written to next.updates.
Instances For
theorem
Regex.VM.εClosure.UpperInv.preserves'
{s : String}
{nfa : NFA}
{states₀ : Data.SparseSet nfa.nodes.size}
{pos₀ : s.ValidPos}
{i₀ : Fin nfa.nodes.size}
{update₀ : List (ℕ × s.ValidPos)}
{next : SearchState (HistoryStrategy s) nfa}
{entry : List (ℕ × s.ValidPos) × Fin nfa.nodes.size}
{stack stack' : εStack (HistoryStrategy s) nfa}
{node : NFA.Node}
(hn : nfa[entry.2] = node)
(nextEntries : εStack (HistoryStrategy s) nfa)
(hstack : stack' = nextEntries ++ stack)
(not_mem : entry.2 ∉ next.states)
(h :
∀ (update : (HistoryStrategy s).Update) (j : Fin nfa.nodes.size),
(update, j) ∈ nextEntries →
∃ (update' : Option (ℕ × s.ValidPos)),
update = entry.1 ++ List.ofOption update' ∧ nfa.εStep' pos₀ entry.2 j update')
(inv : UpperInv states₀ pos₀ i₀ update₀ next (entry :: stack))
:
theorem
Regex.VM.εClosure.UpperInv.preserves
{s : String}
{nfa : NFA}
{states₀ : Data.SparseSet nfa.nodes.size}
{pos₀ : s.ValidPos}
{i₀ : Fin nfa.nodes.size}
{update₀ : List (ℕ × s.ValidPos)}
{next : SearchState (HistoryStrategy s) nfa}
{stack : εStack (HistoryStrategy s) nfa}
{update : List (ℕ × s.ValidPos)}
{state : Fin nfa.nodes.size}
(wf : nfa.WellFormed)
(not_mem : state ∉ next.states)
(inv : UpperInv states₀ pos₀ i₀ update₀ next ((update, state) :: stack))
:
theorem
Regex.VM.εClosure.upper_boundAux
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{matched : Option (List (ℕ × s.ValidPos))}
{next : SearchState (HistoryStrategy s) nfa}
{stack : εStack (HistoryStrategy s) nfa}
{matched' : Option (List (ℕ × s.ValidPos))}
{next' : SearchState (HistoryStrategy s) nfa}
(states₀ : Data.SparseSet nfa.nodes.size)
(pos₀ : s.ValidPos)
(i₀ : Fin nfa.nodes.size)
(update₀ : List (ℕ × s.ValidPos))
(h : εClosure (HistoryStrategy s) nfa wf pos₀ matched next stack = (matched', next'))
(inv₀ : UpperInv states₀ pos₀ i₀ update₀ next stack)
:
All new states in next' are reachable from the starting state i₀ and have corresponding updates in next'.updates.
theorem
Regex.VM.εClosure.UpperInv.intro
{s : String}
{nfa : NFA}
{next : SearchState (HistoryStrategy s) nfa}
{i₀ : Fin nfa.nodes.size}
{update₀ : List (ℕ × s.ValidPos)}
(pos₀ : s.ValidPos)
:
Upper invariant at the start of the εClosure traversal.
theorem
Regex.VM.εClosure.upper_bound
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option (List (ℕ × s.ValidPos))}
{next : SearchState (HistoryStrategy s) nfa}
{matched' : Option (List (ℕ × s.ValidPos))}
{next' : SearchState (HistoryStrategy s) nfa}
{i : Fin nfa.nodes.size}
{update : List (ℕ × s.ValidPos)}
(h : εClosure (HistoryStrategy s) nfa wf pos matched next [(update, i)] = (matched', next'))
(j : Fin nfa.nodes.size)
:
theorem
Regex.VM.εClosure.mem_next
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option (List (ℕ × s.ValidPos))}
{next : SearchState (HistoryStrategy s) nfa}
{matched' : Option (List (ℕ × s.ValidPos))}
{next' : SearchState (HistoryStrategy s) nfa}
{i : Fin nfa.nodes.size}
{update : (HistoryStrategy s).Update}
(h : εClosure (HistoryStrategy s) nfa wf pos matched next [(update, i)] = (matched', next'))
(lb : LowerBound pos next.states)
{j : Fin nfa.nodes.size}
{update' : List (ℕ × s.ValidPos)}
(cls : nfa.εClosure' pos i j update')
:
εClosure inserts all states in the ε-closure of i into next.states.
theorem
Regex.VM.εClosure.write_updates_of_mem_next
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option (List (ℕ × s.ValidPos))}
{next : SearchState (HistoryStrategy s) nfa}
{matched' : Option (List (ℕ × s.ValidPos))}
{next' : SearchState (HistoryStrategy s) nfa}
{i j : Fin nfa.nodes.size}
{update : List (ℕ × s.ValidPos)}
(h : εClosure (HistoryStrategy s) nfa wf pos matched next [(update, i)] = (matched', next'))
(mem : j ∈ next'.states)
:
All states in next'.states are already in next.states or they are reachable from i with the
updates written to next'.updates.
theorem
Regex.VM.εClosure.write_updates
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option (List (ℕ × s.ValidPos))}
{next : SearchState (HistoryStrategy s) nfa}
{matched' : Option (List (ℕ × s.ValidPos))}
{next' : SearchState (HistoryStrategy s) nfa}
{i j : Fin nfa.nodes.size}
{update update' : List (ℕ × s.ValidPos)}
(h : εClosure (HistoryStrategy s) nfa wf pos matched next [(update, i)] = (matched', next'))
(lb : LowerBound pos next.states)
(cls : nfa.εClosure' pos i j update')
:
For all states in the ε-closure of i, it's already in next.states or there is a path from i
whose updates are written to next.updates. The written update list can be different since the
traversal may have reached the state through a different path.
theorem
Regex.VM.εClosure.inv_of_inv
{s : String}
{nfa : NFA}
{wf : nfa.WellFormed}
{pos : s.ValidPos}
{matched : Option (List (ℕ × s.ValidPos))}
{next : SearchState (HistoryStrategy s) nfa}
{matched' : Option (List (ℕ × s.ValidPos))}
{next' : SearchState (HistoryStrategy s) nfa}
{pos₀ : s.ValidPos}
(h : εClosure (HistoryStrategy s) nfa wf pos matched next [([], ⟨nfa.start, ⋯⟩)] = (matched', next'))
(le : pos₀ ≤ pos)
(inv : SearchState.Inv nfa wf pos₀ pos next)
:
SearchState.Inv nfa wf pos₀ pos next'