internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.base
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
cs₂ : List Char
h✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
step : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) (↑next) cs₂
heq : (↑nfa'').nodes.size = nfa.nodes.size ∧ cs₂ = []
eqs : cs = [] ++ cs₂
this : nfa.nodes.size < (↑nfa'').nodes.size
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
Tactic:
exact (Nat.lt_irrefl _ (heq.left ▸ this)).elim
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
Tactic:
simp [eqs, heq.right]
Proof state after:
case intro.intro.intro.intro.intro.step
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) (cs₁ ++ cs₂)
Tactic:
have eqStart : nfa'''.val[nfa'''.val.start.val] = .save (2 * i) nfa''.val.start := by
  rw [eq₃]
  simp
Proof state after:
case intro.intro.intro.intro.intro.step
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) (cs₁ ++ cs₂)
Tactic:
cases step' with
| charStep _ _ step => simp [eqStart, Node.charStep] at step
| εStep _ _ step =>
  simp [eqStart, Node.εStep] at step
  subst step
  simp
  have : pathIn nfa'' nfa.nodes.size nfa''.val.start i' cs₂ := by
    apply rest.cast' (nfa''.val.start.isLt) (Nat.le_of_lt nfa'''.property)
    intro i _ h₂
    rw [eq₃, pushNode_get_lt _ h₂]
  have ⟨cs₃, cs₄, eqs, path', path''⟩ :=
    pathIn_split eq₂.symm (heq.left ▸ nfa'.property) (ge_pushRegex_start eq₂.symm) this
  cases path'' with
  | base _ =>
    simp at eqs
    exact eqs ▸ path'
  | step step rest =>
    have : nfa'.val.start.val < nfa''.val.nodes.size :=
      Nat.lt_trans nfa'.val.start.isLt nfa''.property
    have eqStart : nfa''.val[nfa'.val.start.val] = .save (2 * i + 1) next := by
      rw [pushRegex_get_lt eq₂.symm _ nfa'.val.start.isLt]
      rw [eq₁]
      simp
    have step := step.step
    simp [eqStart, Node.charStep, Node.εStep] at step
    subst step
    have := le_of_pathIn_left rest
    exact (Nat.lt_irrefl _ (Nat.lt_of_le_of_lt this next.isLt)).elim
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
⊢ (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
Tactic:
rw [eq₃]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
⊢ (↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start)
          inBounds'''✝))[↑(↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝)).start] =
    Node.save (2 * i) ↑(↑nfa'').start
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₁ cs₂ : List Char
step' : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa''').start) j cs₁
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqs : cs = cs₁ ++ cs₂ ++ cs₂✝
⊢ (↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start)
          inBounds'''✝))[↑(↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝)).start] =
    Node.save (2 * i) ↑(↑nfa'').start
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step.charStep
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step✝ : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
j : ℕ
cs₂ : List Char
rest : (↑nfa''').pathIn nfa.nodes.size j i' cs₂
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
c✝ : Char
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
step : j ∈ (↑nfa''')[↑(↑nfa''').start].charStep c✝
eqs : cs = [c✝] ++ cs₂ ++ cs₂✝
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) ([c✝] ++ cs₂)
Tactic:
simp [eqStart, Node.charStep] at step
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) ([] ++ cs₂)
Tactic:
simp
Proof state after:
case intro.intro.intro.intro.intro.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₂
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
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' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₂✝ : List Char
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂✝
heq : i' = nfa.nodes.size ∧ cs₂✝ = []
cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs✝ : cs = [] ++ cs₂ ++ cs₂✝
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
this : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) i' cs₂
cs₃ cs₄ : List Char
eqs : cs₂ = cs₃ ++ cs₄
path' : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₃
path'' : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa').start) i' cs₄
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₂
Tactic:
cases path'' with
| base _ =>
  simp at eqs
  exact eqs ▸ path'
| step step rest =>
  have : nfa'.val.start.val < nfa''.val.nodes.size :=
    Nat.lt_trans nfa'.val.start.isLt nfa''.property
  have eqStart : nfa''.val[nfa'.val.start.val] = .save (2 * i + 1) next := by
    rw [pushRegex_get_lt eq₂.symm _ nfa'.val.start.isLt]
    rw [eq₁]
    simp
  have step := step.step
  simp [eqStart, Node.charStep, Node.εStep] at step
  subst step
  have := le_of_pathIn_left rest
  exact (Nat.lt_irrefl _ (Nat.lt_of_le_of_lt this next.isLt)).elim
Proof state after:
no goals