internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ (↑(done.pushRegex ⟨0, ⋯⟩ r)).nodes.size = nfa.nodes.size
Tactic:
simp [←eq, compile]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ nfa[0] = Node.done
Tactic:
simp [←eq]
Proof state after:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (compile r)[0] = Node.done
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (compile r)[0] = Node.done
Tactic:
unfold compile
Proof state after:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (↑(done.pushRegex ⟨0, compile.proof_1⟩ r))[0] = Node.done
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (↑(done.pushRegex ⟨0, compile.proof_1⟩ r))[0] = Node.done
Tactic:
rw [pushRegex_get_lt rfl 0 (by decide)]
Proof state after:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ done[0] = Node.done
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ done[0] = Node.done
Tactic:
rfl
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case inr
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
gt : 0 < j
⊢ 0 < j
Tactic:
exact gt
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathIn
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
have : 0 < nfa.start.val := by
  rw [←eq, compile]
  exact ge_pushRegex_start (rfl : NFA.done.pushRegex _ r = _)
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
this : 0 < ↑nfa.start
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Theorem: Regex.NFA.pathToNext_of_compile_of_pathIn
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
this : 0 < ↑nfa.start
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
exact pathToNext_of_compile_of_pathInAux eq this rfl path
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathIn
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑nfa.start
Tactic:
rw [←eq, compile]
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑(↑(done.pushRegex ⟨0, compile.proof_1⟩ r)).start
Theorem: Regex.NFA.pathToNext_of_compile_of_pathIn
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑(↑(done.pushRegex ⟨0, compile.proof_1⟩ r)).start
Tactic:
exact ge_pushRegex_start (rfl : NFA.done.pushRegex _ r = _)
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_εClosure_right
Proof state before:
nfa : NFA
i j : ℕ
lt : i < nfa.nodes.size
h : j ∈ nfa.εClosure i
⊢ j < nfa.nodes.size
Tactic:
induction h with
| base => exact lt
| @step i j _ step _ ih =>
  have : j < nfa.nodes.size := by
    simp [εStep] at step
    split at step <;> exact lt_of_εStep step
  exact ih this
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_εClosure_right
Proof state before:
case base
nfa : NFA
i j i✝ : ℕ
lt : i✝ < nfa.nodes.size
⊢ i✝ < nfa.nodes.size
Tactic:
exact lt
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_εClosure_right
Proof state before:
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
have : j < nfa.nodes.size := by
  simp [εStep] at step
  split at step <;> exact lt_of_εStep step
Proof state after:
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Theorem: Regex.NFA.lt_of_εClosure_right
Proof state before:
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
exact ih this
Proof state after:
no goals
Theorem: Regex.NFA.lt_of_εClosure_right
Proof state before:
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
simp [εStep] at step
Proof state after:
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ if h : i < nfa.nodes.size then nfa[i].εStep else ∅
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Theorem: Regex.NFA.lt_of_εClosure_right
Proof state before:
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ if h : i < nfa.nodes.size then nfa[i].εStep else ∅
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
split at step <;> exact lt_of_εStep step
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_snoc
Proof state before:
j i k : ℕ
nfa : NFA
cls : j ∈ nfa.εClosure i
step : k ∈ nfa.εStep j
⊢ k ∈ nfa.εClosure i
Tactic:
induction cls with
| base => exact .step step .base
| step step' _ ih => exact εClosure.step step' (ih step)
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_snoc
Proof state before:
case base
j i k : ℕ
nfa : NFA
i✝ : ℕ
step : k ∈ nfa.εStep i✝
⊢ k ∈ nfa.εClosure i✝
Tactic:
exact .step step .base
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_snoc
Proof state before:
case step
j i k : ℕ
nfa : NFA
i✝ j✝ k✝ : ℕ
step' : j✝ ∈ nfa.εStep i✝
rest✝ : nfa.εClosure j✝ k✝
ih : k ∈ nfa.εStep k✝ → k ∈ nfa.εClosure j✝
step : k ∈ nfa.εStep k✝
⊢ k ∈ nfa.εClosure i✝
Tactic:
exact εClosure.step step' (ih step)
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_trans
Proof state before:
j i k : ℕ
nfa : NFA
h₁ : j ∈ nfa.εClosure i
h₂ : k ∈ nfa.εClosure j
⊢ k ∈ nfa.εClosure i
Tactic:
induction h₁ with
| base => exact h₂
| step head _ ih => exact .step head (ih h₂)
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_trans
Proof state before:
case base
j i k : ℕ
nfa : NFA
i✝ : ℕ
h₂ : k ∈ nfa.εClosure i✝
⊢ k ∈ nfa.εClosure i✝
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_trans
Proof state before:
case step
j i k : ℕ
nfa : NFA
i✝ j✝ k✝ : ℕ
head : j✝ ∈ nfa.εStep i✝
rest✝ : nfa.εClosure j✝ k✝
ih : k ∈ nfa.εClosure k✝ → k ∈ nfa.εClosure j✝
h₂ : k ∈ nfa.εClosure k✝
⊢ k ∈ nfa.εClosure i✝
Tactic:
exact .step head (ih h₂)
Proof state after:
no goals
Theorem: Regex.NFA.subset_εClosure_of_mem
Proof state before:
nfa : NFA
i j : ℕ
h : j ∈ nfa.εClosure i
⊢ nfa.εClosure j ⊆ nfa.εClosure i
Tactic:
intro k h'
Proof state after:
nfa : NFA
i j : ℕ
h : j ∈ nfa.εClosure i
k : ℕ
h' : k ∈ nfa.εClosure j
⊢ k ∈ nfa.εClosure i
Theorem: Regex.NFA.subset_εClosure_of_mem
Proof state before:
nfa : NFA
i j : ℕ
h : j ∈ nfa.εClosure i
k : ℕ
h' : k ∈ nfa.εClosure j
⊢ k ∈ nfa.εClosure i
Tactic:
exact εClosure_trans h h'
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) ↔ ∀ i ∈ S, nfa.εClosure i ⊆ S
Tactic:
apply Iff.intro
Proof state after:
case mp
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S

case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S

case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
. intro assm i mem
  intro k cls
  induction cls with
  | base => exact mem
  | @step i j k step _ ih =>
    cases Nat.decLt i nfa.nodes.size with
    | isTrue lt =>
      simp [εStep, lt] at step
      exact ih (assm i mem lt j step)
    | isFalse nlt => simp [εStep, nlt] at step
Proof state after:
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
. intro assm i mem _ j step
  apply Set.mem_of_mem_of_subset _ (assm i mem)
  exact εClosure.step (εStep_of_εStep step) .base
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S
Tactic:
intro assm i mem
Proof state after:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
⊢ nfa.εClosure i ⊆ S
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
⊢ nfa.εClosure i ⊆ S
Tactic:
intro k cls
Proof state after:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
k : ℕ
cls : k ∈ nfa.εClosure i
⊢ k ∈ S
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
k : ℕ
cls : k ∈ nfa.εClosure i
⊢ k ∈ S
Tactic:
induction cls with
| base => exact mem
| @step i j k step _ ih =>
  cases Nat.decLt i nfa.nodes.size with
  | isTrue lt =>
    simp [εStep, lt] at step
    exact ih (assm i mem lt j step)
  | isFalse nlt => simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp.base
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i k i✝ : ℕ
mem : i✝ ∈ S
⊢ i✝ ∈ S
Tactic:
exact mem
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp.step
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
⊢ k ∈ S
Tactic:
cases Nat.decLt i nfa.nodes.size with
| isTrue lt =>
  simp [εStep, lt] at step
  exact ih (assm i mem lt j step)
| isFalse nlt => simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp.step.isTrue
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
lt : i < nfa.nodes.size
⊢ k ∈ S
Tactic:
simp [εStep, lt] at step
Proof state after:
case mp.step.isTrue
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ k ∈ S
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp.step.isTrue
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ k ∈ S
Tactic:
exact ih (assm i mem lt j step)
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mp.step.isFalse
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
nlt : ¬i < nfa.nodes.size
⊢ k ∈ S
Tactic:
simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
intro assm i mem _ j step
Proof state after:
case mpr
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ S
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
case mpr
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ S
Tactic:
apply Set.mem_of_mem_of_subset _ (assm i mem)
Proof state after:
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εClosure i
Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub
Proof state before:
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εClosure i
Tactic:
exact εClosure.step (εStep_of_εStep step) .base
Proof state after:
no goals
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r = result
i : ℕ
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
induction r generalizing nfa next with
| empty | epsilon | char | classes =>
  try apply pushRegex.empty eq
  try apply pushRegex.epsilon eq
  try apply pushRegex.char eq
  try apply pushRegex.sparse eq
  intro eq
  subst eq
  apply pushNode_get_lt i h
| group _ r ih =>
  apply pushRegex.group eq
  intro nfa' nfa'' nfa''' property _ _ eq₁ eq₂ eq₃ eq
  have h₁ : i < nfa'.val.nodes.size := Nat.lt_trans h nfa'.property
  have h₂ : i < nfa''.val.nodes.size := Nat.lt_trans h₁ nfa''.property
  simp [eq, eq₃, pushNode_get_lt _ h₂]
  simp [ih eq₂.symm h₁]
  simp [eq₁, pushNode_get_lt _ h]
| alternate r₁ r₂ ih₁ ih₂ =>
  apply pushRegex.alternate eq
  intro nfa₁ start₁ nfa₂ start₂ _ nfa' property eq₁ _ eq₃ _ eq₅ eq
  have h₁ : i < nfa₁.val.nodes.size := Nat.lt_trans h nfa₁.property
  have h₂ : i < nfa₂.val.nodes.size := Nat.lt_trans h₁ nfa₂.property
  simp [eq, eq₅, pushNode_get_lt _ h₂]
  simp [ih₂ eq₃.symm h₁]
  simp [ih₁ eq₁.symm h]
| concat r₁ r₂ ih₁ ih₂ =>
  apply pushRegex.concat eq
  intro nfa₂ nfa₁ property eq₂ eq₁ eq
  have h₂ : i < nfa₂.val.nodes.size := Nat.lt_trans h nfa₂.property
  simp [eq, ih₁ eq₁.symm h₂, ih₂ eq₂.symm h]
| star r ih =>
  apply pushRegex.star eq
  intro placeholder compiled patched nfa' isLt inBounds property
    eq₁ eq₂ eq₃ eq₄ eq
  have ih := ih eq₂.symm (Nat.lt_trans h placeholder.property)
  conv =>
    lhs
    simp [eq, eq₄, get_eq_nodes_get, eq₃]
  have : i < compiled.val.nodes.size :=
    calc
      _ < _ := h
      _ < _ := placeholder.property
      _ < _ := compiled.property
  rw [Array.get_set (hj := this)]
  have : nfa.nodes.size ≠ i := Nat.ne_of_gt h
  simp [this, ←get_eq_nodes_get, ih, eq₁, pushNode_get_lt _ h]
Proof state after:
no goals
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case empty
i : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
try apply pushRegex.empty eq
Proof state after:
i : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode Node.fail ⋯ → (↑result)[i] = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case epsilon
i : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
try apply pushRegex.epsilon eq
Proof state after:
i : ℕ
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → (↑result)[i] = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case char
i : ℕ
a✝ : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char a✝) = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
try apply pushRegex.char eq
Proof state after:
i : ℕ
a✝ : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char a✝) = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode (Node.char a✝ ↑next) ⋯ → (↑result)[i] = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case classes
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
try apply pushRegex.sparse eq
Proof state after:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯ → (↑result)[i] = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯ → (↑result)[i] = nfa[i]
Tactic:
intro eq
Proof state after:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
eq : result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯
⊢ (↑result)[i] = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
eq : result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯
⊢ (↑result)[i] = nfa[i]
Tactic:
subst eq
Proof state after:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h : i < nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes a✝) = nfa.pushNode (Node.sparse a✝ ↑next) ⋯
⊢ (↑(nfa.pushNode (Node.sparse a✝ ↑next) ⋯))[i] = nfa[i]
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h : i < nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes a✝) = nfa.pushNode (Node.sparse a✝ ↑next) ⋯
⊢ (↑(nfa.pushNode (Node.sparse a✝ ↑next) ⋯))[i] = nfa[i]
Tactic:
apply pushNode_get_lt i h
Proof state after:
no goals
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case classes
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
apply pushRegex.empty eq
Proof state after:
no goals
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case classes
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
apply pushRegex.epsilon eq
Proof state after:
no goals
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case classes
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
apply pushRegex.char eq
Proof state after:
no goals
Theorem: Regex.NFA.pushRegex_get_lt
Proof state before:
case classes
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ (↑result)[i] = nfa[i]
Tactic:
apply pushRegex.sparse eq
Proof state after:
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯ → (↑result)[i] = nfa[i]