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