internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.classes r) = nfa.pushNode (Node.sparse r ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.sparse r ↑next) ⋯)).nodes.size
step :
  (∃ c, j ∈ (↑(nfa.pushNode (Node.sparse r ↑next) ⋯))[i].charStep c) ∨
    j ∈ (↑(nfa.pushNode (Node.sparse r ↑next) ⋯))[i].εStep
h₂ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp [this, NFA.Node.charStep, NFA.Node.εStep] at step
Proof state after:
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.classes r) = nfa.pushNode (Node.sparse r ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.sparse r ↑next) ⋯)).nodes.size
h₂ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
step : (∃ x, x ∈ r) ∧ j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
c : Char
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
h₂ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
step : j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
try exact .inl step
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.classes r) = nfa.pushNode (Node.sparse r ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.sparse r ↑next) ⋯)).nodes.size
h₂ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
step : (∃ x, x ∈ r) ∧ j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
try exact .inl (And.right step)
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case classes
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
apply pushRegex.epsilon eq
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case classes
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
apply pushRegex.char eq
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case classes
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
apply pushRegex.sparse eq
Proof state after:
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes r) = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
⊢ result = nfa.pushNode (Node.sparse r ↑next) ⋯ → j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
c : Char
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
h₂ : i < nfa.nodes.size + 1
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:
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.classes r) = nfa.pushNode (Node.sparse r ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.sparse r ↑next) ⋯)).nodes.size
h₂ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
step : (∃ x, x ∈ r) ∧ j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
exact .inl (And.right step)
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case group
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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
apply pushRegex.group 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)),
    nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → j = ↑next ∨ nfa.nodes.size ≤ j
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)),
    nfa' = nfa.pushNode (Node.save (2 * a✝ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
intro nfa' nfa'' nfa''' property _ _ eq₁ eq₂ eq₃ 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⟩
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
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⟩
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have get₂ (h : i < nfa''.val.nodes.size) : result.val[i] = nfa''.val[i] := by
  simp [eq, eq₃]
  rw [pushNode_get_lt _ h]
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]
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
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]
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have get₁ (h : i < nfa'.val.nodes.size) : result.val[i] = nfa'.val[i] := by
  rw [get₂ (Nat.lt_trans h nfa''.property)]
  rw [pushRegex_get_lt eq₂.symm _ h]
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]
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
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]
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
cases Nat.eq_or_lt_of_le h₁ with
| inl eq =>
  have : i < nfa'.val.nodes.size := eq ▸ nfa'.property
  rw [get₁ this] at step
  simp [eq₁, ←eq, Node.charStep, Node.εStep] at step
  exact .inl step
| inr gt =>
  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:
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⟩
h : i < (↑nfa'').nodes.size
⊢ (↑result)[i] = (↑nfa'')[i]
Tactic:
simp [eq, 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⟩
h : i < (↑nfa'').nodes.size
⊢ (↑((↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝))[i] = (↑nfa'')[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⟩
h : i < (↑nfa'').nodes.size
⊢ (↑((↑nfa'').pushNode (Node.save (2 * a✝) ↑(↑nfa'').start) inBounds'''✝))[i] = (↑nfa'')[i]
Tactic:
rw [pushNode_get_lt _ h]
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]
h : i < (↑nfa').nodes.size
⊢ (↑result)[i] = (↑nfa')[i]
Tactic:
rw [get₂ (Nat.lt_trans h nfa''.property)]
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]
h : i < (↑nfa').nodes.size
⊢ (↑nfa'')[i] = (↑nfa')[i]