theorem
Regex.NFA.captures_of_path.group
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
{tag : ℕ}
(eq : nfa.pushRegex next (Data.Expr.group tag e) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start it next it' update)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
nfa.pushRegex next e = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start it next it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups (Data.Expr.group tag e)
theorem
Regex.NFA.captures_of_path.alternate
{nfa : NFA}
{next : ℕ}
{result : NFA}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.alternate e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start it next it' update)
(ih₁ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
nfa.pushRegex next e₁ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start it next it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e₁)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start it next it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e₂)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups (e₁.alternate e₂)
theorem
Regex.NFA.captures_of_path.concat
{nfa : NFA}
{next : ℕ}
{result : NFA}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
{e₁ e₂ : Data.Expr}
(eq : nfa.pushRegex next (e₁.concat e₂) = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start it next it' update)
(ih₁ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
nfa.pushRegex next e₁ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start it next it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e₁)
(ih₂ :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
nfa.pushRegex next e₂ = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start it next it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e₂)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups (e₁.concat e₂)
theorem
Regex.NFA.captures_of_path.star_of_loop
{e : Data.Expr}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
[Compile.ProofData.Star]
(loop : Compile.ProofData.Star.Loop it it' update)
(ih :
∀ {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
Compile.ProofData.nfa'.Path Compile.ProofData.Star.nfaPlaceholder.nodes.size Compile.ProofData.Star.nfaExpr.start it
Compile.ProofData.Star.nfaPlaceholder.start it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e.star
theorem
Regex.NFA.captures_of_path.star
{nfa : NFA}
{next : ℕ}
{result : NFA}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
{e : Data.Expr}
(eq : nfa.pushRegex next e.star = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start it next it' update)
(ih :
∀ {nfa : NFA} {next : ℕ} {result : NFA} {it it' : String.Iterator} {update : List (ℕ × String.Pos)},
nfa.pushRegex next e = result →
nfa.WellFormed →
next < nfa.nodes.size →
result.Path nfa.nodes.size result.start it next it' update →
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e.star
theorem
Regex.NFA.captures_of_path
{nfa : NFA}
{next : ℕ}
{e : Data.Expr}
{result : NFA}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
(eq : nfa.pushRegex next e = result)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(path : result.Path nfa.nodes.size result.start it next it' update)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e
theorem
Regex.NFA.captures_of_path_compile
{nfa : NFA}
{e : Data.Expr}
{it it' : String.Iterator}
{update : List (ℕ × String.Pos)}
(eq : compile e = nfa)
(path : nfa.Path 1 nfa.start it 0 it' update)
:
∃ (groups : Data.CaptureGroups), EquivUpdate groups update ∧ Data.Expr.Captures it it' groups e