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

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
h : eachStepChar.go nfa c pos current i hle next saveSlots = (matched', next', saveSlots')
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
unfold eachStepChar.go at h
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h :
  (if h : i = current.count then (none, next, saveSlots)
    else
      let_fun hlt := ⋯;
      let result := stepChar nfa c pos next saveSlots current[i];
      match result.1 with
      | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
      | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h :
  (if h : i = current.count then (none, next, saveSlots)
    else
      let_fun hlt := ⋯;
      let result := stepChar nfa c pos next saveSlots current[i];
      match result.1 with
      | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
      | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
split at h
State after:
case 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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : (none, next, saveSlots) = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

case 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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

State before:
case 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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : (none, next, saveSlots) = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

case 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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
next =>
  simp at h
  simp [←h]
  exact hnotDone
State after:
case 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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

State before:
case 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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
next hi =>
  have hlt : i < current.count := Nat.lt_of_le_of_ne hle hi
  simp at h
  generalize heq : stepChar nfa c pos next saveSlots current[i] = result at h
  let (matched'', next'', saveSlots'') := result
  have := stepChar_mem_done_iff heq hnotDone
  simp at h
  split at h
  next =>
    simp at this
    exact eachStepChar_spec.mem_done_iff.go h this
  next =>
    simp at h
    simp only [←h, this]
State after:
no goals

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : (none, next, saveSlots) = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp at h
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : none = matched' ∧ next = next' ∧ saveSlots = saveSlots'
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : none = matched' ∧ next = next' ∧ saveSlots = saveSlots'
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp [←h]
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : none = matched' ∧ next = next' ∧ saveSlots = saveSlots'
⊢ ∀ (x : Fin nfa.nodes.size), next.mem x = true → ¬nfa[↑x] = Node.done

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : none = matched' ∧ next = next' ∧ saveSlots = saveSlots'
⊢ ∀ (x : Fin nfa.nodes.size), next.mem x = true → ¬nfa[↑x] = Node.done
Tactic:
exact hnotDone
State after:
no goals

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
have hlt : i < current.count := Nat.lt_of_le_of_ne hle hi
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
hlt : i < current.count
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
hlt : i < current.count
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp at h
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
h :
  (match (stepChar nfa c pos next saveSlots current[i]).1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (stepChar nfa c pos next saveSlots current[i]).2.1
        (stepChar nfa c pos next saveSlots current[i]).2.2
    | some val => stepChar nfa c pos next saveSlots current[i]) =
    (matched', next', saveSlots')
hlt : i < current.count
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
h :
  (match (stepChar nfa c pos next saveSlots current[i]).1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (stepChar nfa c pos next saveSlots current[i]).2.1
        (stepChar nfa c pos next saveSlots current[i]).2.2
    | some val => stepChar nfa c pos next saveSlots current[i]) =
    (matched', next', saveSlots')
hlt : i < current.count
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
generalize heq : stepChar nfa c pos next saveSlots current[i] = result at h
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : stepChar nfa c pos next saveSlots current[i] = result
h :
  (match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) ⋯ result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : stepChar nfa c pos next saveSlots current[i] = result
h :
  (match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) ⋯ result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
let (matched'', next'', saveSlots'') := result
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : 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 ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : 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 ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
have := stepChar_mem_done_iff heq hnotDone
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : 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')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ matched''.isSome = true
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : 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')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ matched''.isSome = true
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp at h
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match matched'' with
    | none => eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots''
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ matched''.isSome = true
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
heq : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match matched'' with
    | none => eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots''
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ matched''.isSome = true
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
split at h
State after:
case h_1
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
heq : stepChar nfa c pos next saveSlots current[i] = (none, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ none.isSome = true
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

case h_2
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

State before:
case h_1
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
heq : stepChar nfa c pos next saveSlots current[i] = (none, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ none.isSome = true
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

case h_2
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
next =>
  simp at this
  exact eachStepChar_spec.mem_done_iff.go h this
State after:
case h_2
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

State before:
case h_2
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
next =>
  simp at h
  simp only [←h, this]
State after:
no goals

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
heq : stepChar nfa c pos next saveSlots current[i] = (none, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ none.isSome = true
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp at this
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
heq : stepChar nfa c pos next saveSlots current[i] = (none, next'', saveSlots'')
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
this : ∀ (x : Fin nfa.nodes.size), next''.mem x = true → ¬nfa[↑x] = Node.done
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
heq : stepChar nfa c pos next saveSlots current[i] = (none, next'', saveSlots'')
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
this : ∀ (x : Fin nfa.nodes.size), next''.mem x = true → ¬nfa[↑x] = Node.done
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
exact eachStepChar_spec.mem_done_iff.go h this
State after:
no goals

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp at h
State after:
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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : some val✝ = matched' ∧ next'' = next' ∧ saveSlots'' = saveSlots'
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

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
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
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
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : some val✝ = matched' ∧ next'' = next' ∧ saveSlots'' = saveSlots'
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
simp only [←h, this]
State after:
no goals