Theorem: Regex.VM.exploreεClosure_spec.mem_next_iff (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 : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target
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 : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target

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 : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target
Tactic:
have upper_inv : UpperInvExploreεClosure nfa target target #[] := by
  refine ⟨.base, by intros; simp_all⟩
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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
⊢ ∀ (i : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target

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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
⊢ ∀ (i : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target
Tactic:
have lower_bound := lower_bound_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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
lower_bound : LowerBoundεClosure nfa target next next'
⊢ ∀ (i : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target

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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
lower_bound : LowerBoundεClosure nfa target next next'
⊢ ∀ (i : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target
Tactic:
have upper_bound := upper_bound_exploreεClosure h upper_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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
lower_bound : LowerBoundεClosure nfa target next next'
upper_bound : UpperBoundεClosure nfa target next next'
⊢ ∀ (i : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target

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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
lower_bound : LowerBoundεClosure nfa target next next'
upper_bound : UpperBoundεClosure nfa target next next'
⊢ ∀ (i : Fin nfa.nodes.size), i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target
Tactic:
intro i
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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
lower_bound : LowerBoundεClosure nfa target next next'
upper_bound : UpperBoundεClosure nfa target next next'
i : Fin nfa.nodes.size
⊢ i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target

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 #[]
upper_inv : UpperInvExploreεClosure nfa target target #[]
lower_bound : LowerBoundεClosure nfa target next next'
upper_bound : UpperBoundεClosure nfa target next next'
i : Fin nfa.nodes.size
⊢ i ∈ next' ↔ i ∈ next ∨ ↑i ∈ nfa.εClosure ↑target
Tactic:
exact ⟨upper_bound i, lower_bound i⟩
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

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 #[]
⊢ UpperInvExploreεClosure nfa target target #[]
Tactic:
refine ⟨.base, by intros; simp_all⟩
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
lower_inv : LowerInvExploreεClosure nfa next target #[]
⊢ ∀ (j : Fin nfa.nodes.size), StackEntry.explore j ∈ #[] → ↑j ∈ nfa.εClosure ↑target
Tactic:
intros
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 #[]
j✝ : Fin nfa.nodes.size
a✝ : StackEntry.explore j✝ ∈ #[]
⊢ ↑j✝ ∈ nfa.εClosure ↑target

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 #[]
j✝ : Fin nfa.nodes.size
a✝ : StackEntry.explore j✝ ∈ #[]
⊢ ↑j✝ ∈ nfa.εClosure ↑target
Tactic:
simp_all
State after:
no goals