internlm/Lean-Github huggingface dataset:
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this : i' < (↑nfa''').nodes.size
⊢ (↑nfa''')[i'] = (↑nfa'')[i']
Tactic:
simp [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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this : i' < (↑nfa''').nodes.size
⊢ (↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝))[i'] = (↑nfa'')[i']
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this : i' < (↑nfa''').nodes.size
⊢ (↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝))[i'] = (↑nfa'')[i']
Tactic:
rw [pushNode_get_lt _ lt]
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inl.inl
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this✝ : i' < (↑nfa''').nodes.size
this : (↑nfa''')[i'] = (↑nfa'')[i']
eq : ↑next = ↑(↑nfa').start
⊢ False
Tactic:
rw [eq₁] at eq
Proof state after:
case inr.h.inl.inl
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this✝ : i' < (↑nfa''').nodes.size
this : (↑nfa''')[i'] = (↑nfa'')[i']
eq : ↑next = ↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start
⊢ False
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inl.inl
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this✝ : i' < (↑nfa''').nodes.size
this : (↑nfa''')[i'] = (↑nfa'')[i']
eq : ↑next = ↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start
⊢ False
Tactic:
simp at eq
Proof state after:
case inr.h.inl.inl
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this✝ : i' < (↑nfa''').nodes.size
this : (↑nfa''')[i'] = (↑nfa'')[i']
eq : ↑next = nfa.nodes.size
⊢ False
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inl.inl
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this✝ : i' < (↑nfa''').nodes.size
this : (↑nfa''')[i'] = (↑nfa'')[i']
eq : ↑next = nfa.nodes.size
⊢ False
Tactic:
exact Nat.lt_irrefl _ (eq ▸ next.isLt)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inl.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
lt : i' < (↑nfa'').nodes.size
h₁ : (↑nfa').nodes.size ≤ i'
this✝ : i' < (↑nfa''').nodes.size
this : (↑nfa''')[i'] = (↑nfa'')[i']
ge : (↑nfa').nodes.size ≤ ↑next
⊢ False
Tactic:
exact Nat.lt_irrefl _ (Nat.lt_of_lt_of_le (Nat.lt_trans next.isLt nfa'.property) ge)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
ge : i' ≥ (↑nfa'').nodes.size
⊢ False
Tactic:
have eqStart : nfa'''.val[nfa''.val.nodes.size]'nfa'''.property = .save (2 * i) nfa''.val.start := by
  simp [eq₃]
Proof state after:
case inr.h.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
ge : i' ≥ (↑nfa'').nodes.size
eqStart : (↑nfa''')[(↑nfa'').nodes.size] = Node.save (2 * i) ↑(↑nfa'').start
⊢ False
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
ge : i' ≥ (↑nfa'').nodes.size
eqStart : (↑nfa''')[(↑nfa'').nodes.size] = Node.save (2 * i) ↑(↑nfa'').start
⊢ False
Tactic:
have h₂ := step.h₂
Proof state after:
case inr.h.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
ge : i' ≥ (↑nfa'').nodes.size
eqStart : (↑nfa''')[(↑nfa'').nodes.size] = Node.save (2 * i) ↑(↑nfa'').start
h₂ : i' < (↑nfa''').nodes.size
⊢ False
Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case inr.h.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
ge : i' ≥ (↑nfa'').nodes.size
eqStart : (↑nfa''')[(↑nfa'').nodes.size] = Node.save (2 * i) ↑(↑nfa'').start
h₂ : i' < (↑nfa''').nodes.size
⊢ False
Tactic:
simp [eq₃] at h₂
Proof state after:
case inr.h.inr
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₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
gt : nfa.nodes.size < i'
ge : i' ≥ (↑nfa'').nodes.size
eqStart : (↑nfa''')[(↑nfa'').nodes.size] = Node.save (2 * i) ↑(↑nfa'').start
h₂ : i' < (↑nfa'').nodes.size + 1
⊢ False