internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
this : i < nfa.nodes.size + 1
⊢ i < nfa.nodes.size + 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
Tactic:
simp [*]
Proof state after:
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches [c] (Expr.char c)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.base
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
h✝ : nfa.nodes.size ≤ nfa.nodes.size
left✝ : cs = [] ++ [c✝]
⊢ Expr.matches [c] (Expr.char c)
Tactic:
exact .char c
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.step
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝ : True
step✝ : c✝ = c
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size nfa.nodes.size j✝ cs₁✝
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
left✝ : cs = cs₁✝ ++ cs₂✝ ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
Tactic:
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
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.char c ↑next) ⋯))[nfa.nodes.size].charStep c✝
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
⊢ Expr.matches cs (Expr.char c)
Tactic:
simp [NFA.Node.charStep] at step
Proof state after:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
⊢ Expr.matches cs (Expr.char c)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
⊢ Expr.matches cs (Expr.char c)
Tactic:
have := le_of_pathIn_left rest
Proof state after:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs (Expr.char c)
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.step.charStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝¹ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ : True
step✝ : c✝¹ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
c✝ : Char
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
left✝ : cs = [c✝] ++ cs₂✝ ++ [c✝¹]
step : c✝ = c ∧ j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs (Expr.char c)
Tactic:
exact absurd next.isLt (Nat.not_lt_of_ge (step.right ▸ this))
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case intro.intro.intro.intro.intro.charStep.step.εStep
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
c✝ : Char
h₂✝¹ : i < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ : True
step✝ : c✝ = c
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.char c ↑next) ⋯)).nodes.size
step : j✝ ∈ (↑(nfa.pushNode (Node.char c ↑next) ⋯))[nfa.nodes.size].εStep
left✝ : cs = [] ++ cs₂✝ ++ [c✝]
⊢ Expr.matches cs (Expr.char c)
Tactic:
simp [NFA.Node.εStep] at step
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case group
i : ℕ
r : Expr
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
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Expr.group i r) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (Expr.group i r)
Tactic:
exact matches_of_path.group eq path ih
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case alternate
r₁ r₂ : Expr
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
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (r₁.alternate r₂)
Tactic:
exact matches_of_path.alternate eq path ih₁ ih₂
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case concat
r₁ r₂ : Expr
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
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat r₂) = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
exact matches_of_path.concat eq path ih₁ ih₂
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_pushRegex
Proof state before:
case star
r : Expr
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
next : Fin nfa.nodes.size
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
⊢ Expr.matches cs r.star
Tactic:
exact matches_of_path.star eq path ih
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Expr.matches cs r
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r
Proof state after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ Expr.matches cs r
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ Expr.matches cs r
Tactic:
have : nfa = result.val := by
  rw [←eq]
  rfl
Proof state after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
this : nfa = ↑result
⊢ Expr.matches cs r
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
this : nfa = ↑result
⊢ Expr.matches cs r
Tactic:
rw [this] at path
Proof state after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
path : (↑result).pathToNext 0 1 (↑(↑result).start) cs
this : nfa = ↑result
⊢ Expr.matches cs r
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
path : (↑result).pathToNext 0 1 (↑(↑result).start) cs
this : nfa = ↑result
⊢ Expr.matches cs r
Tactic:
exact matches_of_pathToNext_pushRegex rfl path
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa = ↑result
Tactic:
rw [←eq]
Proof state after:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ compile r = ↑result
Theorem: Regex.NFA.matches_of_pathToNext_compile
Proof state before:
r : Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathToNext 0 1 (↑nfa.start) cs
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
⊢ compile r = ↑result
Tactic:
rfl
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.h₁
Proof state before:
nfa : NFA
start i j : ℕ
cs : List Char
step : nfa.stepIn start i j cs
⊢ start ≤ i
Tactic:
cases step with
| charStep h₁ _ _ => exact h₁
| εStep h₁ _ _ => exact h₁
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.h₁
Proof state before:
case charStep
nfa : NFA
start i j : ℕ
c✝ : Char
h₁ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
⊢ start ≤ i
Tactic:
exact h₁
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.h₁
Proof state before:
case εStep
nfa : NFA
start i j : ℕ
h₁ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].εStep
⊢ start ≤ i
Tactic:
exact h₁
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.h₂
Proof state before:
nfa : NFA
start i j : ℕ
cs : List Char
step : nfa.stepIn start i j cs
⊢ i < nfa.nodes.size
Tactic:
cases step with
| charStep _ h₂ _ => exact h₂
| εStep _ h₂ _ => exact h₂
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.h₂
Proof state before:
case charStep
nfa : NFA
start i j : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
⊢ i < nfa.nodes.size
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.h₂
Proof state before:
case εStep
nfa : NFA
start i j : ℕ
h₁✝ : start ≤ i
h₂ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].εStep
⊢ i < nfa.nodes.size
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.step
Proof state before:
nfa : NFA
start i j : ℕ
cs : List Char
step : nfa.stepIn start i j cs
⊢ (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep
Tactic:
cases step with
| charStep _ _ step => exact .inl ⟨_, step⟩
| εStep _ _ step => exact .inr step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.step
Proof state before:
case charStep
nfa : NFA
start i j : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep
Tactic:
exact .inl ⟨_, step⟩
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.step
Proof state before:
case εStep
nfa : NFA
start i j : ℕ
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep
Tactic:
exact .inr step
Proof state after:
no goals
Theorem: Regex.NFA.le_of_stepIn
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step : nfa.stepIn start i j cs
⊢ start ≤ i
Tactic:
cases step with
| charStep h₁ => exact h₁
| εStep h₁ => exact h₁
Proof state after:
no goals
Theorem: Regex.NFA.le_of_stepIn
Proof state before:
case charStep
nfa : NFA
i j start : ℕ
c✝ : Char
h₁ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
⊢ start ≤ i
Tactic:
exact h₁
Proof state after:
no goals
Theorem: Regex.NFA.le_of_stepIn
Proof state before:
case εStep
nfa : NFA
i j start : ℕ
h₁ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].εStep
⊢ start ≤ i
Tactic:
exact h₁
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.lt_right
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step : nfa.stepIn start i j cs
⊢ j < nfa.nodes.size
Tactic:
match step.step with
| .inl ⟨_, step⟩ => exact lt_of_charStep step
| .inr step => exact lt_of_εStep step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.lt_right
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step✝ : nfa.stepIn start i j cs
w✝ : Char
step : j ∈ nfa[i].charStep w✝
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_charStep step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.lt_right
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step✝ : nfa.stepIn start i j cs
step : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_εStep step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.castStart'
Proof state before:
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ i
step : nfa.stepIn start i j cs
⊢ nfa.stepIn start' i j cs
Tactic:
cases step with
| charStep h₁ h₂ step => exact .charStep le h₂ step
| εStep h₁ h₂ step => exact .εStep le h₂ step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.castStart'
Proof state before:
case charStep
i j : ℕ
nfa : NFA
start start' : ℕ
le : start' ≤ i
c✝ : Char
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ nfa.stepIn start' i j [c✝]
Tactic:
exact .charStep le h₂ step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.castStart'
Proof state before:
case εStep
i j : ℕ
nfa : NFA
start start' : ℕ
le : start' ≤ i
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.stepIn start' i j []
Tactic:
exact .εStep le h₂ step
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.cast
Proof state before:
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
step : nfa.stepIn start i j cs
h : i < nfa'.nodes.size
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j cs
Tactic:
cases step with
| charStep h₁ h₂ step =>
  exact .charStep h₁ h (eq ▸ step)
| εStep h₁ h₂ step =>
  exact .εStep h₁ h (eq ▸ step)
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.cast
Proof state before:
case charStep
i j : ℕ
nfa nfa' : NFA
start : ℕ
h : i < nfa'.nodes.size
c✝ : Char
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j [c✝]
Tactic:
exact .charStep h₁ h (eq ▸ step)
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.cast
Proof state before:
case εStep
i j : ℕ
nfa nfa' : NFA
start : ℕ
h : i < nfa'.nodes.size
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j []
Tactic:
exact .εStep h₁ h (eq ▸ step)
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_or_singleton
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
h : nfa.stepIn start i j cs
⊢ cs = [] ∨ ∃ c, cs = [c]
Tactic:
cases h with
| εStep => exact .inl rfl
| charStep => exact .inr ⟨_, rfl⟩
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_or_singleton
Proof state before:
case εStep
nfa : NFA
i j start : ℕ
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].εStep
⊢ [] = [] ∨ ∃ c, [] = [c]
Tactic:
exact .inl rfl
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_or_singleton
Proof state before:
case charStep
nfa : NFA
i j start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
⊢ [c✝] = [] ∨ ∃ c, [c✝] = [c]
Tactic:
exact .inr ⟨_, rfl⟩
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
h : nfa.stepIn start i j (cs ++ [c])
⊢ cs = []
Tactic:
generalize h' : cs ++ [c] = cs' at h
Proof state after:
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h' : cs ++ [c] = cs'
h : nfa.stepIn start i j cs'
⊢ cs = []
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h' : cs ++ [c] = cs'
h : nfa.stepIn start i j cs'
⊢ cs = []
Tactic:
cases h with
| εStep => simp at h'
| charStep =>
  cases cs with
  | nil => rfl
  | cons _ _ =>
    have := congrArg List.length h'
    simp at this
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
case εStep
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].εStep
h' : cs ++ [c] = []
⊢ cs = []
Tactic:
simp at h'
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
case charStep
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
h' : cs ++ [c] = [c✝]
⊢ cs = []
Tactic:
cases cs with
| nil => rfl
| cons _ _ =>
  have := congrArg List.length h'
  simp at this
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
case charStep.nil
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
h' : [] ++ [c] = [c✝]
⊢ [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
⊢ head✝ :: tail✝ = []
Tactic:
have := congrArg List.length h'
Proof state after:
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
this : (head✝ :: tail✝ ++ [c]).length = [c✝].length
⊢ head✝ :: tail✝ = []
Theorem: Regex.NFA.stepIn.nil_of_snoc
Proof state before:
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
this : (head✝ :: tail✝ ++ [c]).length = [c✝].length
⊢ head✝ :: tail✝ = []
Tactic:
simp at this
Proof state after:
no goals
Theorem: Regex.NFA.le_of_pathIn_left
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
path : nfa.pathIn start i j cs
⊢ start ≤ i
Tactic:
cases path with
| base h => exact h
| step step _ => exact le_of_stepIn step
Proof state after:
no goals
Theorem: Regex.NFA.le_of_pathIn_left
Proof state before:
case base
nfa : NFA
i start : ℕ
h : start ≤ i
⊢ start ≤ i
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.NFA.le_of_pathIn_left
Proof state before:
case step
nfa : NFA
i j start j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ j cs₂✝
⊢ start ≤ i
Tactic:
exact le_of_stepIn step
Proof state after:
no goals
Theorem: Regex.NFA.le_of_pathIn_right
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
path : nfa.pathIn start i j cs
⊢ start ≤ j
Tactic:
induction path with
| base h => exact h
| step _ _ ih => exact ih
Proof state after:
no goals