internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r with eq'
Proof state after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa[i] = Node.done ↔ ↑i = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
have := done_iff_zero_pushRegex eq'.symm (by decide) h i (eq ▸ i.isLt)
Proof state after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result)[↑i] = Node.done ↔ ↑i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result)[↑i] = Node.done ↔ ↑i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
exact eq ▸ this
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ done[i] = Node.done ↔ i = 0
Tactic:
simp [NFA.done] at *
Proof state after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[i] = Node.done ↔ i = 0
Tactic:
suffices i = 0 by
  subst this
  simp
  rfl
Proof state after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ i = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ i = 0
Tactic:
simp [NFA.done] at isLt
Proof state after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i = 0
⊢ i = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i = 0
⊢ i = 0
Tactic:
match i with
| 0 => rfl
| i + 1 => contradiction
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
this : i = 0
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[i] = Node.done ↔ i = 0
Tactic:
subst this
Proof state after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done ↔ 0 = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done ↔ 0 = 0
Tactic:
simp
Proof state after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done
Tactic:
rfl
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : 0 = 0
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝¹ : Fin nfa.nodes.size
i✝ i : ℕ
isLt : i + 1 = 0
⊢ i + 1 = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.lt_zero_size_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
⊢ 0 < nfa.nodes.size
Tactic:
unfold compile at eq
Proof state after:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
⊢ 0 < nfa.nodes.size
Theorem: Regex.NFA.lt_zero_size_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
⊢ 0 < nfa.nodes.size
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r
Proof state after:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
⊢ 0 < nfa.nodes.size
Theorem: Regex.NFA.lt_zero_size_compile
Proof state before:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
⊢ 0 < nfa.nodes.size
Tactic:
have : 0 < result.val.nodes.size := Nat.zero_lt_of_lt result.property
Proof state after:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
this : 0 < (↑result).nodes.size
⊢ 0 < nfa.nodes.size
Theorem: Regex.NFA.lt_zero_size_compile
Proof state before:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
this : 0 < (↑result).nodes.size
⊢ 0 < nfa.nodes.size
Tactic:
exact eq ▸ this
Proof state after:
no goals
Theorem: Regex.NFA.lt_zero_size_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = nfa'
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
apply pushRegex.group eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = nfa'
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
⊢ ∀ (nfa'_1 : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa' // (↑nfa'_1).nodes.size < nfa'.nodes.size })
    (nfa''' : { nfa' // (↑nfa'').nodes.size < nfa'.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)),
    nfa'_1 = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds' →
      nfa'' = (↑nfa'_1).pushRegex (↑nfa'_1).start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds''' →
          nfa' = ⟨↑nfa''', property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = nfa'
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
⊢ ∀ (nfa'_1 : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa' // (↑nfa'_1).nodes.size < nfa'.nodes.size })
    (nfa''' : { nfa' // (↑nfa'').nodes.size < nfa'.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)),
    nfa'_1 = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds' →
      nfa'' = (↑nfa'_1).pushRegex (↑nfa'_1).start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds''' →
          nfa' = ⟨↑nfa''', property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
intro nfa' nfa'' nfa''' property _ _ eq₁ eq₂ eq₃ eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs
Tactic:
rw [eq]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑⟨↑nfa''', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa''', property⟩).start) cs
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑⟨↑nfa''', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa''', property⟩).start) cs
Tactic:
simp
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₃ : pathToNext nfa' next nfa.nodes.size nfa'.val.start [] := by
  have h₁ : nfa.nodes.size ≤ nfa'.val.start.val := by
    rw [eq₁]
    simp
  refine ⟨nfa'.val.start.val, [], [], rfl, .base h₁, ?_⟩
  refine .εStep h₁ nfa'.val.start.isLt ?_
  rw [eq₁]
  simp [Node.εStep]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₃ : pathToNext nfa'' next nfa.nodes.size nfa'.val.start [] := by
  apply path₃.cast
  intro i _ h₂
  exists Nat.lt_trans h₂ nfa''.property
  rw [pushRegex_get_lt eq₂.symm _ h₂]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₂ : pathToNext nfa'' nfa'.val.start nfa'.val.nodes.size nfa''.val.start cs :=
  ih eq₂.symm
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
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 : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs