internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case h
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
path : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑final).start) cs
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
⊢ ↑next < ↑start₂
Tactic:
apply Nat.lt_of_lt_of_le (Nat.lt_trans next.isLt nfa₁.property)
Proof state after:
case h
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
path : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑final).start) cs
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
⊢ (↑nfa₁).nodes.size ≤ ↑start₂
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case h
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
path : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑final).start) cs
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
⊢ (↑nfa₁).nodes.size ≤ ↑start₂
Tactic:
exact eq₄ ▸ ge_pushRegex_start eq₃.symm
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
path : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑final).start) cs
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
i : ℕ
x✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ (↑nfa₂)[i] = (↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds))[i]
Tactic:
rw [pushNode_get_lt]
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
path : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑final).start) cs
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
i : ℕ
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
⊢ (↑nfa₁)[i] = (↑nfa₂)[i]
Tactic:
rw [pushRegex_get_lt eq₃.symm]
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case intro.intro.intro.intro.intro.base
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
cs₂ : List Char
h✝ : nfa.nodes.size ≤ ↑(↑final).start
step : (↑final).stepIn nfa.nodes.size (↑(↑final).start) (↑next) cs₂
eqs : cs = [] ++ cs₂
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
cases step with
| charStep _ _ step => simp [NFA.Node.charStep, startNode] at step
| εStep _ _ step =>
  simp [NFA.Node.εStep, startNode] at step
  cases step <;> simp only [neStart₁, neStart₂] at *
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case intro.intro.intro.intro.intro.base.charStep
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
h✝ : nfa.nodes.size ≤ ↑(↑final).start
c✝ : Char
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
step : ↑next ∈ (↑final)[↑(↑final).start].charStep c✝
eqs : cs = [] ++ [c✝]
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
simp [NFA.Node.charStep, startNode] at step
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case intro.intro.intro.intro.intro.base.εStep
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
h✝ h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
eqs : cs = [] ++ []
step : ↑next = ↑start₁ ∨ ↑next = ↑start₂
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
cases step <;> simp only [neStart₁, neStart₂] at *
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case intro.intro.intro.intro.intro.step.charStep
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
i : ℕ
cs₂ : List Char
step✝ : (↑final).stepIn nfa.nodes.size i (↑next) cs₂
j✝ : ℕ
cs₄ : List Char
rest : (↑final).pathIn nfa.nodes.size j✝ i cs₄
c✝ : Char
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
step : j✝ ∈ (↑final)[↑(↑final).start].charStep c✝
eqs : cs = [c✝] ++ cs₄ ++ cs₂
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
simp [NFA.Node.charStep, startNode] at step
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case intro.intro.intro.intro.intro.step.εStep
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
i : ℕ
cs₂ : List Char
step✝ : (↑final).stepIn nfa.nodes.size i (↑next) cs₂
j✝ : ℕ
cs₄ : List Char
rest : (↑final).pathIn nfa.nodes.size j✝ i cs₄
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
eqs : cs = cs₄ ++ cs₂
step : j✝ = ↑start₁ ∨ j✝ = ↑start₂
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
cases step with
| inl eqs₁ =>
  rw [eqs₁] at rest
  have : pathToNext final next nfa.nodes.size nfa₁.val.start.val cs :=
    ⟨i, cs₄, cs₂, eqs, eq₂ ▸ rest, step⟩
  have : pathToNext nfa₁ next nfa.nodes.size nfa₁.val.start.val cs := by
    apply this.cast' nfa₁.val.start.isLt
      (Nat.le_of_lt (Nat.lt_trans nfa₂.property final.property))
      get₁
  exact .alternateLeft (ih₁ eq₁.symm this)
| inr eqs₂ =>
  rw [eqs₂] at rest
  have : pathToNext final next nfa.nodes.size nfa₂.val.start.val cs :=
    ⟨i, cs₄, cs₂, eqs, eq₄ ▸ rest, step⟩
  have : pathToNext nfa₂ next nfa.nodes.size nfa₂.val.start.val cs := by
    apply this.cast' nfa₂.val.start.isLt (Nat.le_of_lt final.property) get₂
  have : pathToNext nfa₂ next nfa₁.val.nodes.size nfa₂.val.start.val cs := by
    apply this.castLE (ge_pushRegex_start eq₃.symm)
    intro i j h₁ h₂ step hj
    have := eq_or_ge_of_step_pushRegex eq₃.symm h₁ h₂ step
    simp at this
    cases this with
    | inl eq =>
      exfalso
      rw [eq] at hj
      exact Nat.not_le_of_gt next.isLt hj
    | inr ge => exact ge
  exact .alternateRight (ih₂ eq₃.symm this)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
case intro.intro.intro.intro.intro.step.εStep.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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
i : ℕ
cs₂ : List Char
step : (↑final).stepIn nfa.nodes.size i (↑next) cs₂
j✝ : ℕ
cs₄ : List Char
rest : (↑final).pathIn nfa.nodes.size (↑start₁) i cs₄
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
eqs : cs = cs₄ ++ cs₂
eqs₁ : j✝ = ↑start₁
this✝ : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
exact .alternateLeft (ih₁ eq₁.symm this)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.alternate
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₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
i : ℕ
cs₂ : List Char
step : (↑final).stepIn nfa.nodes.size i (↑next) cs₂
j✝ : ℕ
cs₄ : List Char
rest : (↑final).pathIn nfa.nodes.size (↑start₁) i cs₄
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
eqs : cs = cs₄ ++ cs₂
eqs₁ : j✝ = ↑start₁
this : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
Tactic:
apply this.cast' nfa₁.val.start.isLt
  (Nat.le_of_lt (Nat.lt_trans nfa₂.property final.property))
  get₁
Proof state after:
no goals