Theorem: Regex.NFA.matches_of_pathToNext_pushRegex (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 = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs r
Tactic:
induction r generalizing nfa next cs with
| classes cls =>
  apply pushRegex.sparse eq
  intro eq
  rw [eq] at path
  obtain ⟨i, pcs, scs, eqs, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  match step with
  | stepIn.charStep (c := c) _ _ step =>
    simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
    cases path with
    | base _ =>
      simp [eqs]
      exact .sparse cls c step
    | step step rest =>
      cases step with
      | charStep _ _ step =>
        simp [NFA.Node.charStep] at step
        have := le_of_pathIn_left rest
        exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
      | εStep _ _ step => simp [NFA.Node.εStep] at step
  | stepIn.εStep _ _ step =>
      simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
| empty =>
  apply pushRegex.empty eq
  intro eq
  rw [eq] at path
  obtain ⟨i, _, _, _, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
| epsilon =>
  apply pushRegex.epsilon eq
  intro eq
  rw [eq] at path
  obtain ⟨i, _, _, eqs, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  cases path with
  | base _ => exact eqs ▸ .epsilon
  | step step rest =>
    cases step with
    | charStep _ _ step => simp [NFA.Node.charStep] at step
    | εStep _ _ step =>
      simp [NFA.Node.εStep] at step
      have := le_of_pathIn_left rest
      exact absurd next.isLt (Nat.not_lt_of_ge (step ▸ this))
| char c =>
  apply pushRegex.char eq
  intro eq
  rw [eq] at path
  obtain ⟨i, _, _, _, path, step⟩ := path
  have : i < nfa.nodes.size + 1 := by
    have := step.h₂
    simp at this
    exact this
  have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
  cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  cases path with
  | base _ =>
    simp [*]
    exact .char c
  | step step rest =>
    cases step with
    | charStep _ _ step =>
      simp [NFA.Node.charStep] at step
      have := le_of_pathIn_left rest
      exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
    | εStep _ _ step => simp [NFA.Node.εStep] at step
| group i r ih => exact matches_of_path.group eq path ih
| alternate r₁ r₂ ih₁ ih₂ => exact matches_of_path.alternate eq path ih₁ ih₂
| concat r₁ r₂ ih₁ ih₂ => exact matches_of_path.concat eq path ih₁ ih₂
| star r ih => exact matches_of_path.star eq path ih
State after:
no goals

State before:
case classes
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
apply pushRegex.sparse eq
State after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.sparse cls ↑next) ⋯ → Expr.matches cs (Expr.classes cls)

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.sparse cls ↑next) ⋯ → Expr.matches cs (Expr.classes cls)
Tactic:
intro eq
State after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
rw [eq] at path
State after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
obtain ⟨i, pcs, scs, eqs, path, step⟩ := path
State after:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
⊢ Expr.matches cs (Expr.classes cls)

State before:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
have : i < nfa.nodes.size + 1 := by
  have := step.h₂
  simp at this
  exact this
State after:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs (Expr.classes cls)

State before:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
State after:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.classes cls)

State before:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
match step with
| stepIn.charStep (c := c) _ _ step =>
  simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  cases path with
  | base _ =>
    simp [eqs]
    exact .sparse cls c step
  | step step rest =>
    cases step with
    | charStep _ _ step =>
      simp [NFA.Node.charStep] at step
      have := le_of_pathIn_left rest
      exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
    | εStep _ _ step => simp [NFA.Node.εStep] at step
| stepIn.εStep _ _ step =>
    simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
no goals

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
⊢ i < nfa.nodes.size + 1
Tactic:
have := step.h₂
State after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1
Tactic:
simp at this
State after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Tactic:
exact this
State after:
no goals

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
c : Char
h₁✝ : nfa.nodes.size ≤ i
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step : ↑next ∈ (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯))[i].charStep c
eqs : cs = pcs ++ [c]
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = pcs ++ [c]
path : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size pcs
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step : c ∈ cls
⊢ Expr.matches cs (Expr.classes cls)

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = pcs ++ [c]
path : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size pcs
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step : c ∈ cls
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
cases path with
| base _ =>
  simp [eqs]
  exact .sparse cls c step
| step step rest =>
  cases step with
  | charStep _ _ step =>
    simp [NFA.Node.charStep] at step
    have := le_of_pathIn_left rest
    exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
  | εStep _ _ step => simp [NFA.Node.εStep] at step
State after:
no goals

State before:
case base
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step : c ∈ cls
h✝ : nfa.nodes.size ≤ nfa.nodes.size
eqs : cs = [] ++ [c]
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
simp [eqs]
State after:
case base
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step : c ∈ cls
h✝ : nfa.nodes.size ≤ nfa.nodes.size
eqs : cs = [] ++ [c]
⊢ Expr.matches [c] (Expr.classes cls)

State before:
case base
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step : c ∈ cls
h✝ : nfa.nodes.size ≤ nfa.nodes.size
eqs : cs = [] ++ [c]
⊢ Expr.matches [c] (Expr.classes cls)
Tactic:
exact .sparse cls c step
State after:
no goals

State before:
case step
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size j✝ cs₁✝
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
eqs : cs = cs₁✝ ++ cs₂✝ ++ [c]
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
cases step with
| charStep _ _ step =>
  simp [NFA.Node.charStep] at step
  have := le_of_pathIn_left rest
  exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
| εStep _ _ step => simp [NFA.Node.εStep] at step
State after:
no goals

State before:
case step.charStep
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝¹ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯))[nfa.nodes.size].charStep c✝
eqs : cs = [c✝] ++ cs₂✝ ++ [c]
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
simp [NFA.Node.charStep] at step
State after:
case step.charStep
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝¹ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = [c✝] ++ cs₂✝ ++ [c]
step : c✝ ∈ cls ∧ j✝ = ↑next
⊢ Expr.matches cs (Expr.classes cls)

State before:
case step.charStep
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝¹ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = [c✝] ++ cs₂✝ ++ [c]
step : c✝ ∈ cls ∧ j✝ = ↑next
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
have := le_of_pathIn_left rest
State after:
case step.charStep
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝¹ this✝ h₁✝¹ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = [c✝] ++ cs₂✝ ++ [c]
step : c✝ ∈ cls ∧ j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs (Expr.classes cls)

State before:
case step.charStep
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝¹ this✝ h₁✝¹ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
eqs : cs = [c✝] ++ cs₂✝ ++ [c]
step : c✝ ∈ cls ∧ j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
State after:
no goals

State before:
case step.εStep
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
scs : List Char
c : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step✝¹ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size (↑next) scs
this✝ this h₁✝¹ : True
step✝ : c ∈ cls
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯))[nfa.nodes.size].εStep
eqs : cs = [] ++ cs₂✝ ++ [c]
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
simp [NFA.Node.εStep] at step
State after:
no goals

State before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step✝ : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
h₁✝ : nfa.nodes.size ≤ i
h₂✝ : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
step : ↑next ∈ (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯))[i].εStep
eqs : cs = pcs ++ []
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
no goals

State before:
case empty
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs Expr.empty
Tactic:
apply pushRegex.empty eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode Node.fail ⋯ → Expr.matches cs Expr.empty

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode Node.fail ⋯ → Expr.matches cs Expr.empty
Tactic:
intro eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode Node.fail ⋯
⊢ Expr.matches cs Expr.empty

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode Node.fail ⋯
⊢ Expr.matches cs Expr.empty
Tactic:
rw [eq] at path
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
path : (↑(nfa.pushNode Node.fail ⋯)).pathToNext (↑next) nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) cs
eq : result = nfa.pushNode Node.fail ⋯
⊢ Expr.matches cs Expr.empty

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
path : (↑(nfa.pushNode Node.fail ⋯)).pathToNext (↑next) nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) cs
eq : result = nfa.pushNode Node.fail ⋯
⊢ Expr.matches cs Expr.empty
Tactic:
obtain ⟨i, _, _, _, path, step⟩ := path
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs Expr.empty

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs Expr.empty
Tactic:
have : i < nfa.nodes.size + 1 := by
  have := step.h₂
  simp at this
  exact this
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs Expr.empty

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs Expr.empty
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs Expr.empty

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs Expr.empty
Tactic:
cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ i < nfa.nodes.size + 1
Tactic:
have := step.h₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1
Tactic:
simp at this
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : (↑(nfa.pushNode Node.fail ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode Node.fail ⋯)).start) i w✝¹
step : (↑(nfa.pushNode Node.fail ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Tactic:
exact this
State after:
no goals

State before:
case epsilon
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.epsilon = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs Expr.epsilon
Tactic:
apply pushRegex.epsilon eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.epsilon = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → Expr.matches cs Expr.epsilon

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.epsilon = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → Expr.matches cs Expr.epsilon
Tactic:
intro eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ Expr.matches cs Expr.epsilon

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ Expr.matches cs Expr.epsilon
Tactic:
rw [eq] at path
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ Expr.matches cs Expr.epsilon

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ Expr.matches cs Expr.epsilon
Tactic:
obtain ⟨i, _, _, eqs, path, step⟩ := path
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs Expr.epsilon

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs Expr.epsilon
Tactic:
have : i < nfa.nodes.size + 1 := by
  have := step.h₂
  simp at this
  exact this
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs Expr.epsilon

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs Expr.epsilon
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs Expr.epsilon

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs Expr.epsilon
Tactic:
cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
case intro.intro.intro.intro.intro.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝ : List Char
h₂✝ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
path : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size w✝
this✝ this h₁✝ step✝ : True
eqs : cs = w✝
⊢ Expr.matches cs Expr.epsilon

State before:
case intro.intro.intro.intro.intro.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝ : List Char
h₂✝ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
path : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size w✝
this✝ this h₁✝ step✝ : True
eqs : cs = w✝
⊢ Expr.matches cs Expr.epsilon
Tactic:
cases path with
| base _ => exact eqs ▸ .epsilon
| step step rest =>
  cases step with
  | charStep _ _ step => simp [NFA.Node.charStep] at step
  | εStep _ _ step =>
    simp [NFA.Node.εStep] at step
    have := le_of_pathIn_left rest
    exact absurd next.isLt (Nat.not_lt_of_ge (step ▸ this))
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ i < nfa.nodes.size + 1
Tactic:
have := step.h₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1
Tactic:
simp at this
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
eqs : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Tactic:
exact this
State after:
no goals

State before:
case intro.intro.intro.intro.intro.εStep.base
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝ step✝ : True
h✝ : nfa.nodes.size ≤ nfa.nodes.size
eqs : cs = []
⊢ Expr.matches cs Expr.epsilon
Tactic:
exact eqs ▸ .epsilon
State after:
no goals

State before:
case intro.intro.intro.intro.intro.εStep.step
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝ step✝ : True
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size j✝ cs₁✝
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
eqs : cs = cs₁✝ ++ cs₂✝
⊢ Expr.matches cs Expr.epsilon
Tactic:
cases step with
| charStep _ _ step => simp [NFA.Node.charStep] at step
| εStep _ _ step =>
  simp [NFA.Node.εStep] at step
  have := le_of_pathIn_left rest
  exact absurd next.isLt (Nat.not_lt_of_ge (step ▸ this))
State after:
no goals

State before:
case intro.intro.intro.intro.intro.εStep.step.charStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.epsilon ↑next) ⋯))[nfa.nodes.size].charStep c✝
eqs : cs = [c✝] ++ cs₂✝
⊢ Expr.matches cs Expr.epsilon
Tactic:
simp [NFA.Node.charStep] at step
State after:
no goals

State before:
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.epsilon ↑next) ⋯))[nfa.nodes.size].εStep
eqs : cs = [] ++ cs₂✝
⊢ Expr.matches cs Expr.epsilon
Tactic:
simp [NFA.Node.εStep] at step
State after:
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
eqs : cs = [] ++ cs₂✝
step : j✝ = ↑next
⊢ Expr.matches cs Expr.epsilon

State before:
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
eqs : cs = [] ++ cs₂✝
step : j✝ = ↑next
⊢ Expr.matches cs Expr.epsilon
Tactic:
have := le_of_pathIn_left rest
State after:
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
eqs : cs = [] ++ cs₂✝
step : j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs Expr.epsilon

State before:
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
eqs : cs = [] ++ cs₂✝
step : j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs Expr.epsilon
Tactic:
exact absurd next.isLt (Nat.not_lt_of_ge (step ▸ this))
State after:
no goals

State before:
case char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.char c) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (Expr.char c)
Tactic:
apply pushRegex.char eq
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.char c) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.char c ↑next) ⋯ → Expr.matches cs (Expr.char c)

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.char c) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.char c ↑next) ⋯ → Expr.matches cs (Expr.char c)
Tactic:
intro eq
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ Expr.matches cs (Expr.char c)

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ Expr.matches cs (Expr.char c)
Tactic:
rw [eq] at path
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ Expr.matches cs (Expr.char c)

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ Expr.matches cs (Expr.char c)
Tactic:
obtain ⟨i, _, _, _, path, step⟩ := path
State after:
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs (Expr.char c)

State before:
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs (Expr.char c)
Tactic:
have : i < nfa.nodes.size + 1 := by
  have := step.h₂
  simp at this
  exact this
State after:
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs (Expr.char c)

State before:
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs (Expr.char c)
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
State after:
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.char c)

State before:
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.char c)
Tactic:
cases step <;> simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
case intro.intro.intro.intro.intro.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝ : List Char
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = w✝ ++ [c✝]
path : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size w✝
this✝ this h₁✝ : True
step✝ : c✝ = c
⊢ Expr.matches cs (Expr.char c)

State before:
case intro.intro.intro.intro.intro.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝ : List Char
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = w✝ ++ [c✝]
path : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size w✝
this✝ this h₁✝ : True
step✝ : c✝ = c
⊢ Expr.matches cs (Expr.char c)
Tactic:
cases path with
| base _ =>
  simp [*]
  exact .char c
| step step rest =>
  cases step with
  | charStep _ _ step =>
    simp [NFA.Node.charStep] at step
    have := le_of_pathIn_left rest
    exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
  | εStep _ _ step => simp [NFA.Node.εStep] at step
State after:
no goals

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ i < nfa.nodes.size + 1
Tactic:
have := step.h₂
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1
Tactic:
simp at this
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Tactic:
exact this
State after:
no goals

State before:
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
Tactic:
simp [*]
State after:
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches [c] (Expr.char c)

State before:
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches [c] (Expr.char c)
Tactic:
exact .char c
State after:
no goals

State before:
case intro.intro.intro.intro.intro.charStep.step
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size j✝ cs₁✝
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
left✝ : cs = cs₁✝ ++ cs₂✝ ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
Tactic:
cases step with
| charStep _ _ step =>
  simp [NFA.Node.charStep] at step
  have := le_of_pathIn_left rest
  exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
| εStep _ _ step => simp [NFA.Node.εStep] at step
State after:
no goals

State before:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.char c ↑next) ⋯))[nfa.nodes.size].charStep c✝
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
⊢ Expr.matches cs (Expr.char c)
Tactic:
simp [NFA.Node.charStep] at step
State after:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
⊢ Expr.matches cs (Expr.char c)

State before:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
⊢ Expr.matches cs (Expr.char c)
Tactic:
have := le_of_pathIn_left rest
State after:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs (Expr.char c)

State before:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs (Expr.char c)
Tactic:
exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
State after:
no goals

State before:
case intro.intro.intro.intro.intro.charStep.step.εStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.char c ↑next) ⋯))[nfa.nodes.size].εStep
left✝ : cs = [] ++ cs₂✝ ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
Tactic:
simp [NFA.Node.εStep] at step
State after:
no goals

State before:
case group
i : ℕ
r : Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.group i r) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (Expr.group i r)
Tactic:
exact matches_of_path.group eq path ih
State after:
no goals

State before:
case alternate
r₁ r₂ : Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
exact matches_of_path.alternate eq path ih₁ ih₂
State after:
no goals

State before:
case concat
r₁ r₂ : Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
exact matches_of_path.concat eq path ih₁ ih₂
State after:
no goals

State before:
case star
r : Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs r.star
Tactic:
exact matches_of_path.star eq path ih
State after:
no goals