Theorem: Regex.VM.eachStepChar_spec.mem_next_iff (RegexCorrectness/VM/Auxiliary.lean)

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
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
unfold eachStepChar at h
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
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

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
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
apply eachStepChar_spec.mem_next_iff.go h
State after:
case inv₁
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
⊢ ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

case inv₂
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

State before:
case inv₁
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
⊢ ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

case inv₂
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:
. intro j
  have : j ∉ next := SparseSet.not_mem_of_isEmpty hemp
  simp at this
  simp [this]
State after:
case inv₂
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

State before:
case inv₂
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:
. intro i j hi
  exact absurd hi (SparseSet.not_mem_of_isEmpty hemp)
State after:
no goals

State before:
case inv₁
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
⊢ ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
intro j
State after:
case inv₁
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
j : Fin nfa.nodes.size
⊢ j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
case inv₁
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
j : Fin nfa.nodes.size
⊢ j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
have : j ∉ next := SparseSet.not_mem_of_isEmpty hemp
State after:
case inv₁
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
j : Fin nfa.nodes.size
this : j ∉ next
⊢ j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
case inv₁
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
j : Fin nfa.nodes.size
this : j ∉ next
⊢ j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
simp at this
State after:
case inv₁
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
j : Fin nfa.nodes.size
this : next.mem j = false
⊢ j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
case inv₁
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
j : Fin nfa.nodes.size
this : next.mem j = false
⊢ j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < 0 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
simp [this]
State after:
no goals

State before:
case inv₂
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:
intro i j hi
State after:
case inv₂
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
hi : i ∈ next
⊢ ↑j ∈ nfa.εStep ↑i → j ∈ next

State before:
case inv₂
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
hi : i ∈ next
⊢ ↑j ∈ nfa.εStep ↑i → j ∈ next
Tactic:
exact absurd hi (SparseSet.not_mem_of_isEmpty hemp)
State after:
no goals