inductive Regex.NFA.Node : Type

• done : Node
• fail : Node
• epsilon (next : Nat) : Node
• anchor (anchor : Data.Anchor) (next : Nat) : Node
• char (c : Char) (next : Nat) : Node
• split (next₁ next₂ : Nat) : Node
• save (offset next : Nat) : Node
• sparse (cs : Data.Classes) (next : Nat) : Node

instance Regex.NFA.instReprNode : Repr Node

Equations

• Regex.NFA.instReprNode = { reprPrec := Regex.NFA.reprNode✝ }

instance Regex.NFA.instDecidableEqNode : DecidableEq Node

Equations

• Regex.NFA.instDecidableEqNode = Regex.NFA.decEqNode✝

instance Regex.NFA.instInhabitedNode : Inhabited Node

Equations

• Regex.NFA.instInhabitedNode = { default := Regex.NFA.Node.done }

instance Regex.NFA.instToExprNode : Lean.ToExpr Node

Equations

• Regex.NFA.instToExprNode = { toExpr := Regex.NFA.toExprNode✝, toTypeExpr := Lean.Expr.const `Regex.NFA.Node [] }

def Regex.NFA.Node.inBounds (n : Node) (size : Nat) : Prop

Equations

• Regex.NFA.Node.done.inBounds size = True
• Regex.NFA.Node.fail.inBounds size = True
• (Regex.NFA.Node.epsilon a).inBounds size = (a < size)
• (Regex.NFA.Node.anchor a a_1).inBounds size = (a_1 < size)
• (Regex.NFA.Node.char a a_1).inBounds size = (a_1 < size)
• (Regex.NFA.Node.split a a_1).inBounds size = (a < size ∧ a_1 < size)
• (Regex.NFA.Node.save a a_1).inBounds size = (a_1 < size)
• (Regex.NFA.Node.sparse a a_1).inBounds size = (a_1 < size)

@[simp]

theorem Regex.NFA.Node.inBounds.done {size : Nat} : Node.done.inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.fail {size : Nat} : Node.fail.inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.epsilon {size next : Nat} (h : next < size) : (Node.epsilon next).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.anchor {size next : Nat} {a : Data.Anchor} (h : next < size) : (Node.anchor a next).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.char {size next : Nat} {c : Char} (h : next < size) : (Node.char c next).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.split {size next₁ next₂ : Nat} (h₁ : next₁ < size) (h₂ : next₂ < size) : (Node.split next₁ next₂).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.save {size offset next : Nat} (h : next < size) : (Node.save offset next).inBounds size

theorem Regex.NFA.Node.lt_of_inBounds.epsilon {size next : Nat} (h : (Node.epsilon next).inBounds size) : next < size

theorem Regex.NFA.Node.lt_of_inBounds.char {size next : Nat} {c : Char} (h : (Node.char c next).inBounds size) : next < size

theorem Regex.NFA.Node.lt_of_inBounds.split {size next₁ next₂ : Nat} (h : (Node.split next₁ next₂).inBounds size) : next₁ < size ∧ next₂ < size

theorem Regex.NFA.Node.lt_of_inBounds.split_left {size next₁ next₂ : Nat} (h : (Node.split next₁ next₂).inBounds size) : next₁ < size

theorem Regex.NFA.Node.lt_of_inBounds.split_right {size next₁ next₂ : Nat} (h : (Node.split next₁ next₂).inBounds size) : next₂ < size

theorem Regex.NFA.Node.lt_of_inBounds.save {size offset next : Nat} (h : (Node.save offset next).inBounds size) : next < size

theorem Regex.NFA.Node.inBounds_of_inBounds_of_le {n : Node} {size size' : Nat} (h : n.inBounds size) (le : size ≤ size') : n.inBounds size'

instance Regex.NFA.Node.decInBounds {node : Node} {size : Nat} : Decidable (node.inBounds size)

Equations

• Regex.NFA.Node.decInBounds = isTrue trivial
• Regex.NFA.Node.decInBounds = isTrue trivial
• Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
• Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
• Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
• Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
• Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next₁ < size ∧ next₂ < size))
• Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))

structure Regex.NFA : Type

A NFA consists an array of nodes and a designated start node.

The transition relation and accept nodes are embedded in the nodes themselves.

• nodes : Array Node
• start : Nat

instance Regex.instReprNFA : Repr NFA

Equations

• Regex.instReprNFA = { reprPrec := Regex.reprNFA✝ }

instance Regex.instDecidableEqNFA : DecidableEq NFA

Equations

• Regex.instDecidableEqNFA = Regex.decEqNFA✝

instance Regex.instInhabitedNFA : Inhabited NFA

Equations

• Regex.instInhabitedNFA = { default := { nodes := default, start := default } }

instance Regex.instToExprNFA : Lean.ToExpr NFA

Equations

• Regex.instToExprNFA = { toExpr := Regex.toExprNFA✝, toTypeExpr := Lean.Expr.const `Regex.NFA [] }

instance Regex.instToStringNFA : ToString NFA

Equations

• Regex.instToStringNFA = { toString := fun (nfa : Regex.NFA) => reprStr nfa }

def Regex.NFA.done : NFA

Equations

• Regex.NFA.done = { nodes := #[Regex.NFA.Node.done], start := 0 }

def Regex.NFA.get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Node

Equations

• nfa.get i h = nfa.nodes[i]

instance Regex.NFA.instGetElemNatNodeLtSizeNodes : GetElem NFA Nat Node fun (nfa : NFA) (i : Nat) => i < nfa.nodes.size

Equations

• Regex.NFA.instGetElemNatNodeLtSizeNodes = { getElem := fun (nfa : Regex.NFA) (i : Nat) (h : i < nfa.nodes.size) => nfa.get i h }

theorem Regex.NFA.get_eq_nodes_get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : nfa[i] = nfa.nodes[i]

def Regex.NFA.maxTag (nfa : NFA) : Nat

Equations

• nfa.maxTag = Array.foldl (fun (accum : Nat) (node : Regex.NFA.Node) => match node with | Regex.NFA.Node.save tag next => accum.max tag | x => accum) 0 nfa.nodes

theorem Regex.NFA.le_maxTag {tag next : Nat} (nfa : NFA) (i : Fin nfa.nodes.size) (eq : nfa[i] = Node.save tag next) : tag ≤ nfa.maxTag

structure Regex.NFA.WellFormed (nfa : NFA) : Prop

• start_lt : nfa.start < nfa.nodes.size
• inBounds (i : Fin nfa.nodes.size) : nfa[i].inBounds nfa.nodes.size

theorem Regex.NFA.WellFormed.iff {nfa : NFA} : nfa.WellFormed ↔ nfa.start < nfa.nodes.size ∧ ∀ (i : Fin nfa.nodes.size), nfa[i].inBounds nfa.nodes.size

theorem Regex.NFA.WellFormed.inBounds' {nfa : NFA} {node : Node} (wf : nfa.WellFormed) (i : Fin nfa.nodes.size) (hn : nfa[i] = node) : node.inBounds nfa.nodes.size

theorem Regex.NFA.done_WellFormed : done.WellFormed

instance Regex.NFA.decWellFormed (nfa : NFA) : Decidable nfa.WellFormed

Equations

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