internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
gt : nfa.nodes.size < i
this : i < (↑compiled).nodes.size
⊢ ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i] = (↑compiled).nodes[i]
Tactic:
rw [Array.get_set_ne]
Proof state after:
case h
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
gt : nfa.nodes.size < i
this : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case h
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
gt : nfa.nodes.size < i
this : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Tactic:
simp
Proof state after:
case h
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
gt : nfa.nodes.size < i
this : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case h
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
gt : nfa.nodes.size < i
this : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Tactic:
exact Nat.ne_of_lt gt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
gt : nfa.nodes.size < i
this✝ : i < (↑compiled).nodes.size
this : nfa'[i] = (↑compiled)[i]
⊢ i < (↑compiled).nodes.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inl
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq✝ : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).nodes.size
isLt : i < nfa.nodes.size + 1
eq : i.succ = nfa.nodes.size + 1
⊢ (↑placeholder)[i] = Node.done ↔ i = 0
Tactic:
simp at eq
Proof state after:
case inl
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq✝ : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).nodes.size
isLt : i < nfa.nodes.size + 1
eq : i = nfa.nodes.size
⊢ (↑placeholder)[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inl
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq✝ : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).nodes.size
isLt : i < nfa.nodes.size + 1
eq : i = nfa.nodes.size
⊢ (↑placeholder)[i] = Node.done ↔ i = 0
Tactic:
simp [eq₁, eq, -List.length_eq_zero]
Proof state after:
case inl
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq✝ : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).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
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq✝ : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).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
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).nodes.size
isLt : i < nfa.nodes.size + 1
lt : i.succ < nfa.nodes.size + 1
⊢ (↑placeholder)[i] = Node.done ↔ i = 0
Tactic:
have lt := Nat.lt_of_succ_lt_succ lt
Proof state after:
case inr
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).nodes.size
isLt : i < nfa.nodes.size + 1
lt✝ : i.succ < nfa.nodes.size + 1
lt : i < nfa.nodes.size
⊢ (↑placeholder)[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case inr
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).nodes.size
isLt : i < nfa.nodes.size + 1
lt✝ : i.succ < nfa.nodes.size + 1
lt : i < nfa.nodes.size
⊢ (↑placeholder)[i] = Node.done ↔ i = 0
Tactic:
simp [eq₁, pushNode_get_lt _ lt]
Proof state after:
case inr
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).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
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
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
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt✝²⟩, inBounds := inBounds }
eq : nfa.pushRegex next r.star = ⟨nfa', property⟩
i✝ : ℕ
isLt✝¹ : i✝ < nfa'.nodes.size
gt : nfa.nodes.size < i✝
this✝ : i✝ < (↑compiled).nodes.size
this : nfa'[i✝] = (↑compiled)[i✝]
i : ℕ
isLt✝ : i < (↑placeholder).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_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
have h (i : Nat) (isLt : i < NFA.done.nodes.size) : done[i] = Node.done ↔ i = 0 := by
  simp [NFA.done] at *
  suffices i = 0 by
    subst this
    simp
    rfl
  simp [NFA.done] at isLt
  match i with
  | 0 => rfl
  | i + 1 => contradiction
Proof state after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Theorem: Regex.NFA.done_iff_zero_compile
Proof state before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
unfold compile at eq
Proof state after:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0