internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.mem_stack_mem_ε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
i : Fin nfa.nodes.size
hmem : StackEntry.explore i ∈ stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
heq : StackEntry.explore i = stack.back' hemp
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 ∈ next'
Tactic:
rw [heq'] 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
i : Fin nfa.nodes.size
hmem : StackEntry.explore i ∈ stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : StackEntry.explore i = StackEntry.restore save✝
heq' : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
⊢ i ∈ next'
Theorem: Regex.VM.mem_stack_mem_ε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
i : Fin nfa.nodes.size
hmem : StackEntry.explore i ∈ stack
hemp : ¬stack.isEmpty = true
this : stack.pop.size < stack.size
entry✝ : StackEntry nfa.nodes.size
save✝ : Array (Option String.Pos)
heq : StackEntry.explore i = StackEntry.restore save✝
heq' : stack.back' hemp = StackEntry.restore save✝
h : εClosure nfa pos next save✝ matched saveSlots stack.pop = (matched', next', saveSlots')
⊢ i ∈ next'
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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
h : exploreεClosure nfa pos next currentSave matched saveSlots target stack = (matched', next', saveSlots')
inv : LowerInvExploreεClosure nfa next target stack
⊢ LowerInvεClosure nfa next' #[]
Tactic:
unfold exploreεClosure at h
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h :
  (if target ∈ next then εClosure nfa pos next currentSave matched saveSlots stack
    else
      let next' := next.insert target;
      match hn : nfa[target] with
      | Node.epsilon target' =>
        let_fun isLt := ⋯;
        exploreεClosure nfa pos next' currentSave matched saveSlots ⟨target', isLt⟩ stack
      | Node.split target₁ target₂ =>
        let_fun isLt := ⋯;
        exploreεClosure nfa pos next' currentSave matched saveSlots ⟨target₁, ⋯⟩
          (stack.push (StackEntry.explore ⟨target₂, ⋯⟩))
      | Node.save offset target' =>
        let_fun isLt := ⋯;
        if h : offset < currentSave.size then
          let nextSave := currentSave.set ⟨offset, h⟩ (some pos);
          let stack' := stack.push (StackEntry.restore currentSave);
          exploreεClosure nfa pos next' nextSave matched saveSlots ⟨target', isLt⟩ stack'
        else exploreεClosure nfa pos next' currentSave matched saveSlots ⟨target', isLt⟩ stack
      | Node.done =>
        let matched' := HOrElse.hOrElse matched fun x => some currentSave;
        let saveSlots' := saveSlots.set ↑target ⋯ currentSave;
        εClosure nfa pos next' currentSave matched' saveSlots' stack
      | Node.char c next =>
        let saveSlots' := saveSlots.set ↑target ⋯ currentSave;
        εClosure nfa pos next' currentSave matched saveSlots' stack
      | Node.sparse cs next =>
        let saveSlots' := saveSlots.set ↑target ⋯ currentSave;
        εClosure nfa pos next' currentSave matched saveSlots' stack
      | Node.fail => εClosure nfa pos next' currentSave matched saveSlots stack) =
    (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Tactic:
have inv' : LowerInvεClosure nfa next stack := by
  intro i j hi hj
  match inv i j hi hj with
  | .inl hnext => exact .inl hnext
  | .inr (.inl htarget) =>
    rw [←htarget] at hmem
    exact .inl hmem
  | .inr (.inr hstack) => exact .inr hstack
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
inv' : LowerInvεClosure nfa next stack
⊢ LowerInvεClosure nfa next' #[]
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
inv' : LowerInvεClosure nfa next stack
⊢ LowerInvεClosure nfa next' #[]
Tactic:
exact lower_inv_εClosure h inv'
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next stack
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack
Tactic:
match inv i j hi hj with
| .inl hnext => exact .inl hnext
| .inr (.inl htarget) =>
  rw [←htarget] at hmem
  exact .inl hmem
| .inr (.inr hstack) => exact .inr hstack
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (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
Tactic:
exact .inl hnext
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
htarget : j = target
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack
Tactic:
rw [←htarget] at hmem
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hmem : j ∈ next
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
htarget : j = target
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
i j : Fin nfa.nodes.size
hmem : j ∈ next
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
htarget : j = target
⊢ j ∈ next ∨ StackEntry.explore j ∈ stack
Tactic:
exact .inl hmem
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
hmem : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (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
Tactic:
exact .inr hstack
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreεClosure
Proof state before:
case h_6
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
cs✝ : Data.Classes
next✝ : ℕ
heq✝ : nfa[↑target] = Node.sparse cs✝ next✝
h :
  εClosure nfa pos (next.insert target) currentSave matched (saveSlots.set ↑target ⋯ currentSave) stack =
    (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]

case h_7
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
heq✝ : nfa[↑target] = Node.fail
h : εClosure nfa pos (next.insert target) currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Tactic:
next _ _ hn =>
  have inv' : LowerInvεClosure nfa (next.insert target) stack := by
    intro i j hi hj
    cases SparseSet.eq_or_mem_of_mem_insert hi with
    | inl htarget =>
      subst htarget
      simp [εStep, Node.εStep, hn] at hj
    | inr hnext =>
      match inv i j hnext hj with
      | .inl hnext => exact .inl (SparseSet.mem_insert_of_mem hnext)
      | .inr (.inl htarget) => exact .inl (htarget ▸ SparseSet.mem_insert)
      | .inr (.inr hstack) => exact .inr hstack
  exact lower_inv_εClosure h inv'
Proof state after:
case h_7
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
heq✝ : nfa[↑target] = Node.fail
h : εClosure nfa pos (next.insert target) currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Theorem: Regex.VM.lower_inv_exploreεClosure
Proof state before:
case h_7
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
heq✝ : nfa[↑target] = Node.fail
h : εClosure nfa pos (next.insert target) currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Tactic:
next hn =>
  have inv' : LowerInvεClosure nfa (next.insert target) stack := by
    intro i j hi hj
    cases SparseSet.eq_or_mem_of_mem_insert hi with
    | inl htarget =>
      subst htarget
      simp [εStep, Node.εStep, hn] at hj
    | inr hnext =>
      match inv i j hnext hj with
      | .inl hnext => exact .inl (SparseSet.mem_insert_of_mem hnext)
      | .inr (.inl htarget) => exact .inl (htarget ▸ SparseSet.mem_insert)
      | .inr (.inr hstack) => exact .inr hstack
  exact lower_inv_εClosure h inv'
Proof state after:
no goals
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
target' : ℕ
hn : nfa[↑target] = Node.epsilon target'
h :
  exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack =
    (matched', next', saveSlots')
⊢ LowerInvεClosure nfa next' #[]
Tactic:
have isLt := nfa.inBounds' target hn
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
target' : ℕ
hn : nfa[↑target] = Node.epsilon target'
h :
  exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack =
    (matched', next', saveSlots')
isLt : (Node.epsilon target').inBounds nfa.nodes.size
⊢ LowerInvεClosure nfa next' #[]
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
target' : ℕ
hn : nfa[↑target] = Node.epsilon target'
h :
  exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack =
    (matched', next', saveSlots')
isLt : (Node.epsilon target').inBounds nfa.nodes.size
⊢ LowerInvεClosure nfa next' #[]
Tactic:
have inv' : LowerInvExploreεClosure nfa (next.insert target) ⟨target', isLt⟩ stack := by
  intro i j hi hj
  cases SparseSet.eq_or_mem_of_mem_insert hi with
  | inl htarget =>
    subst htarget
    simp [εStep, Node.εStep, hn] at hj
    exact .inr (.inl (Fin.eq_of_val_eq hj))
  | inr hnext =>
    match inv i j hnext hj with
    | .inl hnext => exact .inl (SparseSet.mem_insert_of_mem hnext)
    | .inr (.inl htarget) => exact .inl (htarget ▸ SparseSet.mem_insert)
    | .inr (.inr hstack) => exact .inr (.inr hstack)
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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
target' : ℕ
hn : nfa[↑target] = Node.epsilon target'
h :
  exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack =
    (matched', next', saveSlots')
isLt : (Node.epsilon target').inBounds nfa.nodes.size
inv' : LowerInvExploreεClosure nfa (next.insert target) ⟨target', isLt⟩ stack
⊢ LowerInvεClosure nfa next' #[]
Theorem: Regex.VM.lower_inv_exploreε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
target : Fin 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 : LowerInvExploreεClosure nfa next target stack
h✝ : target ∉ next
target' : ℕ
hn : nfa[↑target] = Node.epsilon target'
h :
  exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack =
    (matched', next', saveSlots')
isLt : (Node.epsilon target').inBounds nfa.nodes.size
inv' : LowerInvExploreεClosure nfa (next.insert target) ⟨target', isLt⟩ stack
⊢ LowerInvεClosure nfa next' #[]
Tactic:
exact lower_inv_exploreεClosure h inv'
Proof state after:
no goals