theorem
Regex.NFA.EquivUpdate.materialize
{s : String}
{e : Data.Expr}
{n : ℕ}
{pos pos' : s.Pos}
{groups : Data.CaptureGroups s}
{updates : List (ℕ × s.Pos)}
(c : Data.Expr.Captures pos pos' groups e)
(disj : e.Disjoint)
(eqv : EquivUpdate groups updates)
:
Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) (Strategy.materializeUpdates n updates)
Under suitable conditions, the equivalence between capture groups and NFA buffer updates can be naturally transformed into a materialized version.
theorem
Regex.NFA.EquivUpdate.materialize.concat
{s : String}
{n : ℕ}
{g₁ g₂ : Data.CaptureGroups s}
{u₁ u₂ : List (ℕ × s.Pos)}
(eqv₁ : Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups g₁) (Strategy.materializeUpdates n u₁))
(eqv₂ : Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups g₂) (Strategy.materializeUpdates n u₂))
(tag : ℕ)
:
(∀ (h₁ : 2 * tag < n),
Strategy.equivPos (Option.map (fun (x : s.Pos × s.Pos) => x.1) (Strategy.materializeRegexGroups (g₁.concat g₂) tag))
(Strategy.materializeUpdates n (u₁ ++ u₂))[2 * tag]) ∧ ∀ (h₂ : 2 * tag + 1 < n),
Strategy.equivPos (Option.map (fun (x : s.Pos × s.Pos) => x.2) (Strategy.materializeRegexGroups (g₁.concat g₂) tag))
(Strategy.materializeUpdates n (u₁ ++ u₂))[2 * tag + 1]