internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome✝ : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
hsome : matched'.isSome = true
i : Fin nfa.nodes.size
hi : i ∈ init'
hdone : nfa[i] = Node.done
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ SparseSet.empty → ↑j ∈ nfa.εStep ↑i → j ∈ SparseSet.empty
Tactic:
simp only [hnotMem]
Proof state after:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome✝ : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
hsome : matched'.isSome = true
i : Fin nfa.nodes.size
hi : i ∈ init'
hdone : nfa[i] = Node.done
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → False
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome✝ : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
hsome : matched'.isSome = true
i : Fin nfa.nodes.size
hi : i ∈ init'
hdone : nfa[i] = Node.done
⊢ ∀ (i j : Fin nfa.nodes.size), False → ↑j ∈ nfa.εStep ↑i → False
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome✝ : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
hsome : matched'.isSome = true
i : Fin nfa.nodes.size
hi : i ∈ init'
hdone : nfa[i] = Node.done
cls : ↑i ∈ nfa.εClosure ↑nfa.start
l r : List Char
v' : String.Iterator.ValidFor l r it
pos : String.Pos := { byteIdx := String.utf8Len l }
⊢ it.toString = { data := l.reverse ++ [] ++ r }
Tactic:
simp [v'.toString, List.reverseAux_eq]
Proof state after:
no goals
Theorem: Regex.VM.captureNext_spec
Proof state before:
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h : captureNext.go nfa saveSize it init' SparseSet.empty saveSlots matched' = matched
hnotMem : ∀ (i : Fin nfa.nodes.size), i ∉ SparseSet.empty
inv : captureNext.go.Inv nfa it it.toString init' matched'
⊢ SparseSet.empty.isEmpty = true
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds.done
Proof state before:
size : Nat
⊢ Node.done.inBounds size
Tactic:
simp [inBounds]
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds.fail
Proof state before:
size : Nat
⊢ Node.fail.inBounds size
Tactic:
simp [inBounds]
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds.epsilon
Proof state before:
size next : Nat
h : next < size
⊢ (Node.epsilon next).inBounds size
Tactic:
simp [inBounds, h]
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds.char
Proof state before:
size next : Nat
c : Char
h : next < size
⊢ (Node.char c next).inBounds size
Tactic:
simp [inBounds, h]
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds.split
Proof state before:
size next₁ next₂ : Nat
h₁ : next₁ < size
h₂ : next₂ < size
⊢ (Node.split next₁ next₂).inBounds size
Tactic:
simp [inBounds, h₁, h₂]
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds.save
Proof state before:
size offset next : Nat
h : next < size
⊢ (Node.save offset next).inBounds size
Tactic:
simp [inBounds, h]
Proof state after:
no goals
Theorem: Regex.NFA.Node.lt_of_inBounds.epsilon
Proof state before:
size next : Nat
h : (Node.epsilon next).inBounds size
⊢ next < size
Tactic:
simp [inBounds] at h
Proof state after:
size next : Nat
h : next < size
⊢ next < size
Theorem: Regex.NFA.Node.lt_of_inBounds.epsilon
Proof state before:
size next : Nat
h : next < size
⊢ next < size
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.NFA.Node.lt_of_inBounds.char
Proof state before:
size next : Nat
c : Char
h : (Node.char c next).inBounds size
⊢ next < size
Tactic:
simp [inBounds] at h
Proof state after:
size next : Nat
c : Char
h : next < size
⊢ next < size
Theorem: Regex.NFA.Node.lt_of_inBounds.char
Proof state before:
size next : Nat
c : Char
h : next < size
⊢ next < size
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.NFA.Node.lt_of_inBounds.split
Proof state before:
size next₁ next₂ : Nat
h : (Node.split next₁ next₂).inBounds size
⊢ next₁ < size ∧ next₂ < size
Tactic:
simp [inBounds] at h
Proof state after:
size next₁ next₂ : Nat
h : next₁ < size ∧ next₂ < size
⊢ next₁ < size ∧ next₂ < size
Theorem: Regex.NFA.Node.lt_of_inBounds.split
Proof state before:
size next₁ next₂ : Nat
h : next₁ < size ∧ next₂ < size
⊢ next₁ < size ∧ next₂ < size
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.NFA.Node.lt_of_inBounds.save
Proof state before:
size offset next : Nat
h : (Node.save offset next).inBounds size
⊢ next < size
Tactic:
simp [inBounds] at h
Proof state after:
size offset next : Nat
h : next < size
⊢ next < size
Theorem: Regex.NFA.Node.lt_of_inBounds.save
Proof state before:
size offset next : Nat
h : next < size
⊢ next < size
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
n : Node
h : n.inBounds size
le : size ≤ size'
⊢ n.inBounds size'
Tactic:
simp [inBounds] at *
Proof state after:
size size' : Nat
n : Node
h :
  match n with
  | done => True
  | fail => True
  | epsilon next => next < size
  | char c next => next < size
  | split next₁ next₂ => next₁ < size ∧ next₂ < size
  | save offset next => next < size
  | sparse cs next => next < size
le : size ≤ size'
⊢ match n with
  | done => True
  | fail => True
  | epsilon next => next < size'
  | char c next => next < size'
  | split next₁ next₂ => next₁ < size' ∧ next₂ < size'
  | save offset next => next < size'
  | sparse cs next => next < size'
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
n : Node
h :
  match n with
  | done => True
  | fail => True
  | epsilon next => next < size
  | char c next => next < size
  | split next₁ next₂ => next₁ < size ∧ next₂ < size
  | save offset next => next < size
  | sparse cs next => next < size
le : size ≤ size'
⊢ match n with
  | done => True
  | fail => True
  | epsilon next => next < size'
  | char c next => next < size'
  | split next₁ next₂ => next₁ < size' ∧ next₂ < size'
  | save offset next => next < size'
  | sparse cs next => next < size'
Tactic:
split <;> simp at h <;> try simp
Proof state after:
case h_3
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
case h_3
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
Proof state after:
case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
case h_4
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
Proof state after:
case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
case h_5
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'

case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact ⟨Nat.lt_of_lt_of_le h.left le, Nat.lt_of_lt_of_le h.right le⟩
Proof state after:
case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
case h_6
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'

case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
Proof state after:
case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
case h_7
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
next => exact Nat.lt_of_lt_of_le h le
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
case h_2
size size' : Nat
le : size ≤ size'
x✝ : Node
h : True
⊢ True
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Char
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝¹ < size ∧ a✝ < size
⊢ a✝¹ < size' ∧ a✝ < size'
Tactic:
exact ⟨Nat.lt_of_lt_of_le h.left le, Nat.lt_of_lt_of_le h.right le⟩
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
Proof state after:
no goals
Theorem: Regex.NFA.Node.inBounds_of_inBounds_of_le
Proof state before:
size size' : Nat
le : size ≤ size'
x✝ : Node
a✝¹ : Data.Classes
a✝ : Nat
h : a✝ < size
⊢ a✝ < size'
Tactic:
exact Nat.lt_of_lt_of_le h le
Proof state after:
no goals
Theorem: Regex.NFA.zero_lt_size
Proof state before:
nfa : NFA
⊢ 0 < nfa.nodes.size
Tactic:
apply Nat.zero_lt_of_ne_zero
Proof state after:
case h
nfa : NFA
⊢ nfa.nodes.size ≠ 0
Theorem: Regex.NFA.zero_lt_size
Proof state before:
case h
nfa : NFA
⊢ nfa.nodes.size ≠ 0
Tactic:
intro h
Proof state after:
case h
nfa : NFA
h : nfa.nodes.size = 0
⊢ False
Theorem: Regex.NFA.zero_lt_size
Proof state before:
case h
nfa : NFA
h : nfa.nodes.size = 0
⊢ False
Tactic:
exact (h ▸ nfa.start).elim0
Proof state after:
no goals
Theorem: Regex.NFA.inBounds'
Proof state before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ n.inBounds nfa.nodes.size
Tactic:
rw [←hn]
Proof state after:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ nfa[i].inBounds nfa.nodes.size
Theorem: Regex.NFA.inBounds'
Proof state before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ nfa[i].inBounds nfa.nodes.size
Tactic:
have inBounds := nfa.inBounds i
Proof state after:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
⊢ nfa[i].inBounds nfa.nodes.size
Theorem: Regex.NFA.inBounds'
Proof state before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
⊢ nfa[i].inBounds nfa.nodes.size
Tactic:
have : nfa[i] = nfa.nodes[i.val] := rfl
Proof state after:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
this : nfa[i] = nfa.nodes[↑i]
⊢ nfa[i].inBounds nfa.nodes.size
Theorem: Regex.NFA.inBounds'
Proof state before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
this : nfa[i] = nfa.nodes[↑i]
⊢ nfa[i].inBounds nfa.nodes.size
Tactic:
exact this ▸ inBounds
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
i i' : ℕ
nfa : NFA
start : ℕ
path : nfa.pathIn start i i' []
⊢ i' ∈ nfa.εClosure i
Tactic:
generalize h : [] = cs at path
Proof state after:
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
h : [] = cs
path : nfa.pathIn start i i' cs
⊢ i' ∈ nfa.εClosure i
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
h : [] = cs
path : nfa.pathIn start i i' cs
⊢ i' ∈ nfa.εClosure i
Tactic:
induction path with
| base _ => exact .base
| @step i j k cs cs' step _ ih =>
  simp at h
  simp [h] at *
  cases step with
  | εStep _ _ step =>
    exact εClosure.step (εStep_of_εStep step) ih
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
case base
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
i✝ : ℕ
h✝ : start ≤ i✝
h : [] = []
⊢ i✝ ∈ nfa.εClosure i✝
Tactic:
exact .base
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest✝ : nfa.pathIn start j k cs'
ih : [] = cs' → k ∈ nfa.εClosure j
h : [] = cs ++ cs'
⊢ k ∈ nfa.εClosure i
Tactic:
simp at h
Proof state after:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest✝ : nfa.pathIn start j k cs'
ih : [] = cs' → k ∈ nfa.εClosure j
h : cs = [] ∧ cs' = []
⊢ k ∈ nfa.εClosure i
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest✝ : nfa.pathIn start j k cs'
ih : [] = cs' → k ∈ nfa.εClosure j
h : cs = [] ∧ cs' = []
⊢ k ∈ nfa.εClosure i
Tactic:
simp [h] at *
Proof state after:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j []
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
⊢ k ∈ nfa.εClosure i
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
case step
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j []
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
⊢ k ∈ nfa.εClosure i
Tactic:
cases step with
| εStep _ _ step =>
  exact εClosure.step (εStep_of_εStep step) ih
Proof state after:
no goals
Theorem: Regex.NFA.εClosure_of_pathIn
Proof state before:
case step.εStep
i✝ i' : ℕ
nfa : NFA
start : ℕ
cs✝ : List Char
i j k : ℕ
cs cs' : List Char
rest✝ : nfa.pathIn start j k []
ih : k ∈ nfa.εClosure j
h : True
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ k ∈ nfa.εClosure i
Tactic:
exact εClosure.step (εStep_of_εStep step) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] ↔ i' ∈ nfa.εClosure i
Tactic:
apply Iff.intro
Proof state after:
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i

case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i

case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Tactic:
. exact εClosure_of_pathIn
Proof state after:
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Tactic:
. intro h
  induction h with
  | base => exact .base (Nat.zero_le _)
  | @step i j k step _ ih =>
    cases Nat.decLt i nfa.nodes.size with
    | isTrue lt =>
      simp [εStep, lt] at step
      exact .step (.εStep (Nat.zero_le _) lt step) ih
    | isFalse nlt => simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mp
i i' : ℕ
nfa : NFA
⊢ nfa.pathIn 0 i i' [] → i' ∈ nfa.εClosure i
Tactic:
exact εClosure_of_pathIn
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr
i i' : ℕ
nfa : NFA
⊢ i' ∈ nfa.εClosure i → nfa.pathIn 0 i i' []
Tactic:
intro h
Proof state after:
case mpr
i i' : ℕ
nfa : NFA
h : i' ∈ nfa.εClosure i
⊢ nfa.pathIn 0 i i' []
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr
i i' : ℕ
nfa : NFA
h : i' ∈ nfa.εClosure i
⊢ nfa.pathIn 0 i i' []
Tactic:
induction h with
| base => exact .base (Nat.zero_le _)
| @step i j k step _ ih =>
  cases Nat.decLt i nfa.nodes.size with
  | isTrue lt =>
    simp [εStep, lt] at step
    exact .step (.εStep (Nat.zero_le _) lt step) ih
  | isFalse nlt => simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr.base
i i' : ℕ
nfa : NFA
i✝ : ℕ
⊢ nfa.pathIn 0 i✝ i✝ []
Tactic:
exact .base (Nat.zero_le _)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr.step
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
⊢ nfa.pathIn 0 i k []
Tactic:
cases Nat.decLt i nfa.nodes.size with
| isTrue lt =>
  simp [εStep, lt] at step
  exact .step (.εStep (Nat.zero_le _) lt step) ih
| isFalse nlt => simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
⊢ nfa.pathIn 0 i k []
Tactic:
simp [εStep, lt] at step
Proof state after:
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathIn 0 i k []
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr.step.isTrue
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathIn 0 i k []
Tactic:
exact .step (.εStep (Nat.zero_le _) lt step) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_iff_εClosure
Proof state before:
case mpr.step.isFalse
i✝ i' : ℕ
nfa : NFA
i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : nfa.pathIn 0 j k []
nlt : ¬i < nfa.nodes.size
⊢ nfa.pathIn 0 i k []
Tactic:
simp [εStep, nlt] at step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c])
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k
Tactic:
generalize h : cs ++ [c] = cs' at path
Proof state after:
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h : cs ++ [c] = cs'
path : nfa.pathIn start i l cs'
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h : cs ++ [c] = cs'
path : nfa.pathIn start i l cs'
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k
Tactic:
induction path generalizing cs with
| base _ => simp at h
| @step i j k cs₁ cs₂ step rest ih =>
  match snoc_eq_append h with
  | .inl ⟨h₁, h₂⟩ =>
    simp [h₁, h₂] at step rest
    have := step.nil_of_snoc
    simp [this] at *
    cases step with
    | charStep le _ step =>
      exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
  | .inr ⟨cs₂', h₁, h₂⟩ =>
    have ⟨j', k', path', step', cls⟩ := ih h₂.symm
    exact ⟨j', k', h₁ ▸ .step step path', step', cls⟩
Proof state after:
no goals