Theorem: Regex.NFA.pathIn_split (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 }
i' i : ℕ
cs : List Char
start : ℕ
eq : nfa.pushRegex next r = result
assm₁ : i' < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
path : (↑result).pathIn start i i' cs
⊢ ∃ cs₁ cs₂, cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) i' cs₂
Tactic:
induction path with
| base _ => exact absurd assm₁ (Nat.not_lt_of_le assm₂)
| @step i j k cs cs' step rest ih =>
  have := eq_or_ge_of_step_pushRegex eq assm₂ step.h₂ step.step
  cases this with
  | inl eq =>
    simp [eq] at step rest
    have pathToNext : pathToNext result next nfa.nodes.size i cs :=
      ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
    exact ⟨cs, cs', rfl, pathToNext, rest⟩
  | inr ge =>
    obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
    exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
State after:
no goals

State before:
case base
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i : ℕ
cs : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i✝ : ℕ
h✝ : start ≤ i✝
assm₁ : i✝ < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i✝
⊢ ∃ cs₁ cs₂,
    [] = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i✝ cs₁ ∧ (↑result).pathIn start (↑next) i✝ cs₂
Tactic:
exact absurd assm₁ (Nat.not_lt_of_le assm₂)
State after:
no goals

State before:
case step
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
have := eq_or_ge_of_step_pushRegex eq assm₂ step.h₂ step.step
State after:
case step
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
this : j = ↑next ∨ nfa.nodes.size ≤ j
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂

State before:
case step
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
this : j = ↑next ∨ nfa.nodes.size ≤ j
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
cases this with
| inl eq =>
  simp [eq] at step rest
  have pathToNext : pathToNext result next nfa.nodes.size i cs :=
    ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
  exact ⟨cs, cs', rfl, pathToNext, rest⟩
| inr ge =>
  obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
  exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
State after:
no goals

State before:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
simp [eq] at step rest
State after:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂

State before:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
have pathToNext : pathToNext result next nfa.nodes.size i cs :=
  ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
State after:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size i cs
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂

State before:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size i cs
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
exact ⟨cs, cs', rfl, pathToNext, rest⟩
State after:
no goals

State before:
case step.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
State after:
case step.inr.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size j cs₁
pathIn : (↑result).pathIn start (↑next) k cs₂
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂

State before:
case step.inr.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size j cs₁
pathIn : (↑result).pathIn start (↑next) k cs₂
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size j cs₁
pathIn : (↑result).pathIn start (↑next) k cs₂
⊢ cs ++ cs' = cs ++ cs₁ ++ cs₂
Tactic:
simp [eqs]
State after:
no goals