class Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr

def Regex.NFA.Compile.ProofData.nfa' [ProofData] : NFA

Equations

• Regex.NFA.Compile.ProofData.nfa' = Regex.NFA.Compile.ProofData.nfa.pushRegex Regex.NFA.Compile.ProofData.next Regex.NFA.Compile.ProofData.e

theorem Regex.NFA.Compile.ProofData.size_lt [ProofData] : nfa.nodes.size < nfa'.nodes.size

theorem Regex.NFA.Compile.ProofData.eq_result [ProofData] {result : NFA} (eq : nfa.pushRegex next e = result) : result = nfa'

theorem Regex.NFA.Compile.ProofData.eq [ProofData] : nfa.pushRegex next e = nfa'

class Regex.NFA.Compile.ProofData.Emptyextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• expr_eq : e = Data.Expr.empty

def Regex.NFA.Compile.ProofData.Empty.intro {nfa : NFA} {next : Nat} {result : NFA} : nfa.pushRegex next Data.Expr.empty = result → Empty

Equations

• Regex.NFA.Compile.ProofData.Empty.intro x✝ = { nfa := nfa, next := next, e := Regex.Data.Expr.empty, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Empty.intro' (nfa : NFA) (next : Nat) : Empty

Equations

• Regex.NFA.Compile.ProofData.Empty.intro' nfa next = { nfa := nfa, next := next, e := Regex.Data.Expr.empty, expr_eq := ⋯ }

theorem Regex.NFA.Compile.ProofData.Empty.eq' [Empty] : nfa' = nfa.pushRegex next Data.Expr.empty

theorem Regex.NFA.Compile.ProofData.Empty.start_eq [Empty] : nfa'.start = nfa.nodes.size

theorem Regex.NFA.Compile.ProofData.Empty.size_eq [Empty] : nfa'.nodes.size = nfa.nodes.size + 1

theorem Regex.NFA.Compile.ProofData.Empty.get_lt [Empty] {i : Nat} (h : i < nfa.nodes.size) : nfa'[i] = nfa[i]

theorem Regex.NFA.Compile.ProofData.Empty.get_eq [Empty] : nfa'[nfa.nodes.size] = Node.fail

theorem Regex.NFA.Compile.ProofData.Empty.get [Empty] (i : Nat) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else nfa'[i] = Node.fail

class Regex.NFA.Compile.ProofData.Epsilonextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• expr_eq : e = Data.Expr.epsilon

def Regex.NFA.Compile.ProofData.Epsilon.intro {nfa : NFA} {next : Nat} {result : NFA} : nfa.pushRegex next Data.Expr.epsilon = result → Epsilon

Equations

• Regex.NFA.Compile.ProofData.Epsilon.intro x✝ = { nfa := nfa, next := next, e := Regex.Data.Expr.epsilon, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Epsilon.intro' (nfa : NFA) (next : Nat) : Epsilon

Equations

• Regex.NFA.Compile.ProofData.Epsilon.intro' nfa next = { nfa := nfa, next := next, e := Regex.Data.Expr.epsilon, expr_eq := ⋯ }

theorem Regex.NFA.Compile.ProofData.Epsilon.eq' [Epsilon] : nfa' = nfa.pushRegex next Data.Expr.epsilon

theorem Regex.NFA.Compile.ProofData.Epsilon.start_eq [Epsilon] : nfa'.start = nfa.nodes.size

theorem Regex.NFA.Compile.ProofData.Epsilon.size_eq [Epsilon] : nfa'.nodes.size = nfa.nodes.size + 1

theorem Regex.NFA.Compile.ProofData.Epsilon.get_lt [Epsilon] {i : Nat} (h : i < nfa.nodes.size) : nfa'[i] = nfa[i]

theorem Regex.NFA.Compile.ProofData.Epsilon.get_eq [Epsilon] : nfa'[nfa.nodes.size] = Node.epsilon next

theorem Regex.NFA.Compile.ProofData.Epsilon.get [Epsilon] (i : Nat) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else nfa'[i] = Node.epsilon next

class Regex.NFA.Compile.ProofData.Anchorextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• anchor : Data.Anchor
• expr_eq : e = Data.Expr.anchor anchor

def Regex.NFA.Compile.ProofData.Anchor.intro {nfa : NFA} {next : Nat} {anchor : Data.Anchor} {result : NFA} : nfa.pushRegex next (Data.Expr.anchor anchor) = result → Anchor

Equations

• Regex.NFA.Compile.ProofData.Anchor.intro x✝ = { nfa := nfa, next := next, e := Regex.Data.Expr.anchor anchor, anchor := anchor, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Anchor.intro' (nfa : NFA) (next : Nat) (anchor : Data.Anchor) : Anchor

Equations

• Regex.NFA.Compile.ProofData.Anchor.intro' nfa next anchor = { nfa := nfa, next := next, e := Regex.Data.Expr.anchor anchor, anchor := anchor, expr_eq := ⋯ }

theorem Regex.NFA.Compile.ProofData.Anchor.eq' [Anchor] : nfa' = nfa.pushRegex next (Data.Expr.anchor anchor)

theorem Regex.NFA.Compile.ProofData.Anchor.start_eq [Anchor] : nfa'.start = nfa.nodes.size

theorem Regex.NFA.Compile.ProofData.Anchor.size_eq [Anchor] : nfa'.nodes.size = nfa.nodes.size + 1

theorem Regex.NFA.Compile.ProofData.Anchor.get_lt [Anchor] {i : Nat} (h : i < nfa.nodes.size) : nfa'[i] = nfa[i]

theorem Regex.NFA.Compile.ProofData.Anchor.get_eq [Anchor] : nfa'[nfa.nodes.size] = Node.anchor anchor next

theorem Regex.NFA.Compile.ProofData.Anchor.get [Anchor] (i : Nat) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else nfa'[i] = Node.anchor anchor next

class Regex.NFA.Compile.ProofData.Charextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• c : _root_.Char
• expr_eq : e = Data.Expr.char c

def Regex.NFA.Compile.ProofData.Char.intro {nfa : NFA} {next : Nat} {c : _root_.Char} {result : NFA} : nfa.pushRegex next (Data.Expr.char c) = result → Char

Equations

• Regex.NFA.Compile.ProofData.Char.intro x✝ = { nfa := nfa, next := next, e := Regex.Data.Expr.char c, c := c, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Char.intro' (nfa : NFA) (next : Nat) (c : _root_.Char) : Char

Equations

• Regex.NFA.Compile.ProofData.Char.intro' nfa next c = { nfa := nfa, next := next, e := Regex.Data.Expr.char c, c := c, expr_eq := ⋯ }

theorem Regex.NFA.Compile.ProofData.Char.eq' [Char] : nfa' = nfa.pushRegex next (Data.Expr.char c)

theorem Regex.NFA.Compile.ProofData.Char.start_eq [Char] : nfa'.start = nfa.nodes.size

theorem Regex.NFA.Compile.ProofData.Char.size_eq [Char] : nfa'.nodes.size = nfa.nodes.size + 1

theorem Regex.NFA.Compile.ProofData.Char.get_lt [Char] {i : Nat} (h : i < nfa.nodes.size) : nfa'[i] = nfa[i]

theorem Regex.NFA.Compile.ProofData.Char.get_eq [Char] : nfa'[nfa.nodes.size] = Node.char c next

theorem Regex.NFA.Compile.ProofData.Char.get [Char] (i : Nat) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else nfa'[i] = Node.char c next

class Regex.NFA.Compile.ProofData.Classesextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• cs : Data.Classes
• expr_eq : e = Data.Expr.classes cs

def Regex.NFA.Compile.ProofData.Classes.intro {nfa : NFA} {next : Nat} {cs : Data.Classes} {result : NFA} : nfa.pushRegex next (Data.Expr.classes cs) = result → Classes

Equations

• Regex.NFA.Compile.ProofData.Classes.intro x✝ = { nfa := nfa, next := next, e := Regex.Data.Expr.classes cs, cs := cs, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Classes.intro' (nfa : NFA) (next : Nat) (cs : Data.Classes) : Classes

Equations

• Regex.NFA.Compile.ProofData.Classes.intro' nfa next cs = { nfa := nfa, next := next, e := Regex.Data.Expr.classes cs, cs := cs, expr_eq := ⋯ }

theorem Regex.NFA.Compile.ProofData.Classes.eq' [Classes] : nfa' = nfa.pushRegex next (Data.Expr.classes cs)

theorem Regex.NFA.Compile.ProofData.Classes.start_eq [Classes] : nfa'.start = nfa.nodes.size

theorem Regex.NFA.Compile.ProofData.Classes.size_eq [Classes] : nfa'.nodes.size = nfa.nodes.size + 1

theorem Regex.NFA.Compile.ProofData.Classes.get_lt [Classes] {i : Nat} (h : i < nfa.nodes.size) : nfa'[i] = nfa[i]

theorem Regex.NFA.Compile.ProofData.Classes.get_eq [Classes] : nfa'[nfa.nodes.size] = Node.sparse cs next

theorem Regex.NFA.Compile.ProofData.Classes.get [Classes] (i : Nat) (h : i < nfa'.nodes.size) : if x : i < nfa.nodes.size then nfa'[i] = nfa[i] else nfa'[i] = Node.sparse cs next

class Regex.NFA.Compile.ProofData.Groupextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• tag : Nat
• e' : Data.Expr
• expr_eq : e = Data.Expr.group tag e'

def Regex.NFA.Compile.ProofData.Group.intro {nfa : NFA} {next tag : Nat} {e' : Data.Expr} {result : NFA} : nfa.pushRegex next (Data.Expr.group tag e') = result → Group

Equations

• Regex.NFA.Compile.ProofData.Group.intro x✝ = { nfa := nfa, next := next, e := Regex.Data.Expr.group tag e', tag := tag, e' := e', expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Group.intro' (nfa : NFA) (next tag : Nat) (e' : Data.Expr) : Group

Equations

• Regex.NFA.Compile.ProofData.Group.intro' nfa next tag e' = { nfa := nfa, next := next, e := Regex.Data.Expr.group tag e', tag := tag, e' := e', expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Group.nfaClose [Group] : NFA

Equations

• Regex.NFA.Compile.ProofData.Group.nfaClose = Regex.NFA.Compile.ProofData.nfa.pushNode (Regex.NFA.Node.save (2 * Regex.NFA.Compile.ProofData.Group.tag + 1) Regex.NFA.Compile.ProofData.next)

def Regex.NFA.Compile.ProofData.Group.nfaExpr [Group] : NFA

Equations

• Regex.NFA.Compile.ProofData.Group.nfaExpr = Regex.NFA.Compile.ProofData.Group.nfaClose.pushRegex Regex.NFA.Compile.ProofData.Group.nfaClose.start Regex.NFA.Compile.ProofData.Group.e'

theorem Regex.NFA.Compile.ProofData.Group.nfaClose_property [Group] : nfa.nodes.size < nfaClose.nodes.size

theorem Regex.NFA.Compile.ProofData.Group.nfaExpr_property [Group] : nfaClose.nodes.size < nfaExpr.nodes.size

theorem Regex.NFA.Compile.ProofData.Group.eq' [Group] : nfa' = nfa.pushRegex next (Data.Expr.group tag e')

theorem Regex.NFA.Compile.ProofData.Group.eq_push [Group] : nfa' = nfaExpr.pushNode (Node.save (2 * tag) nfaExpr.start)

theorem Regex.NFA.Compile.ProofData.Group.start_eq [Group] : nfa'.start = nfaExpr.nodes.size

theorem Regex.NFA.Compile.ProofData.Group.size_lt_expr' [Group] : nfaExpr.nodes.size < nfa'.nodes.size

theorem Regex.NFA.Compile.ProofData.Group.size_lt_close' [Group] : nfaClose.nodes.size < nfa'.nodes.size

theorem Regex.NFA.Compile.ProofData.Group.size_lt_nfa_expr [Group] : nfa.nodes.size < nfaExpr.nodes.size

theorem Regex.NFA.Compile.ProofData.Group.get_open [Group] : nfa'[nfaExpr.nodes.size] = Node.save (2 * tag) nfaExpr.start

theorem Regex.NFA.Compile.ProofData.Group.get_lt_expr [Group] {i : Nat} (h : i < nfaExpr.nodes.size) : nfa'[i] = nfaExpr[i]

theorem Regex.NFA.Compile.ProofData.Group.get_close_pre [Group] : nfaClose[nfa.nodes.size] = Node.save (2 * tag + 1) next

class Regex.NFA.Compile.ProofData.Alternateextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• e₁ : Data.Expr
• e₂ : Data.Expr
• expr_eq : e = e₁.alternate e₂

def Regex.NFA.Compile.ProofData.Alternate.intro {nfa : NFA} {next : Nat} {e₁ e₂ : Data.Expr} {result : NFA} : nfa.pushRegex next (e₁.alternate e₂) = result → Alternate

Equations

• Regex.NFA.Compile.ProofData.Alternate.intro x✝ = { nfa := nfa, next := next, e := e₁.alternate e₂, e₁ := e₁, e₂ := e₂, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Alternate.intro' (nfa : NFA) (next : Nat) (e₁ e₂ : Data.Expr) : Alternate

Equations

• Regex.NFA.Compile.ProofData.Alternate.intro' nfa next e₁ e₂ = { nfa := nfa, next := next, e := e₁.alternate e₂, e₁ := e₁, e₂ := e₂, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Alternate.nfa₁ [Alternate] : NFA

Equations

• Regex.NFA.Compile.ProofData.Alternate.nfa₁ = Regex.NFA.Compile.ProofData.nfa.pushRegex Regex.NFA.Compile.ProofData.next Regex.NFA.Compile.ProofData.Alternate.e₁

def Regex.NFA.Compile.ProofData.Alternate.nfa₂ [Alternate] : NFA

Equations

• Regex.NFA.Compile.ProofData.Alternate.nfa₂ = Regex.NFA.Compile.ProofData.Alternate.nfa₁.pushRegex Regex.NFA.Compile.ProofData.next Regex.NFA.Compile.ProofData.Alternate.e₂

theorem Regex.NFA.Compile.ProofData.Alternate.nfa₁_property [Alternate] : nfa.nodes.size < nfa₁.nodes.size

theorem Regex.NFA.Compile.ProofData.Alternate.nfa₂_property [Alternate] : nfa₁.nodes.size < nfa₂.nodes.size

theorem Regex.NFA.Compile.ProofData.Alternate.eq' [Alternate] : nfa' = nfa.pushRegex next (e₁.alternate e₂)

theorem Regex.NFA.Compile.ProofData.Alternate.eq_push [Alternate] : nfa' = nfa₂.pushNode (Node.split nfa₁.start nfa₂.start)

theorem Regex.NFA.Compile.ProofData.Alternate.size_lt₂ [Alternate] : nfa₂.nodes.size < nfa'.nodes.size

theorem Regex.NFA.Compile.ProofData.Alternate.size_lt₁ [Alternate] : nfa₁.nodes.size < nfa'.nodes.size

theorem Regex.NFA.Compile.ProofData.Alternate.get_split [Alternate] : nfa'[nfa₂.nodes.size] = Node.split nfa₁.start nfa₂.start

theorem Regex.NFA.Compile.ProofData.Alternate.start_eq [Alternate] : nfa'.start = nfa₂.nodes.size

theorem Regex.NFA.Compile.ProofData.Alternate.get_start [Alternate] : nfa'[nfa'.start] = Node.split nfa₁.start nfa₂.start

class Regex.NFA.Compile.ProofData.Concatextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• e₁ : Data.Expr
• e₂ : Data.Expr
• expr_eq : e = e₁.concat e₂

def Regex.NFA.Compile.ProofData.Concat.intro {nfa : NFA} {next : Nat} {e₁ e₂ : Data.Expr} {result : NFA} : nfa.pushRegex next (e₁.concat e₂) = result → Concat

Equations

• Regex.NFA.Compile.ProofData.Concat.intro x✝ = { nfa := nfa, next := next, e := e₁.concat e₂, e₁ := e₁, e₂ := e₂, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Concat.intro' (nfa : NFA) (next : Nat) (e₁ e₂ : Data.Expr) : Concat

Equations

• Regex.NFA.Compile.ProofData.Concat.intro' nfa next e₁ e₂ = { nfa := nfa, next := next, e := e₁.concat e₂, e₁ := e₁, e₂ := e₂, expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Concat.nfa₂ [Concat] : NFA

Equations

• Regex.NFA.Compile.ProofData.Concat.nfa₂ = Regex.NFA.Compile.ProofData.nfa.pushRegex Regex.NFA.Compile.ProofData.next Regex.NFA.Compile.ProofData.Concat.e₂

theorem Regex.NFA.Compile.ProofData.Concat.nfa₂_property [Concat] : nfa.nodes.size < nfa₂.nodes.size

theorem Regex.NFA.Compile.ProofData.Concat.eq' [Concat] : nfa' = nfa.pushRegex next (e₁.concat e₂)

theorem Regex.NFA.Compile.ProofData.Concat.eq_push [Concat] : nfa' = nfa₂.pushRegex nfa₂.start e₁

theorem Regex.NFA.Compile.ProofData.Concat.size₂_lt [Concat] : nfa₂.nodes.size < nfa'.nodes.size

class Regex.NFA.Compile.ProofData.Starextends Regex.NFA.Compile.ProofData : Type

• nfa : NFA
• next : Nat
• e : Data.Expr
• e' : Data.Expr
• expr_eq : e = e'.star

def Regex.NFA.Compile.ProofData.Star.intro {nfa : NFA} {next : Nat} {e' : Data.Expr} {result : NFA} : nfa.pushRegex next e'.star = result → Star

Equations

• Regex.NFA.Compile.ProofData.Star.intro x✝ = { nfa := nfa, next := next, e := e'.star, e' := e', expr_eq := ⋯ }

def Regex.NFA.Compile.ProofData.Star.intro' (nfa : NFA) (next : Nat) (e' : Data.Expr) : Star

Equations

• Regex.NFA.Compile.ProofData.Star.intro' nfa next e' = { nfa := nfa, next := next, e := e'.star, e' := e', expr_eq := ⋯ }

theorem Regex.NFA.Compile.ProofData.Star.eq' [Star] : nfa' = nfa.pushRegex next e'.star

def Regex.NFA.Compile.ProofData.Star.nfaPlaceholder [Star] : NFA

Equations

• Regex.NFA.Compile.ProofData.Star.nfaPlaceholder = Regex.NFA.Compile.ProofData.nfa.pushNode Regex.NFA.Node.fail

def Regex.NFA.Compile.ProofData.Star.nfaExpr [Star] : NFA

Equations

• Regex.NFA.Compile.ProofData.Star.nfaExpr = Regex.NFA.Compile.ProofData.Star.nfaPlaceholder.pushRegex Regex.NFA.Compile.ProofData.Star.nfaPlaceholder.start Regex.NFA.Compile.ProofData.Star.e'

theorem Regex.NFA.Compile.ProofData.Star.nfaPlaceholder_property [Star] : nfa.nodes.size < nfaPlaceholder.nodes.size

theorem Regex.NFA.Compile.ProofData.Star.nfaExpr_property [Star] : nfaPlaceholder.nodes.size < nfaExpr.nodes.size

theorem Regex.NFA.Compile.ProofData.Star.start_eq [Star] : nfa'.start = nfa.nodes.size

theorem Regex.NFA.Compile.ProofData.Star.size_eq_expr' [Star] : nfa'.nodes.size = nfaExpr.nodes.size

theorem Regex.NFA.Compile.ProofData.Star.get_start [Star] : nfa'[nfa.nodes.size] = Node.split nfaExpr.start next

theorem Regex.NFA.Compile.ProofData.Star.get_ne_start [Star] (i : Nat) (h : i < nfa'.nodes.size) (ne : i ≠ nfa.nodes.size) : nfa'[i] = nfaExpr[i]