internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa' : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'.nodes.size),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ →
              ∃ rStart, nfa.nodes.size + 1 ≤ rStart ∧ (↑result)[nfa.nodes.size] = Node.split rStart ↑next
Tactic:
intro placeholder compiled patched nfa' isLt inBounds property
  eq₁ eq₂ eq₃ eq₄ eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
⊢ ∃ rStart, nfa.nodes.size + 1 ≤ rStart ∧ (↑result)[nfa.nodes.size] = Node.split rStart ↑next
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
⊢ ∃ rStart, nfa.nodes.size + 1 ≤ rStart ∧ (↑result)[nfa.nodes.size] = Node.split rStart ↑next
Tactic:
exists compiled.val.start
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start ∧ (↑result)[nfa.nodes.size] = Node.split ↑(↑compiled).start ↑next
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start ∧ (↑result)[nfa.nodes.size] = Node.split ↑(↑compiled).start ↑next
Tactic:
simp [eq, eq₄, get_eq_nodes_get, eq₃]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start
Tactic:
have := ge_pushRegex_start eq₂.symm
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
this : (↑placeholder).nodes.size ≤ ↑(↑compiled).start
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
this : (↑placeholder).nodes.size ≤ ↑(↑compiled).start
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start
Tactic:
simp [eq₁] at this
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
this : nfa.nodes.size + 1 ≤ ↑(↑compiled).start
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
this : nfa.nodes.size + 1 ≤ ↑(↑compiled).start
⊢ nfa.nodes.size + 1 ≤ ↑(↑compiled).start
Tactic:
exact 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
assm₁ : i < (↑result).nodes.size
assm₂ : loopStart = nfa.nodes.size
ev : (↑result).pathIn nfa.nodes.size i loopStart cs
⊢ if i = 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) i cs₁ ∧ starLoop eq cs₂
Tactic:
induction ev with
| base h =>
  subst assm₂
  simp
| @step i j k cs cs' step path ih =>
  have ih := ih step.lt_right assm₂
  split
  case inl eqi =>
    subst eqi
    have ⟨ge, node⟩ := rStart_of_spec eq
    simp [node]
    cases step with
    | charStep _ _ step => simp [node, NFA.Node.charStep] at step
    | εStep h₁ h₂ step =>
      apply Or.inr
      have : j = rStart_of eq := by
        simp [node, NFA.Node.εStep] at step
        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))
      subst this
      simp [NFA.Node.εStep]
      have : rStart_of eq ≠ nfa.nodes.size := Nat.ne_of_gt ge
      simp [this] at ih
      exact ih
  case inr nei =>
    have gti : nfa.nodes.size < i := Nat.lt_of_le_of_ne step.h₁ (Ne.symm nei)
    split at ih
    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⟩
    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
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case base
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✝ : ℕ
h : nfa.nodes.size ≤ i✝
assm₁ : i✝ < (↑result).nodes.size
assm₂ : i✝ = nfa.nodes.size
⊢ if i✝ = 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) i✝ cs₁ ∧ starLoop eq cs₂
Tactic:
subst assm₂
Proof state after:
case base
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
h : nfa.nodes.size ≤ nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
⊢ if nfa.nodes.size = 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) nfa.nodes.size cs₁ ∧ starLoop eq cs₂
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case base
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
h : nfa.nodes.size ≤ nfa.nodes.size
assm₁ : nfa.nodes.size < (↑result).nodes.size
⊢ if nfa.nodes.size = 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) nfa.nodes.size cs₁ ∧ starLoop eq cs₂
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.starLoop.intro'
Proof state before:
case 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 : ℕ
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
⊢ if i = nfa.nodes.size then
    cs ++ cs' = [] ∨
      ∃ 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₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
have ih := ih step.lt_right assm₂
Proof state after:
case 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 : ℕ
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₂
⊢ if i = nfa.nodes.size then
    cs ++ cs' = [] ∨
      ∃ 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₁ ++ 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
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₂
eqi : i = nfa.nodes.size
⊢ cs ++ cs' = [] ∨
    ∃ cs₁ cs₂,
      cs ++ cs' = cs₁ ++ cs₂ ∧
        (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Tactic:
case inl eqi =>
  subst eqi
  have ⟨ge, node⟩ := rStart_of_spec eq
  simp [node]
  cases step with
  | charStep _ _ step => simp [node, NFA.Node.charStep] at step
  | εStep h₁ h₂ step =>
    apply Or.inr
    have : j = rStart_of eq := by
      simp [node, NFA.Node.εStep] at step
      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))
    subst this
    simp [NFA.Node.εStep]
    have : rStart_of eq ≠ nfa.nodes.size := Nat.ne_of_gt ge
    simp [this] at ih
    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
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:
case inr nei =>
  have gti : nfa.nodes.size < i := Nat.lt_of_le_of_ne step.h₁ (Ne.symm nei)
  split at ih
  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⟩
  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
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₂
eqi : i = nfa.nodes.size
⊢ cs ++ cs' = [] ∨
    ∃ cs₁ cs₂,
      cs ++ cs' = cs₁ ++ cs₂ ∧
        (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
Tactic:
subst eqi
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 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₂
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size j cs
assm₁ : nfa.nodes.size < (↑result).nodes.size
⊢ cs ++ cs' = [] ∨
    ∃ cs₁ cs₂,
      cs ++ cs' = cs₁ ++ cs₂ ∧
        (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂