theorem Regex.NFA.Step.εStep_or_charStep {nfa : NFA} {it it' : String.Iterator} {i j : ℕ} {update : Option (ℕ × String.Pos)} (wf : nfa.WellFormed) (step : nfa.Step 0 i it j it' update) : nfa.εStep' it ⟨i, ⋯⟩ ⟨j, ⋯⟩ update ∧ it' = it ∨ nfa.CharStep it ⟨i, ⋯⟩ ⟨j, ⋯⟩ ∧ it' = it.next ∧ update = none

inductive Regex.NFA.VMPath (nfa : NFA) (wf : nfa.WellFormed) (it₀ : String.Iterator) : String.Iterator → Fin nfa.nodes.size → List (ℕ × String.Pos) → Prop

• init {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (eqs : it.toString = it₀.toString) (le : it₀.pos ≤ it.pos) (cls : nfa.εClosure' it ⟨nfa.start, ⋯⟩ i update) : nfa.VMPath wf it₀ it i update
• more {nfa : NFA} {wf : nfa.WellFormed} {it₀ : String.Iterator} {i j k : Fin nfa.nodes.size} {it it' : String.Iterator} {update₁ update₂ update₃ : List (ℕ × String.Pos)} (prev : nfa.VMPath wf it₀ it i update₁) (step : nfa.CharStep it i j) (cls : nfa.εClosure' it.next j k update₂) (hupdate : update₃ = update₁ ++ update₂) (eqit : it' = it.next) : nfa.VMPath wf it₀ it' k update₃

theorem Regex.NFA.VMPath.more_εStep {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i j : Fin nfa.nodes.size} {update₁ : List (ℕ × String.Pos)} {update₂ : Option (ℕ × String.Pos)} (prev : nfa.VMPath wf it₀ it i update₁) (step : nfa.εStep' it i j update₂) : nfa.VMPath wf it₀ it j (update₁ ++ List.ofOption update₂)

theorem Regex.NFA.VMPath.more_charStep {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i j : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (prev : nfa.VMPath wf it₀ it i update) (step : nfa.CharStep it i j) : nfa.VMPath wf it₀ it.next j update

theorem Regex.NFA.VMPath.more_step {nfa : NFA} {wf : nfa.WellFormed} {it₀ it it' : String.Iterator} {i : Fin nfa.nodes.size} {j : ℕ} {update₁ : List (ℕ × String.Pos)} {update₂ : Option (ℕ × String.Pos)} (prev : nfa.VMPath wf it₀ it i update₁) (step : nfa.Step 0 (↑i) it j it' update₂) : nfa.VMPath wf it₀ it' ⟨j, ⋯⟩ (update₁ ++ List.ofOption update₂)

theorem Regex.NFA.VMPath.valid {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (path : nfa.VMPath wf it₀ it i update) : it.Valid

theorem Regex.NFA.VMPath.toString {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (path : nfa.VMPath wf it₀ it i update) : it.toString = it₀.toString

theorem Regex.NFA.VMPath.le_pos {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (path : nfa.VMPath wf it₀ it i update) : it₀.pos ≤ it.pos

theorem Regex.NFA.VMPath.εClosure_of_eq_it {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (path : nfa.VMPath wf it it i update) : nfa.εClosure' it ⟨nfa.start, ⋯⟩ i update

theorem Regex.NFA.VMPath.eq_or_nfaPath {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (path : nfa.VMPath wf it₀ it i update) : ↑i = nfa.start ∧ update = [] ∧ it.toString = it₀.toString ∧ it₀.pos ≤ it.pos ∨ ∃ (its : String.Iterator), its.toString = it₀.toString ∧ it₀.pos ≤ its.pos ∧ nfa.Path 0 nfa.start its (↑i) it update

theorem Regex.NFA.VMPath.nfaPath_of_ne {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} (path : nfa.VMPath wf it₀ it i update) (ne : ↑i ≠ nfa.start) : ∃ (its : String.Iterator), its.toString = it₀.toString ∧ it₀.pos ≤ its.pos ∧ nfa.Path 0 nfa.start its (↑i) it update

theorem Regex.NFA.VMPath.concat_nfaPath {nfa : NFA} {wf : nfa.WellFormed} {it₀ it it' : String.Iterator} {i j : ℕ} {update₁ update₂ : List (ℕ × String.Pos)} (isLt₁ : i < nfa.nodes.size) (path₁ : nfa.VMPath wf it₀ it ⟨i, isLt₁⟩ update₁) (path₂ : nfa.Path 0 i it j it' update₂) : nfa.VMPath wf it₀ it' ⟨j, ⋯⟩ (update₁ ++ update₂)

theorem Regex.NFA.VMPath.of_nfaPath {nfa : NFA} {it₀ it it' : String.Iterator} {i : ℕ} {update : List (ℕ × String.Pos)} (wf : nfa.WellFormed) (eqs : it.toString = it₀.toString) (le : it₀.pos ≤ it.pos) (path : nfa.Path 0 nfa.start it i it' update) : nfa.VMPath wf it₀ it' ⟨i, ⋯⟩ update

def Regex.VM.SearchState.Inv (nfa : NFA) (wf : nfa.WellFormed) (it₀ it : String.Iterator) (next : SearchState HistoryStrategy nfa) : Prop

The invariant for the soundness theorem.

All states in next.state have a corresponding path from nfa.start to the state ending at it, and their updates are written to next.updates when necessary.

Equations

• One or more equations did not get rendered due to their size.

theorem Regex.VM.SearchState.Inv.of_empty {nfa : NFA} {wf : nfa.WellFormed} {it₀ it : String.Iterator} {next : SearchState HistoryStrategy nfa} (h : next.states.isEmpty = true) : Inv nfa wf it₀ it next

def Regex.VM.SearchState.MemOfPathInv (nfa : NFA) (wf : nfa.WellFormed) (it₀ it : String.Iterator) (next : SearchState HistoryStrategy nfa) : Prop

The invariant for the completeness theorem. The invariant holds only when returning .none, since we short-circuit when encountering .done.

For all paths ending at it, the state must be tracked in next.states. We don't care about the updates for the completeness.

Equations

• Regex.VM.SearchState.MemOfPathInv nfa wf it₀ it next = ∀ (i : Fin nfa.nodes.size) (update : List (ℕ × String.Pos)), nfa.VMPath wf it₀ it i update → i ∈ next.states

def Regex.VM.SearchState.NotDoneInv (σ : Strategy) (nfa : NFA) (next : SearchState σ nfa) : Prop

Invariant for the completeness theorem.

The .done state is not in next.states.

Equations

• Regex.VM.SearchState.NotDoneInv σ nfa next = ∀ i ∈ next.states, nfa[i] ≠ Regex.NFA.Node.done

theorem Regex.VM.SearchState.NotDoneInv.of_empty {σ : Strategy} {nfa : NFA} {next : SearchState σ nfa} (h : next.states.isEmpty = true) : NotDoneInv σ nfa next

theorem Regex.NFA.CharStep.write_update {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} (step : nfa.CharStep it i j) : VM.εClosure.writeUpdate nfa[i] = true