internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case εStep.h
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
k : ℕ
cs' : List Char
assm₂ : k = nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
path : (↑result).pathIn nfa.nodes.size (rStart_of eq) k cs'
ih✝ :
  rStart_of eq < (↑result).nodes.size →
    k = nfa.nodes.size →
      if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
ih :
  if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
step : rStart_of eq ∈ (↑result)[nfa.nodes.size].εStep
⊢ ∃ cs₁ cs₂,
    cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Tactic:
have : rStart_of eq ≠ nfa.nodes.size := Nat.ne_of_gt ge
Proof state after:
case εStep.h
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
k : ℕ
cs' : List Char
assm₂ : k = nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
path : (↑result).pathIn nfa.nodes.size (rStart_of eq) k cs'
ih✝ :
  rStart_of eq < (↑result).nodes.size →
    k = nfa.nodes.size →
      if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
ih :
  if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
step : rStart_of eq ∈ (↑result)[nfa.nodes.size].εStep
this : rStart_of eq ≠ nfa.nodes.size
⊢ ∃ cs₁ cs₂,
    cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case εStep.h
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
k : ℕ
cs' : List Char
assm₂ : k = nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
path : (↑result).pathIn nfa.nodes.size (rStart_of eq) k cs'
ih✝ :
  rStart_of eq < (↑result).nodes.size →
    k = nfa.nodes.size →
      if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
ih :
  if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
step : rStart_of eq ∈ (↑result)[nfa.nodes.size].εStep
this : rStart_of eq ≠ nfa.nodes.size
⊢ ∃ cs₁ cs₂,
    cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Tactic:
simp [this] at ih
Proof state after:
case εStep.h
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
k : ℕ
cs' : List Char
assm₂ : k = nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
path : (↑result).pathIn nfa.nodes.size (rStart_of eq) k cs'
ih✝ :
  rStart_of eq < (↑result).nodes.size →
    k = nfa.nodes.size →
      if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
step : rStart_of eq ∈ (↑result)[nfa.nodes.size].εStep
this : rStart_of eq ≠ nfa.nodes.size
ih :
  ∃ 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₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case εStep.h
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
k : ℕ
cs' : List Char
assm₂ : k = nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
path : (↑result).pathIn nfa.nodes.size (rStart_of eq) k cs'
ih✝ :
  rStart_of eq < (↑result).nodes.size →
    k = nfa.nodes.size →
      if rStart_of eq = 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) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
step : rStart_of eq ∈ (↑result)[nfa.nodes.size].εStep
this : rStart_of eq ≠ nfa.nodes.size
ih :
  ∃ 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₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Tactic:
exact ih
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
step : j ∈ (↑result)[nfa.nodes.size].εStep
⊢ j = rStart_of eq
Tactic:
simp [node, NFA.Node.εStep] at step
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
step : j = rStart_of eq ∨ j = ↑next
⊢ j = rStart_of eq
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
step : j = rStart_of eq ∨ j = ↑next
⊢ j = rStart_of eq
Tactic:
cases step with
| inl eq => exact eq
| inr eq =>
  have : nfa.nodes.size ≤ j := le_of_pathIn_left path
  exact absurd next.isLt (Nat.not_lt_of_le (eq ▸ this))
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq✝
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq✝) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
eq : j = rStart_of eq✝
⊢ j = rStart_of eq✝
Tactic:
exact eq
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq✝
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq✝) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
eq : j = ↑next
⊢ j = rStart_of eq✝
Tactic:
have : nfa.nodes.size ≤ j := le_of_pathIn_left path
Proof state after:
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq✝
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq✝) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
eq : j = ↑next
this : nfa.nodes.size ≤ j
⊢ j = rStart_of eq✝
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
j k : ℕ
cs' : List Char
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₂ : k = nfa.nodes.size
ih :
  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₁ : nfa.nodes.size < (↑result).nodes.size
ge : nfa.nodes.size + 1 ≤ rStart_of eq✝
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq✝) ↑next
h₁ : nfa.nodes.size ≤ nfa.nodes.size
h₂ : nfa.nodes.size < (↑result).nodes.size
eq : j = ↑next
this : nfa.nodes.size ≤ j
⊢ j = rStart_of eq✝
Tactic:
exact absurd next.isLt (Nat.not_lt_of_le (eq ▸ this))
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
ih :
  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₂
nei : ¬i = nfa.nodes.size
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
have gti : nfa.nodes.size < i := Nat.lt_of_le_of_ne step.h₁ (Ne.symm nei)
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
ih :
  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₂
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
⊢ ∃ 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₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
case inl eqj =>
  have toNext : pathToNext result nfa.nodes.size (nfa.nodes.size + 1) i cs :=
    ⟨i, [], cs, rfl, .base gti, (eqj ▸ step).castStart' gti⟩
  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:
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:
case inr nej =>
  obtain ⟨cs₁, cs₂, eqs, path', loop⟩ := ih
  subst eqs
  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