internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ patched[i] = (↑compiled).nodes[i]
Tactic:
simp [eq₃]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i] = (↑compiled).nodes[i]
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : 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
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Tactic:
simp
Proof state after:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Tactic:
exact Nat.ne_of_lt ge
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inr.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝¹ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq✝ : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
eqn : (↑result)[i] = (↑compiled)[i]
eq : ↑next = nfa.nodes.size
⊢ False
Tactic:
exact Nat.lt_irrefl _ (eq ▸ next.isLt)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inr.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) cs
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
eqn : (↑result)[i] = (↑compiled)[i]
gt : nfa.nodes.size + 1 ≤ ↑next
⊢ False
Tactic:
exact Nat.lt_irrefl _ (Nat.lt_trans gt next.isLt)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case classes
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
apply pushRegex.sparse eq
Proof state after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.sparse cls ↑next) ⋯ → Expr.matches cs (Expr.classes cls)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode (Node.sparse cls ↑next) ⋯ → Expr.matches cs (Expr.classes cls)
Tactic:
intro eq
Proof state after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
rw [eq] at path
Proof state after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
obtain ⟨i, pcs, scs, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
⊢ Expr.matches cs (Expr.classes cls)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
have : i < nfa.nodes.size + 1 := by
  have := step.h₂
  simp at this
  exact this
Proof state after:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs (Expr.classes cls)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
have : i = nfa.nodes.size := Nat.eq_of_le_of_lt_succ (le_of_pathIn_right path) this
Proof state after:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.classes cls)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this✝ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
⊢ Expr.matches cs (Expr.classes cls)
Tactic:
match step with
| stepIn.charStep (c := c) _ _ step =>
  simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
  cases path with
  | base _ =>
    simp [eqs]
    exact .sparse cls c step
  | step step rest =>
    cases step with
    | charStep _ _ step =>
      simp [NFA.Node.charStep] at step
      have := le_of_pathIn_left rest
      exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
    | εStep _ _ step => simp [NFA.Node.εStep] at step
| stepIn.εStep _ _ step =>
    simp [this, NFA.Node.charStep, NFA.Node.εStep] at *
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
⊢ i < nfa.nodes.size + 1
Tactic:
have := step.h₂
Proof state after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).nodes.size
⊢ i < nfa.nodes.size + 1
Tactic:
simp at this
Proof state after:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
cls : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.classes cls) = result
eq : result = nfa.pushNode (Node.sparse cls ↑next) ⋯
i : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path :
  (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).start)
    i pcs
step : (↑(nfa.pushNode (Node.sparse cls ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) scs
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Tactic:
exact this
Proof state after:
no goals