inductive
Regex.Backtracker.Path
(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 : String.Iterator} (v : it.Valid) : Path nfa wf it it ⟨nfa.start, ⋯⟩ []
- more {nfa : NFA} {wf : nfa.WellFormed} {it : String.Iterator} {i j : Fin nfa.nodes.size} {it' it'' : String.Iterator} {update₁ : List (ℕ × String.Pos)} {update₂ : Option (ℕ × String.Pos)} {update₃ : List (ℕ × String.Pos)} (prev : Path nfa wf it it' i update₁) (step : nfa.Step 0 (↑i) it' (↑j) it'' update₂) (equpdate : update₃ = update₁ ++ List.ofOption update₂) : Path nfa wf it it'' j update₃
Instances For
theorem
Regex.Backtracker.Path.validL
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(path : Path nfa wf it it' i update)
:
it.Valid
theorem
Regex.Backtracker.Path.validR
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(path : Path nfa wf it it' i update)
:
it'.Valid
theorem
Regex.Backtracker.Path.toString_eq
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(path : Path nfa wf it it' i update)
:
theorem
Regex.Backtracker.Path.le_pos
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(path : Path nfa wf it it' i update)
:
theorem
Regex.Backtracker.Path.nfaPath_of_ne
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(path : Path nfa wf it it' i update)
(ne : ↑i ≠ nfa.start)
:
theorem
Regex.Backtracker.Path.concat_nfaPath
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i j : ℕ}
{it'' : String.Iterator}
{update₁ update₂ update₃ : List (ℕ × String.Pos)}
(isLt : i < nfa.nodes.size)
(path₁ : Path nfa wf it it' ⟨i, isLt⟩ update₁)
(path₂ : nfa.Path 0 i it' j it'' update₂)
(equpdate : update₃ = update₁ ++ update₂)
:
theorem
Regex.Backtracker.Path.of_nfaPath
{nfa : NFA}
{wf : nfa.WellFormed}
{it it' : String.Iterator}
{i : ℕ}
{update : List (ℕ × String.Pos)}
(path : nfa.Path 0 nfa.start it i it' update)
:
def
Regex.Backtracker.Path.bit'
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit : Data.BoundedIterator startIdx maxIdx}
{it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(path : Path nfa wf bit.it it' i update)
:
Data.BoundedIterator startIdx maxIdx
Instances For
theorem
Regex.Backtracker.Path.reaches
{nfa : NFA}
{wf : nfa.WellFormed}
{startIdx maxIdx : ℕ}
{bit bit' : Data.BoundedIterator startIdx maxIdx}
{it' : String.Iterator}
{i : Fin nfa.nodes.size}
{update : List (ℕ × String.Pos)}
(eqit' : bit'.it = it')
(path : Path nfa wf bit.it it' i update)
:
bit.Reaches bit'