internlm/Lean-Github huggingface dataset:
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs✝ = cs₁
loop : starLoop eq cs₁
cs : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
mem : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
this : ↑(↑compiled).start = rStart_of eq
j : ℕ
h₁ : nfa.nodes.size + 1 ≤ j
h₂✝ : j < (↑result).nodes.size
h₂ : j < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = j
Tactic:
exact Nat.ne_of_lt h₁
Proof state after:
no goals
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ starLoop eq cs₁
Tactic:
apply starLoop.intro 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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
Tactic:
suffices result.val.start = nfa.nodes.size by
  rw [this] at path
  exact path
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ ↑(↑result).start = nfa.nodes.size
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ ↑(↑result).start = nfa.nodes.size
Tactic:
rw [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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ ↑(↑⟨nfa', property⟩).start = nfa.nodes.size
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ ↑(↑⟨nfa', property⟩).start = nfa.nodes.size
Tactic:
simp
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ ↑nfa'.start = nfa.nodes.size
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
⊢ ↑nfa'.start = nfa.nodes.size
Tactic:
rw [eq₄]
Proof state after:
no goals
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
this : ↑(↑result).start = nfa.nodes.size
⊢ (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
Tactic:
rw [this] at path
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
this : ↑(↑result).start = nfa.nodes.size
⊢ (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs = cs₁
this : ↑(↑result).start = nfa.nodes.size
⊢ (↑result).pathIn nfa.nodes.size nfa.nodes.size nfa.nodes.size cs₁
Tactic:
exact path
Proof state after:
no goals
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs✝ = cs₁
loop : starLoop eq cs₁
cs : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
this : (↑result)[nfa.nodes.size] = Node.split ↑(↑compiled).start ↑next
mem : ↑(↑compiled).start = rStart_of eq
⊢ ↑(↑compiled).start = rStart_of eq
Tactic:
exact mem
Proof state after:
no goals
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
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
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⟩
i : ℕ
cs₁ cs₂ : List Char
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
step : (↑result).stepIn nfa.nodes.size nfa.nodes.size ↑next []
eqs : cs✝ = cs₁
loop : starLoop eq cs₁
cs : List Char
path' : (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
mem : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
⊢ (↑result)[nfa.nodes.size] = Node.split ↑(↑compiled).start ↑next
Tactic:
simp [eq', eq₄, get_eq_nodes_get, eq₃]
Proof state after:
no goals
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
⊢ i = nfa.nodes.size ∧ cs = []
Tactic:
apply pushRegex.star 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),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ → i = nfa.nodes.size ∧ cs = []