internlm/Lean-Github huggingface dataset:
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]
h : i < (↑nfa').nodes.size
⊢ (↑nfa'')[i] = (↑nfa')[i]
Tactic:
rw [pushRegex_get_lt eq₂.symm _ h]
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case 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]
eq : nfa.nodes.size = i
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have : i < nfa'.val.nodes.size := eq ▸ nfa'.property
Proof state after:
case 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]
eq : nfa.nodes.size = i
this : i < (↑nfa').nodes.size
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case 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]
eq : nfa.nodes.size = i
this : i < (↑nfa').nodes.size
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
rw [get₁ this] at step
Proof state after:
case 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
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]
eq : nfa.nodes.size = i
this : i < (↑nfa').nodes.size
step : (∃ c, j ∈ (↑nfa')[i].charStep c) ∨ j ∈ (↑nfa')[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case 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
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]
eq : nfa.nodes.size = i
this : i < (↑nfa').nodes.size
step : (∃ c, j ∈ (↑nfa')[i].charStep c) ∨ j ∈ (↑nfa')[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp [eq₁, ←eq, Node.charStep, Node.εStep] at step
Proof state after:
case 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
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]
eq : nfa.nodes.size = i
this : i < (↑nfa').nodes.size
step : j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case 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
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]
eq : nfa.nodes.size = i
this : i < (↑nfa').nodes.size
step : j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
exact .inl step
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case 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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
cases Nat.lt_or_ge i nfa''.val.nodes.size with
| inl lt =>
  have : nfa'.val.nodes.size ≤ i := by
    simp [eq₁]
    exact gt
  have ih := ih eq₂.symm this lt (get₂ lt ▸ step)
  apply Or.inr
  cases ih with
  | inl eq =>
    rw [eq, eq₁]
    simp
  | inr ge => exact Nat.le_trans (Nat.le_of_lt nfa'.property) ge
| inr ge =>
  simp [eq, eq₃] at h₂
  have : i = nfa''.val.nodes.size := Nat.eq_of_le_of_lt_succ ge h₂
  simp [this, eq, eq₃, Node.charStep, Node.εStep] at step
  exact .inr (Nat.le_trans (Nat.le_of_lt nfa'.property) (step ▸ ge_pushRegex_start eq₂.symm))
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have : nfa'.val.nodes.size ≤ i := by
  simp [eq₁]
  exact gt
Proof state after:
case inr.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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have ih := ih eq₂.symm this lt (get₂ lt ▸ step)
Proof state after:
case inr.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
ih : j = ↑(↑nfa').start ∨ (↑nfa').nodes.size ≤ j
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inr.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
ih : j = ↑(↑nfa').start ∨ (↑nfa').nodes.size ≤ j
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
apply Or.inr
Proof state after:
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