internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mpr
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ (∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') →
    (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
. intro h
  have ⟨i', hlt', hlt'', hmem⟩ := h
  cases Nat.lt_succ_iff_lt_or_eq.mp hlt'' with
  | inl hlt'' => exact .inl ⟨i', hlt', hlt'', hmem⟩
  | inr heq =>
    simp [heq] at hmem
    exact .inr hmem
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mp
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h :
  (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
cases h with
| inl h =>
  have ⟨i', hlt', hlt'', hmem⟩ := h
  exact ⟨i', hlt', Nat.le.step hlt'', hmem⟩
| inr hmem => exact ⟨i, hlt, Nat.lt_succ_self _, hmem⟩
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mp.inl
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
exact ⟨i', hlt', Nat.le.step hlt'', hmem⟩
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mp.inr
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
hmem : ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
exact ⟨i, hlt, Nat.lt_succ_self _, hmem⟩
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mpr
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
cases Nat.lt_succ_iff_lt_or_eq.mp hlt'' with
| inl hlt'' => exact .inl ⟨i', hlt', hlt'', hmem⟩
| inr heq =>
  simp [heq] at hmem
  exact .inr hmem
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mpr.inl
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt''✝ : i' < i + 1
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
hlt'' : i' < i
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
exact .inl ⟨i', hlt', hlt'', hmem⟩
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case mpr.inr
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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
heq : i' = i
hmem : ∃ i'' ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
exact .inr hmem
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂' : ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
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')
⊢ ∃ 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:
exact go h inv₁' inv₂'
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.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₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
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'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂' : ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
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'
⊢ ∃ 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:
exact ⟨i + 1, inv₁'⟩
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff
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
⊢ ∃ 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
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
⊢ ∃ 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''
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff
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
⊢ ∃ 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
Proof 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
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff
Proof 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]
Proof 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
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff
Proof 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)
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_next_iff
Proof 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
Proof 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''