internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
nlt : ¬i < (↑nfa₂).nodes.size
eq : ↑next = ↑(↑nfa₂).start
⊢ ↑next < ↑next
Tactic:
have := ge_pushRegex_start eq₂.symm
Proof state after:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
nlt : ¬i < (↑nfa₂).nodes.size
eq : ↑next = ↑(↑nfa₂).start
this : nfa.nodes.size ≤ ↑(↑nfa₂).start
⊢ ↑next < ↑next
Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
nlt : ¬i < (↑nfa₂).nodes.size
eq : ↑next = ↑(↑nfa₂).start
this : nfa.nodes.size ≤ ↑(↑nfa₂).start
⊢ ↑next < ↑next
Tactic:
calc
  _ < nfa.nodes.size := next.isLt
  _ ≤ nfa₂.val.start := this
  _ = next := eq.symm
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
nlt : ¬i < (↑nfa₂).nodes.size
ge : (↑nfa₂).nodes.size ≤ ↑next
⊢ ↑next < ↑next
Tactic:
calc
  _ < nfa.nodes.size := next.isLt
  _ < nfa₂.val.nodes.size := nfa₂.property
  _ ≤ next := ge
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂✝ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
lti : i < (↑nfa₂).nodes.size
cs₃ cs₄ : List Char
eqs' : cs₁ = cs₃ ++ cs₄
path₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) (↑nfa₂).nodes.size (↑(↑nfa₁).start) cs₃
path₂ : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
m₁ : Expr.matches cs₃ r₁
step₂ : (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
⊢ (↑nfa₂).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
Tactic:
apply path₂.cast' nfa₂.val.start.isLt (Nat.le_of_lt nfa₁.property) get
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
lti : i < (↑nfa₂).nodes.size
cs₃ cs₄ : List Char
eqs' : cs₁ = cs₃ ++ cs₄
path₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) (↑nfa₂).nodes.size (↑(↑nfa₁).start) cs₃
path₂ : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
m₁ : Expr.matches cs₃ r₁
⊢ (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
Tactic:
apply step₂.cast lti
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
lti : i < (↑nfa₂).nodes.size
cs₃ cs₄ : List Char
eqs' : cs₁ = cs₃ ++ cs₄
path₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) (↑nfa₂).nodes.size (↑(↑nfa₁).start) cs₃
path₂ : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
m₁ : Expr.matches cs₃ r₁
⊢ (↑nfa₁)[i] = (↑nfa₂)[i]
Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = 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₁
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₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
i : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₁).start) i cs₁
step₂ : (↑nfa₁).stepIn nfa.nodes.size i (↑next) cs₂
lti : i < (↑nfa₂).nodes.size
cs₃ cs₄ : List Char
eqs' : cs₁ = cs₃ ++ cs₄
path₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) (↑nfa₂).nodes.size (↑(↑nfa₁).start) cs₃
path₂ : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
m₁ : Expr.matches cs₃ r₁
⊢ (↑nfa₁)[i] = (↑nfa₂)[i]
Tactic:
rw [get i step₂.h₁ lti]
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
⊢ Expr.matches cs r.star
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
⊢ ∀ (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⟩ → Expr.matches cs r.star
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
⊢ ∀ (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⟩ → Expr.matches cs r.star
Tactic:
intro placeholder compiled patched nfa' isLt inBounds property
  eq₁ eq₂ eq₃ eq₄ 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
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⟩
⊢ Expr.matches cs r.star
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
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⟩
⊢ Expr.matches cs r.star
Tactic:
obtain ⟨i, cs₁, cs₂, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
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
eqs : cs = cs₁ ++ cs₂
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) i cs₁
step : (↑result).stepIn nfa.nodes.size i (↑next) cs₂
⊢ Expr.matches cs r.star
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case intro.intro.intro.intro.intro
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
eqs : cs = cs₁ ++ cs₂
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) i cs₁
step : (↑result).stepIn nfa.nodes.size i (↑next) cs₂
⊢ Expr.matches cs r.star
Tactic:
have eqis := eq_of_step_next eq step
Proof state after:
case intro.intro.intro.intro.intro
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
eqs : cs = cs₁ ++ cs₂
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) i cs₁
step : (↑result).stepIn nfa.nodes.size i (↑next) cs₂
eqis : i = nfa.nodes.size ∧ cs₂ = []
⊢ Expr.matches cs r.star
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case intro.intro.intro.intro.intro
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
eqs : cs = cs₁ ++ cs₂
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) i cs₁
step : (↑result).stepIn nfa.nodes.size i (↑next) cs₂
eqis : i = nfa.nodes.size ∧ cs₂ = []
⊢ Expr.matches cs r.star
Tactic:
simp [eqis] at path
Proof state after:
case intro.intro.intro.intro.intro
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
eqs : cs = cs₁ ++ cs₂
step : (↑result).stepIn nfa.nodes.size i (↑next) cs₂
eqis : i = nfa.nodes.size ∧ cs₂ = []
path : (↑result).pathIn nfa.nodes.size (↑(↑result).start) nfa.nodes.size cs₁
⊢ Expr.matches cs r.star