internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
ih :
  cs' = [] ∨
    ∃ cs₁ cs₂,
      cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
have toNext : pathToNext result nfa.nodes.size (nfa.nodes.size + 1) i cs :=
  ⟨i, [], cs, rfl, .base gti, (eqj ▸ step).castStart' gti⟩
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
ih :
  cs' = [] ∨
    ∃ cs₁ cs₂,
      cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
ih :
  cs' = [] ∨
    ∃ cs₁ cs₂,
      cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
cases ih with
| inl eqs =>
  subst eqs
  exact ⟨cs, [], rfl, toNext, .complete⟩
| inr cond =>
  obtain ⟨cs₁, cs₂, eqs, path', loop⟩ := cond
  exact ⟨cs, cs₁ ++ cs₂, by simp [eqs], toNext, .loop path' loop⟩
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs
eqs : cs' = []
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
subst eqs
Proof state after:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs
path : (↑result).pathIn nfa.nodes.size j k []
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        [] = [] ∨
          ∃ 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₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ [] = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs
path : (↑result).pathIn nfa.nodes.size j k []
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        [] = [] ∨
          ∃ 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₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ [] = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
exact ⟨cs, [], rfl, toNext, .complete⟩
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs
cond :
  ∃ cs₁ cs₂,
    cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
obtain ⟨cs₁, cs₂, eqs, path', loop⟩ := cond
Proof state after:
case inr.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i 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₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case inr.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i 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₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
exact ⟨cs, cs₁ ++ cs₂, by simp [eqs], toNext, .loop path' loop⟩
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
eqj : j = nfa.nodes.size
toNext : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i 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₂
⊢ cs ++ cs' = cs ++ (cs₁ ++ cs₂)
Tactic:
simp [eqs]
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
ih : ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
obtain ⟨cs₁, cs₂, eqs, path', loop⟩ := ih
Proof state after:
case intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = 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) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
subst eqs
Proof state after:
case intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
path : (↑result).pathIn nfa.nodes.size j k (cs₁ ++ cs₂)
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs₁ ++ cs₂ = [] ∨
          ∃ cs₁_1 cs₂_1,
            cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁_1 ∧ starLoop eq cs₂_1
      else
        ∃ cs₁_1 cs₂_1,
          cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
            (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁_1 ∧ starLoop eq cs₂_1
⊢ ∃ cs₁_1 cs₂_1,
    cs ++ (cs₁ ++ cs₂) = cs₁_1 ++ cs₂_1 ∧
      (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁_1 ∧ starLoop eq cs₂_1
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
path : (↑result).pathIn nfa.nodes.size j k (cs₁ ++ cs₂)
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs₁ ++ cs₂ = [] ∨
          ∃ cs₁_1 cs₂_1,
            cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁_1 ∧ starLoop eq cs₂_1
      else
        ∃ cs₁_1 cs₂_1,
          cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
            (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁_1 ∧ starLoop eq cs₂_1
⊢ ∃ cs₁_1 cs₂_1,
    cs ++ (cs₁ ++ cs₂) = cs₁_1 ++ cs₂_1 ∧
      (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁_1 ∧ starLoop eq cs₂_1
Tactic:
cases step with
| charStep h₁ h₂ step =>
  exact ⟨_ :: cs₁, cs₂, rfl, path'.cons (.charStep gti h₂ step), loop⟩
| εStep h₁ h₂ step =>
  exact ⟨cs₁, cs₂, rfl, path'.cons (.εStep gti h₂ step), loop⟩
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case intro.intro.intro.intro.charStep
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
path : (↑result).pathIn nfa.nodes.size j k (cs₁ ++ cs₂)
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs₁ ++ cs₂ = [] ∨
          ∃ cs₁_1 cs₂_1,
            cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁_1 ∧ starLoop eq cs₂_1
      else
        ∃ cs₁_1 cs₂_1,
          cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
            (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁_1 ∧ starLoop eq cs₂_1
c✝ : Char
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : j ∈ (↑result)[i].charStep c✝
⊢ ∃ cs₁_1 cs₂_1,
    [c✝] ++ (cs₁ ++ cs₂) = cs₁_1 ++ cs₂_1 ∧
      (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁_1 ∧ starLoop eq cs₂_1
Tactic:
exact ⟨_ :: cs₁, cs₂, rfl, path'.cons (.charStep gti h₂ step), loop⟩
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case intro.intro.intro.intro.εStep
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
nej : ¬j = nfa.nodes.size
cs₁ cs₂ : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁
loop : starLoop eq cs₂
path : (↑result).pathIn nfa.nodes.size j k (cs₁ ++ cs₂)
ih :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs₁ ++ cs₂ = [] ∨
          ∃ cs₁_1 cs₂_1,
            cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁_1 ∧ starLoop eq cs₂_1
      else
        ∃ cs₁_1 cs₂_1,
          cs₁ ++ cs₂ = cs₁_1 ++ cs₂_1 ∧
            (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁_1 ∧ starLoop eq cs₂_1
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : j ∈ (↑result)[i].εStep
⊢ ∃ cs₁_1 cs₂_1,
    [] ++ (cs₁ ++ cs₂) = cs₁_1 ++ cs₂_1 ∧
      (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁_1 ∧ starLoop eq cs₂_1
Tactic:
exact ⟨cs₁, cs₂, rfl, path'.cons (.εStep gti h₂ step), loop⟩
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro
Proof 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
Proof 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
Theorem: Regex.NFA.starLoop.intro
Proof 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
Proof 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
Theorem: Regex.NFA.starLoop.intro
Proof 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
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro
Proof 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
Proof state after:
no goals