Theorem: Regex.VM.exploreεClosure_spec.preserve_cls (RegexCorrectness/VM/Auxiliary.lean)

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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
have lower_inv : LowerInvExploreεClosure nfa next target #[] := by
  intro i j hi hj
  exact .inl (inv i j hi hj)
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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
lower_inv : LowerInvExploreεClosure nfa next target #[]
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'

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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
lower_inv : LowerInvExploreεClosure nfa next target #[]
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
have lower_inv' : LowerInvεClosure nfa next' #[] := lower_inv_exploreεClosure h lower_inv
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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
lower_inv : LowerInvExploreεClosure nfa next target #[]
lower_inv' : LowerInvεClosure nfa next' #[]
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'

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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
lower_inv : LowerInvExploreεClosure nfa next target #[]
lower_inv' : LowerInvεClosure nfa next' #[]
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
simp [LowerInvεClosure] at lower_inv'
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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
lower_inv : LowerInvExploreεClosure nfa next target #[]
lower_inv' : ∀ (i j : Fin nfa.nodes.size), next'.mem i = true → ↑j ∈ nfa.εStep ↑i → next'.mem j = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'

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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
lower_inv : LowerInvExploreεClosure nfa next target #[]
lower_inv' : ∀ (i j : Fin nfa.nodes.size), next'.mem i = true → ↑j ∈ nfa.εStep ↑i → next'.mem j = true
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
Tactic:
exact lower_inv'
State after:
no goals

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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
⊢ LowerInvExploreεClosure nfa next target #[]
Tactic:
intro i j hi hj
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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
⊢ j ∈ next ∨ j = target ∨ StackEntry.explore j ∈ #[]

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
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 #[] = (matched', next', saveSlots')
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
i j : Fin nfa.nodes.size
hi : i ∈ next
hj : ↑j ∈ nfa.εStep ↑i
⊢ j ∈ next ∨ j = target ∨ StackEntry.explore j ∈ #[]
Tactic:
exact .inl (inv i j hi hj)
State after:
no goals