internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inl.h
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
this : (↑nfa').nodes.size ≤ i
ih : j = ↑(↑nfa').start ∨ (↑nfa').nodes.size ≤ j
⊢ nfa.nodes.size ≤ j
Tactic:
cases ih with
| inl eq =>
  rw [eq, eq₁]
  simp
| inr ge => exact Nat.le_trans (Nat.le_of_lt nfa'.property) ge
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
⊢ (↑nfa').nodes.size ≤ i
Tactic:
simp [eq₁]
Proof state after:
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
⊢ nfa.nodes.size + 1 ≤ i
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
⊢ nfa.nodes.size + 1 ≤ i
Tactic:
exact gt
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inl.h.inl
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝¹ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq✝ : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
this : (↑nfa').nodes.size ≤ i
eq : j = ↑(↑nfa').start
⊢ nfa.nodes.size ≤ j
Tactic:
rw [eq, eq₁]
Proof state after:
case inr.inl.h.inl
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝¹ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq✝ : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
this : (↑nfa').nodes.size ≤ i
eq : j = ↑(↑nfa').start
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝)).start
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inl.h.inl
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝¹ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq✝ : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
this : (↑nfa').nodes.size ≤ i
eq : j = ↑(↑nfa').start
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝)).start
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inl.h.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
lt : i < (↑nfa'').nodes.size
this : (↑nfa').nodes.size ≤ i
ge : (↑nfa').nodes.size ≤ j
⊢ nfa.nodes.size ≤ j
Tactic:
exact Nat.le_trans (Nat.le_of_lt nfa'.property) ge
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp [eq, eq₃] at h₂
Proof state after:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
h₂ : i < (↑nfa'').nodes.size + 1
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
h₂ : i < (↑nfa'').nodes.size + 1
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have : i = nfa''.val.nodes.size := Nat.eq_of_le_of_lt_succ ge h₂
Proof state after:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
h₂ : i < (↑nfa'').nodes.size + 1
this : i = (↑nfa'').nodes.size
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
h₂ : i < (↑nfa'').nodes.size + 1
this : i = (↑nfa'').nodes.size
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp [this, eq, eq₃, Node.charStep, Node.εStep] at step
Proof state after:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
h₂ : i < (↑nfa'').nodes.size + 1
this : i = (↑nfa'').nodes.size
step : j = ↑(↑nfa'').start
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.inr
i j a✝ : ℕ
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 ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
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)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
get₂ : ∀ (h : i < (↑nfa'').nodes.size), (↑result)[i] = (↑nfa'')[i]
get₁ : ∀ (h : i < (↑nfa').nodes.size), (↑result)[i] = (↑nfa')[i]
gt : nfa.nodes.size < i
ge : i ≥ (↑nfa'').nodes.size
h₂ : i < (↑nfa'').nodes.size + 1
this : i = (↑nfa'').nodes.size
step : j = ↑(↑nfa'').start
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
exact .inr (Nat.le_trans (Nat.le_of_lt nfa'.property) (step ▸ ge_pushRegex_start eq₂.symm))
Proof state after:
no goals