internlm/Lean-Github huggingface dataset:
Theorem: Regex.VM.eachStepChar_spec.mem_done_iff.go
Proof 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]
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
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
Proof 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
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
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
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
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
Proof 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
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
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]
Proof state after:
no goals
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
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
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
apply eachStepChar_spec.mem_done_iff.go 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
⊢ ∀ j ∈ next, nfa[j] ≠ Node.done
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
⊢ ∀ j ∈ next, nfa[j] ≠ Node.done
Tactic:
intro j hmem
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
j : Fin nfa.nodes.size
hmem : j ∈ next
⊢ nfa[j] ≠ Node.done
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
j : Fin nfa.nodes.size
hmem : j ∈ next
⊢ nfa[j] ≠ Node.done
Tactic:
have : j ∉ next := SparseSet.not_mem_of_isEmpty hemp
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
j : Fin nfa.nodes.size
hmem : j ∈ next
this : j ∉ next
⊢ nfa[j] ≠ Node.done
Theorem: Regex.VM.eachStepChar_spec.mem_done_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
j : Fin nfa.nodes.size
hmem : j ∈ next
this : j ∉ next
⊢ nfa[j] ≠ Node.done
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
assm₁ : 0 < i
assm₂ : next = 0
path : nfa.pathIn 0 i next cs
⊢ nfa.pathToNext 0 1 i cs
Tactic:
induction path with
| base _ =>
  subst assm₂
  contradiction
| @step i j k cs cs' step rest ih =>
  cases rest with
  | base _ =>
    subst assm₂
    exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
  | step step' rest =>
    have : 0 < j := by
      cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
      | inl eqj =>
        have : 0 < nfa.nodes.size :=
          calc
            0 < 1 := by decide
            _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
            _ = _ := by simp [←eq, compile]
        have hn : nfa[0] = .done := by
          simp [←eq]
          unfold compile
          rw [pushRegex_get_lt rfl 0 (by decide)]
          rfl
        simp [eqj] at hn
        cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
      | inr gt => exact gt
    have ih := ih this assm₂
    apply ih.cons (step.castStart' assm₁)
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case base
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
i✝ : ℕ
h✝ : 0 ≤ i✝
assm₁ : 0 < i✝
assm₂ : i✝ = 0
⊢ nfa.pathToNext 0 1 i✝ []
Tactic:
subst assm₂
Proof state after:
case base
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
h✝ : 0 ≤ 0
assm₁ : 0 < 0
⊢ nfa.pathToNext 0 1 0 []
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case base
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
h✝ : 0 ≤ 0
assm₁ : 0 < 0
⊢ nfa.pathToNext 0 1 0 []
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn 0 i j cs
rest : nfa.pathIn 0 j k cs'
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j cs'
assm₁ : 0 < i
assm₂ : k = 0
⊢ nfa.pathToNext 0 1 i (cs ++ cs')
Tactic:
cases rest with
| base _ =>
  subst assm₂
  exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
| step step' rest =>
  have : 0 < j := by
    cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
    | inl eqj =>
      have : 0 < nfa.nodes.size :=
        calc
          0 < 1 := by decide
          _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
          _ = _ := by simp [←eq, compile]
      have hn : nfa[0] = .done := by
        simp [←eq]
        unfold compile
        rw [pushRegex_get_lt rfl 0 (by decide)]
        rfl
      simp [eqj] at hn
      cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
    | inr gt => exact gt
  have ih := ih this assm₂
  apply ih.cons (step.castStart' assm₁)
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
h✝ : 0 ≤ j
assm₂ : j = 0
ih : 0 < j → j = 0 → nfa.pathToNext 0 1 j []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
Tactic:
subst assm₂
Proof state after:
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
Tactic:
exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ cs ++ [] = [] ++ cs
Tactic:
simp
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Tactic:
have : 0 < j := by
  cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
  | inl eqj =>
    have : 0 < nfa.nodes.size :=
      calc
        0 < 1 := by decide
        _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
        _ = _ := by simp [←eq, compile]
    have hn : nfa[0] = .done := by
      simp [←eq]
      unfold compile
      rw [pushRegex_get_lt rfl 0 (by decide)]
      rfl
    simp [eqj] at hn
    cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
  | inr gt => exact gt
Proof state after:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Tactic:
have ih := ih this assm₂
Proof state after:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih✝ : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
ih : nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih✝ : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
ih : nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Tactic:
apply ih.cons (step.castStart' assm₁)
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ 0 < j
Tactic:
cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
| inl eqj =>
  have : 0 < nfa.nodes.size :=
    calc
      0 < 1 := by decide
      _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
      _ = _ := by simp [←eq, compile]
  have hn : nfa[0] = .done := by
    simp [←eq]
    unfold compile
    rw [pushRegex_get_lt rfl 0 (by decide)]
    rfl
  simp [eqj] at hn
  cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
| inr gt => exact gt
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ 0 < j
Tactic:
have : 0 < nfa.nodes.size :=
  calc
    0 < 1 := by decide
    _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
    _ = _ := by simp [←eq, compile]
Proof state after:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ 0 < j
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ 0 < j
Tactic:
have hn : nfa[0] = .done := by
  simp [←eq]
  unfold compile
  rw [pushRegex_get_lt rfl 0 (by decide)]
  rfl
Proof state after:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[0] = Node.done
⊢ 0 < j
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[0] = Node.done
⊢ 0 < j
Tactic:
simp [eqj] at hn
Proof state after:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[j] = Node.done
⊢ 0 < j
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[j] = Node.done
⊢ 0 < j
Tactic:
cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux
Proof state before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ 0 < 1
Tactic:
decide
Proof state after:
no goals