internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa₁, property✝⟩).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa₁, property✝⟩).start
Tactic:
simp
Proof state after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa₁).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa₁).start
Tactic:
exact Nat.le_trans (Nat.le_of_lt nfa₂.property) (ih₁ eq₁.symm)
Proof state after:
no goals
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
case star
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.star eq
Proof state after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa' : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'.nodes.size),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa' : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'.nodes.size),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro _ _ _ nfa' _ _ _ _ _ _ eq₄ eq
Proof state after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
Proof state after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨nfa', property✝⟩).start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨nfa', property✝⟩).start
Tactic:
simp
Proof state after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑nfa'.start
Theorem: Regex.NFA.ge_pushRegex_start
Proof state before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
placeholder✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled✝ : { nfa' // (↑placeholder✝).nodes.size < nfa'.nodes.size }
patched✝ : Array Node
nfa' : NFA
isLt✝ : nfa.nodes.size < patched✝.size
inBounds✝ : ∀ (i : Fin patched✝.size), patched✝[↑i].inBounds patched✝.size
property✝ : nfa.nodes.size < nfa'.nodes.size
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑nfa'.start
Tactic:
rw [eq₄]
Proof state after:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case empty
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = 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.empty eq
Proof state after:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = 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.fail ⋯ → j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = 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.fail ⋯ → j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
intro eq
Proof state after:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.empty = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
eq : result = nfa.pushNode Node.fail ⋯
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.empty = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
step : (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep
eq : result = nfa.pushNode Node.fail ⋯
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
subst eq
Proof state after:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp at h₂
Proof state after:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂✝ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
h₂ : i < nfa.nodes.size + 1
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂✝ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
h₂ : i < nfa.nodes.size + 1
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ h₁ h₂
Proof state after:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂✝ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
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:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂✝ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[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:
no goals
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case epsilon
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = 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:
try apply pushRegex.epsilon eq
Proof state after:
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = 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.epsilon ↑next) ⋯ → j = ↑next ∨ nfa.nodes.size ≤ j
Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case char
i j : ℕ
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = 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:
try apply pushRegex.char eq
Proof state after:
i j : ℕ
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = 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.char c ↑next) ⋯ → j = ↑next ∨ nfa.nodes.size ≤ j
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:
try 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 : ℕ
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
Tactic:
intro 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
eq : 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 : ℕ
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
eq : result = nfa.pushNode (Node.sparse r ↑next) ⋯
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
subst eq
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
step :
  (∃ c, j ∈ (↑(nfa.pushNode (Node.sparse r ↑next) ⋯))[i].charStep c) ∨
    j ∈ (↑(nfa.pushNode (Node.sparse r ↑next) ⋯))[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp at h₂
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
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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
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
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ h₁ h₂
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
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