Theorem: Regex.VM.eachStepChar_spec.preserve_cls (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
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
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
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'

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
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

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]
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

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
State after:
no goals