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
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:
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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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_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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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
lt✝ : i✝.succ < (↑nfa'').nodes.size + 1
lt : i✝ < (↑nfa'').nodes.size
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_zero_iff_zero_lt.mpr h₁
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
lt✝ : i✝ < (↑nfa'').nodes.size
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
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
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
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
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:
exact h₂ i lt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case alternate
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 →
      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
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
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
⊢ ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
Tactic:
apply pushRegex.alternate 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 →
      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
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
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
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 }) (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⟩ → ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0