Theorem: Regex.NFA.starLoop.intro (RegexCorrectness/NFA/Transition/Path/Equivalence/MatchOfPath.lean)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
⊢ starLoop eq cs
Tactic:
let loop := starLoop.intro' eq result.property rfl ev
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
loop : if nfa.nodes.size = nfa.nodes.size then
  cs = [] ∨
    ∃ cs₁ cs₂,
      cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
else
  ∃ cs₁ cs₂,
    cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) nfa.nodes.size cs₁ ∧ starLoop eq cs₂ :=
  intro' eq result.property rfl ev
⊢ starLoop eq cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
loop : if nfa.nodes.size = nfa.nodes.size then
  cs = [] ∨
    ∃ cs₁ cs₂,
      cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
else
  ∃ cs₁ cs₂,
    cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) nfa.nodes.size cs₁ ∧ starLoop eq cs₂ :=
  intro' eq result.property rfl ev
⊢ starLoop eq cs
Tactic:
simp at loop
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
loop :
  cs = [] ∨
    ∃ cs₁ cs₂,
      cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
⊢ starLoop eq cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
loop :
  cs = [] ∨
    ∃ cs₁ cs₂,
      cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
⊢ starLoop eq cs
Tactic:
match loop with
| .inl eqs => exact eqs ▸ .complete
| .inr ⟨cs₁, cs₂, eqs, path, loop⟩ =>
  exact eqs ▸ .loop path loop
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
loop :
  cs = [] ∨
    ∃ cs₁ cs₂,
      cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
eqs : cs = []
⊢ starLoop eq cs
Tactic:
exact eqs ▸ .complete
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
ev : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs
loop✝ :
  cs = [] ∨
    ∃ cs₁ cs₂,
      cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁
loop : starLoop eq cs₂
⊢ starLoop eq cs
Tactic:
exact eqs ▸ .loop path loop
State after:
no goals