internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.eachStepChar_spec.preserve_cls.go
Proof state before:
case h_2
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
next =>
  simp at h
  simp only [←h]
  exact stepChar_spec.preserve_cls hres inv
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.preserve_cls.go
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h :
  eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
      (matched'', next'', saveSlots'').2.2 =
    (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
simp at h
Proof state after:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Theorem: Regex.VM.eachStepChar_spec.preserve_cls.go
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
exact eachStepChar_spec.preserve_cls.go h (stepChar_spec.preserve_cls hres inv)
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.preserve_cls.go
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
simp at h
Proof state after:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = saveSlots'
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Theorem: Regex.VM.eachStepChar_spec.preserve_cls.go
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = saveSlots'
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
simp only [←h]
Proof state after:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = saveSlots'
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
Theorem: Regex.VM.eachStepChar_spec.preserve_cls.go
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched'' : Option (Array (Option String.Pos))
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = saveSlots'
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
Tactic:
exact stepChar_spec.preserve_cls hres inv
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.preserve_cls
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar nfa c pos current next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
unfold eachStepChar at h
Proof state after:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar.go nfa c pos current 0 ⋯ next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Theorem: Regex.VM.eachStepChar_spec.preserve_cls
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar.go nfa c pos current 0 ⋯ next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
apply eachStepChar_spec.preserve_cls.go h
Proof state after:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar.go nfa c pos current 0 ⋯ next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
Theorem: Regex.VM.eachStepChar_spec.preserve_cls
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar.go nfa c pos current 0 ⋯ next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
Tactic:
simp only [SparseSet.not_mem_of_isEmpty hemp]
Proof state after:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar.go nfa c pos current 0 ⋯ next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → False
Theorem: Regex.VM.eachStepChar_spec.preserve_cls
Proof state before:
nfa : NFA
c : Char
pos : String.Pos
current next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) 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 : eachStepChar.go nfa c pos current 0 ⋯ next saveSlots = (matched', next', saveSlots')
hemp : next.isEmpty = true
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → False
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.VM.exploreεClosure_mem_done_iff
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
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')
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true
Theorem: Regex.VM.exploreεClosure_mem_done_iff
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
h✝ : target ∈ next
h : εClosure nfa pos next currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true
Tactic:
exact εClosure_mem_done_iff h inv
Proof state after:
no goals
Theorem: Regex.VM.exploreεClosure_mem_done_iff
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
hmem : target ∉ next
inv' : nfa[target] ≠ Node.done → ((∃ i ∈ next.insert target, nfa[i] = Node.done) ↔ matched.isSome = true)
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')
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true

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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
hmem : target ∉ next
inv' : nfa[target] ≠ Node.done → ((∃ i ∈ next.insert target, nfa[i] = Node.done) ↔ matched.isSome = true)
heq✝ : nfa[↑target] = Node.fail
h : εClosure nfa pos (next.insert target) currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true
Tactic:
next hn => exact εClosure_mem_done_iff h (inv' (by simp [hn]))
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
hmem : target ∉ next
inv' : nfa[target] ≠ Node.done → ((∃ i ∈ next.insert target, nfa[i] = Node.done) ↔ matched.isSome = true)
heq✝ : nfa[↑target] = Node.fail
h : εClosure nfa pos (next.insert target) currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true
Theorem: Regex.VM.exploreεClosure_mem_done_iff
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
hmem : target ∉ next
inv' : nfa[target] ≠ Node.done → ((∃ i ∈ next.insert target, nfa[i] = Node.done) ↔ matched.isSome = true)
heq✝ : nfa[↑target] = Node.fail
h : εClosure nfa pos (next.insert target) currentSave matched saveSlots stack = (matched', next', saveSlots')
⊢ (∃ i ∈ next', nfa[i] = Node.done) ↔ matched'.isSome = true
Tactic:
next hn => exact εClosure_mem_done_iff h (inv' (by simp [hn]))
Proof state after:
no goals
Theorem: Regex.VM.exploreεClosure_mem_done_iff
Proof state before:
case mpr
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 : (∃ i ∈ next, nfa[i] = Node.done) ↔ matched.isSome = true
hmem : target ∉ next
h :
  (match hn : nfa[↑target] with
    | Node.epsilon target' =>
      exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack
    | Node.split target₁ target₂ =>
      exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target₁, ⋯⟩
        (stack.push (StackEntry.explore ⟨target₂, ⋯⟩))
    | Node.save offset target' =>
      if h : offset < currentSave.size then
        exploreεClosure nfa pos (next.insert target) (currentSave.set ⟨offset, ⋯⟩ (some pos)) matched saveSlots
          ⟨target', ⋯⟩ (stack.push (StackEntry.restore currentSave))
      else exploreεClosure nfa pos (next.insert target) currentSave matched saveSlots ⟨target', ⋯⟩ stack
    | Node.done =>
      εClosure nfa pos (next.insert target) currentSave (HOrElse.hOrElse matched fun x => some currentSave)
        (saveSlots.set ↑target ⋯ currentSave) stack
    | Node.char c next_1 =>
      εClosure nfa pos (next.insert target) currentSave matched (saveSlots.set ↑target ⋯ currentSave) stack
    | Node.sparse cs next_1 =>
      εClosure nfa pos (next.insert target) currentSave matched (saveSlots.set ↑target ⋯ currentSave) stack
    | Node.fail => εClosure nfa pos (next.insert target) currentSave matched saveSlots stack) =
    (matched', next', saveSlots')
hn : nfa[target] ≠ Node.done
⊢ matched.isSome = true → ∃ i ∈ next.insert target, nfa[i] = Node.done
Tactic:
. intro h
  have ⟨i, hmem', hn'⟩ := inv.mpr h
  exact ⟨i, SparseSet.mem_insert_of_mem hmem', hn'⟩
Proof state after:
no goals