internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
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 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa''').start
Tactic:
rw [eq₃]
Proof state after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
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 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝)).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
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 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝)).start
Tactic:
simp
Proof state after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
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 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ (↑nfa'').nodes.size
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
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 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ (↑nfa'').nodes.size
Tactic:
apply Nat.le_of_lt (Nat.lt_trans nfa'.property nfa''.property)
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case alternate
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.alternate eq
Proof state after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
⊢ ∀ (nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa').nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
⊢ ∀ (nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa').nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro nfa₁ _ nfa₂ _ _ _ _ _ _ _ _ eq₅ eq
Proof state after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
Proof state after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa'✝, property✝⟩).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa'✝, property✝⟩).start
Tactic:
simp
Proof state after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa'✝).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa'✝).start
Tactic:
rw [eq₅]
Proof state after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝)).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝)).start
Tactic:
simp [pushNode]
Proof state after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ (↑nfa₂).nodes.size
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
start₁✝ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂✝ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁✝ ↑start₂✝).inBounds ((↑nfa₂).nodes.size + 1)
nfa'✝ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa'✝).nodes.size
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ (↑nfa₂).nodes.size
Tactic:
exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case concat
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.concat eq
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
⊢ ∀ (nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size })
    (property : nfa.nodes.size < (↑nfa₁).nodes.size),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ → result = ⟨↑nfa₁, property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
⊢ ∀ (nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size })
    (property : nfa.nodes.size < (↑nfa₁).nodes.size),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ → result = ⟨↑nfa₁, property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro nfa₂ nfa₁ _ _ eq₁ eq
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start