internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
case inr.inr
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this✝ : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
target : Fin nfa.nodes.size
heq : stack.back' hemp = StackEntry.explore target
h : exploreεClosure nfa pos next currentSave matched saveSlots target stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : StackEntry.explore j = StackEntry.explore target
this : j = target
⊢ j ∈ next ∨ j = target ∨ StackEntry.explore j ∈ stack.pop
Tactic:
exact .inr (.inl this)
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
target : Fin nfa.nodes.size
heq : stack.back' hemp = StackEntry.explore target
h : exploreεClosure nfa pos next currentSave matched saveSlots target stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : StackEntry.explore j = StackEntry.explore target
⊢ j = target
Tactic:
simp at heq'
Proof state after:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
target : Fin nfa.nodes.size
heq : stack.back' hemp = StackEntry.explore target
h : exploreεClosure nfa pos next currentSave matched saveSlots target stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : j = target
⊢ j = target
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
target : Fin nfa.nodes.size
heq : stack.back' hemp = StackEntry.explore target
h : exploreεClosure nfa pos next currentSave matched saveSlots target stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : j = target
⊢ j = target
Tactic:
exact heq'
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Tactic:
have inv' : LowerInvεClosure nfa next stack.pop := by
  intro i j hi hj
  cases inv i j hi hj with
  | inl hnext => exact .inl hnext
  | inr hstack =>
    cases Array.mem_pop_or_eq_of_mem _ _ hemp hstack with
    | inl hstack => exact .inr hstack
    | inr heq' =>
      rw [heq] at heq'
      contradiction
Proof state after:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
inv' : LowerInvεClosure nfa next stack.pop
⊢ LowerInvεClosure nfa next' #[]
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
inv' : LowerInvεClosure nfa next stack.pop
⊢ LowerInvεClosure nfa next' #[]
Tactic:
exact lower_inv_εClosure h inv'
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next stack.pop
Tactic:
intro i j hi hj
Proof state after:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Tactic:
cases inv i j hi hj with
| inl hnext => exact .inl hnext
| inr hstack =>
  cases Array.mem_pop_or_eq_of_mem _ _ hemp hstack with
  | inl hstack => exact .inr hstack
  | inr heq' =>
    rw [heq] at heq'
    contradiction
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
case inl
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hnext : j ∈ next
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Tactic:
exact .inl hnext
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
case inr
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Tactic:
cases Array.mem_pop_or_eq_of_mem _ _ hemp hstack with
| inl hstack => exact .inr hstack
| inr heq' =>
  rw [heq] at heq'
  contradiction
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
case inr.inl
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack✝ : StackEntry.explore j ∈ stack
hstack : StackEntry.explore j ∈ stack.pop
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Tactic:
exact .inr hstack
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
case inr.inr
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : StackEntry.explore j = stack.back' hemp
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Tactic:
rw [heq] at heq'
Proof state after:
case inr.inr
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : StackEntry.explore j = StackEntry.restore save✝
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Theorem: Regex.VM.lower_inv_εClosure
Proof state before:
case inr.inr
nfa : NFA
pos : String.Pos
next : SparseSet nfa.nodes.size
currentSave : Array (Option String.Pos)
matched : Option (Array (Option String.Pos))
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
stack : Array (StackEntry nfa.nodes.size)
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : LowerInvεClosure nfa next stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
hstack : StackEntry.explore j ∈ stack
heq' : StackEntry.explore j = StackEntry.restore save✝
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack.pop
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
let S := { j | ∃ isLt : j < nfa.nodes.size, ⟨j, isLt⟩ ∈ next }
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have : ∀ i ∈ S, (_ : i < nfa.nodes.size) → ∀ j ∈ nfa[i].εStep, j ∈ S := by
  intro i hi iLt j hj
  have ⟨_, hi⟩ := hi
  have jLt : j < nfa.nodes.size := lt_of_εStep hj
  have hj : j ∈ nfa.εStep i := by
    simp [εStep, iLt, hj]
  have := inv ⟨i, iLt⟩ ⟨j, jLt⟩ hi hj
  simp at this
  refine ⟨jLt, this⟩
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have := mem_εStep_iff_εClosure_sub.mp this
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
intro i hi j hj
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have : nfa.εClosure i ⊆ S := this i ⟨i.isLt, hi⟩
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝¹ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this : nfa.εClosure ↑i ⊆ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝¹ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this : nfa.εClosure ↑i ⊆ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have : j ∈ S := this hj
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝² : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝¹ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this✝ : nfa.εClosure ↑i ⊆ S
this : j ∈ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝² : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝¹ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this✝ : nfa.εClosure ↑i ⊆ S
this : j ∈ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
exact this
Proof state after:
no goals
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
intro i hi iLt j hj
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
⊢ j ∈ S
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
⊢ j ∈ S
Tactic:
have ⟨_, hi⟩ := hi
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
⊢ j ∈ S
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
⊢ j ∈ S
Tactic:
have jLt : j < nfa.nodes.size := lt_of_εStep hj
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
⊢ j ∈ S
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
⊢ j ∈ S
Tactic:
have hj : j ∈ nfa.εStep i := by
  simp [εStep, iLt, hj]
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
⊢ j ∈ S
Theorem: Regex.VM.εClosure_subset_lower_inv
Proof state before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
⊢ j ∈ S
Tactic:
have := inv ⟨i, iLt⟩ ⟨j, jLt⟩ hi hj
Proof state after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : ⟨j, jLt⟩ ∈ next ∨ StackEntry.explore ⟨j, jLt⟩ ∈ #[]
⊢ j ∈ S