internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt : i < (↑nfa''').nodes.size
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Tactic:
simp [eq₃] at isLt
Proof state after:
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Tactic:
cases Nat.eq_or_lt_of_le isLt with
| inl eq =>
  simp at eq
  simp [eq₃, eq, -List.length_eq_zero]
  exact Nat.ne_of_gt (Nat.zero_lt_of_lt nfa''.property)
| inr lt =>
  have lt := Nat.lt_of_succ_lt_succ lt
  simp [eq₃, pushNode_get_lt _ lt]
  apply ih eq₂.symm (Nat.zero_lt_of_lt nfa'.property) ?_ i lt
  intro i isLt
  simp [eq₁] at isLt
  cases Nat.eq_or_lt_of_le isLt with
  | inl eq =>
    simp at eq
    simp [eq₁, eq, -List.length_eq_zero]
    exact Nat.ne_zero_iff_zero_lt.mpr h₁
  | inr lt =>
    have lt := Nat.lt_of_succ_lt_succ lt
    simp [eq₁, pushNode_get_lt _ lt]
    exact h₂ i lt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inl
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
eq : i.succ = (↑nfa'').nodes.size + 1
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Tactic:
simp at eq
Proof state after:
case inl
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
eq : i = (↑nfa'').nodes.size
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inl
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
eq : i = (↑nfa'').nodes.size
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Tactic:
simp [eq₃, eq, -List.length_eq_zero]
Proof state after:
case inl
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
eq : i = (↑nfa'').nodes.size
⊢ ¬(↑nfa'').nodes.size = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inl
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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✝ : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
eq : i = (↑nfa'').nodes.size
⊢ ¬(↑nfa'').nodes.size = 0
Tactic:
exact Nat.ne_of_gt (Nat.zero_lt_of_lt nfa''.property)
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inr
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt : i.succ < (↑nfa'').nodes.size + 1
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Tactic:
have lt := Nat.lt_of_succ_lt_succ lt
Proof state after:
case inr
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt✝ : i.succ < (↑nfa'').nodes.size + 1
lt : i < (↑nfa'').nodes.size
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inr
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt✝ : i.succ < (↑nfa'').nodes.size + 1
lt : i < (↑nfa'').nodes.size
⊢ (↑nfa''')[i] = Node.done ↔ i = 0
Tactic:
simp [eq₃, pushNode_get_lt _ lt]
Proof state after:
case inr
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt✝ : i.succ < (↑nfa'').nodes.size + 1
lt : i < (↑nfa'').nodes.size
⊢ (↑nfa'')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inr
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt✝ : i.succ < (↑nfa'').nodes.size + 1
lt : i < (↑nfa'').nodes.size
⊢ (↑nfa'')[i] = Node.done ↔ i = 0
Tactic:
apply ih eq₂.symm (Nat.zero_lt_of_lt nfa'.property) ?_ i lt
Proof state after:
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt✝ : i.succ < (↑nfa'').nodes.size + 1
lt : i < (↑nfa'').nodes.size
⊢ ∀ (i : ℕ) (isLt : i < (↑nfa').nodes.size), (↑nfa')[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i : ℕ
isLt✝ : i < (↑nfa''').nodes.size
isLt : i < (↑nfa'').nodes.size + 1
lt✝ : i.succ < (↑nfa'').nodes.size + 1
lt : i < (↑nfa'').nodes.size
⊢ ∀ (i : ℕ) (isLt : i < (↑nfa').nodes.size), (↑nfa')[i] = Node.done ↔ i = 0
Tactic:
intro i isLt
Proof state after:
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 →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next (Data.Expr.group a✝ r) = ⟨↑nfa''', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < (↑nfa''').nodes.size
isLt✝ : i✝ < (↑nfa'').nodes.size + 1
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
i : ℕ
isLt : i < (↑nfa').nodes.size
⊢ (↑nfa')[i] = Node.done ↔ i = 0