internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case base
nfa : NFA
i l : ℕ
c : Char
start : ℕ
cs' : List Char
i✝ : ℕ
h✝ : start ≤ i✝
cs : List Char
h : cs ++ [c] = []
⊢ ∃ j k, nfa.pathIn start i✝ j cs ∧ k ∈ nfa.charStep j c ∧ i✝ ∈ nfa.εClosure k
Tactic:
simp at h
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case step
nfa : NFA
i✝ l : ℕ
c : Char
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 : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
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
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i✝ l : ℕ
c : Char
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 : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
simp [h₁, h₂] at step rest
Proof state after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
have := step.nil_of_snoc
Proof state after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
this : cs = []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
this : cs = []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
simp [this] at *
Proof state after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ cs : List Char
h₂ : cs₂ = []
rest : nfa.pathIn start j k []
ih :
  ∀ {cs : List Char}, cs ++ [c] = cs₂ → ∃ j_1, nfa.pathIn start j j_1 cs ∧ ∃ x ∈ nfa.charStep j_1 c, k ∈ nfa.εClosure x
h : [c] = cs₁ ++ cs₂
h₁ : cs₁ = [c]
step : nfa.stepIn start i j [c]
this : True
⊢ ∃ j, nfa.pathIn start i j [] ∧ ∃ x ∈ nfa.charStep j c, k ∈ nfa.εClosure x
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ cs : List Char
h₂ : cs₂ = []
rest : nfa.pathIn start j k []
ih :
  ∀ {cs : List Char}, cs ++ [c] = cs₂ → ∃ j_1, nfa.pathIn start j j_1 cs ∧ ∃ x ∈ nfa.charStep j_1 c, k ∈ nfa.εClosure x
h : [c] = cs₁ ++ cs₂
h₁ : cs₁ = [c]
step : nfa.stepIn start i j [c]
this : True
⊢ ∃ j, nfa.pathIn start i j [] ∧ ∃ x ∈ nfa.charStep j c, k ∈ nfa.εClosure x
Tactic:
cases step with
| charStep le _ step =>
  exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case charStep
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ cs : List Char
h₂ : cs₂ = []
rest : nfa.pathIn start j k []
ih :
  ∀ {cs : List Char}, cs ++ [c] = cs₂ → ∃ j_1, nfa.pathIn start j j_1 cs ∧ ∃ x ∈ nfa.charStep j_1 c, k ∈ nfa.εClosure x
h : [c] = cs₁ ++ cs₂
h₁ : cs₁ = [c]
this : True
le : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c
⊢ ∃ j, nfa.pathIn start i j [] ∧ ∃ x ∈ nfa.charStep j c, k ∈ nfa.εClosure x
Tactic:
exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i✝ l : ℕ
c : Char
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 : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
cs₂' : List Char
h₁ : cs = cs₁ ++ cs₂'
h₂ : cs₂ = cs₂' ++ [c]
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
have ⟨j', k', path', step', cls⟩ := ih h₂.symm
Proof state after:
nfa : NFA
i✝ l : ℕ
c : Char
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 : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
cs₂' : List Char
h₁ : cs = cs₁ ++ cs₂'
h₂ : cs₂ = cs₂' ++ [c]
j' k' : ℕ
path' : nfa.pathIn start j j' cs₂'
step' : k' ∈ nfa.charStep j' c
cls : k ∈ nfa.εClosure k'
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
nfa : NFA
i✝ l : ℕ
c : Char
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 : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
cs₂' : List Char
h₁ : cs = cs₁ ++ cs₂'
h₂ : cs₂ = cs₂' ++ [c]
j' k' : ℕ
path' : nfa.pathIn start j j' cs₂'
step' : k' ∈ nfa.charStep j' c
cls : k ∈ nfa.εClosure k'
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
exact ⟨j', k', h₁ ▸ .step step path', step', cls⟩
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✝])
cs₁ cs₂ cs₃ : List Char
c : Char
h : cs₁ ++ [c] = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ = cs₃' ++ [c]
Tactic:
cases cs₃ using List.list_reverse_induction with
| base =>
  simp at h
  exact .inl ⟨h.symm, rfl⟩
| ind cs₃ c' =>
  have : c = c' ∧ cs₁ = cs₂ ++ cs₃ := by
    have h₁ := congrArg List.reverse h
    simp at h₁
    have h₂ := congrArg List.reverse h₁.right
    simp at h₂
    exact ⟨h₁.left, h₂⟩
  simp [this]
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case base
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
h : cs₁ ++ [c] = cs₂ ++ []
⊢ cs₂ = cs₁ ++ [c] ∧ [] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ [] = cs₃' ++ [c]
Tactic:
simp at h
Proof state after:
case base
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
h : cs₁ ++ [c] = cs₂
⊢ cs₂ = cs₁ ++ [c] ∧ [] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ [] = cs₃' ++ [c]
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case base
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
h : cs₁ ++ [c] = cs₂
⊢ cs₂ = cs₁ ++ [c] ∧ [] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ [] = cs₃' ++ [c]
Tactic:
exact .inl ⟨h.symm, rfl⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
Tactic:
have : c = c' ∧ cs₁ = cs₂ ++ cs₃ := by
  have h₁ := congrArg List.reverse h
  simp at h₁
  have h₂ := congrArg List.reverse h₁.right
  simp at h₂
  exact ⟨h₁.left, h₂⟩
Proof state after:
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
this : c = c' ∧ cs₁ = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
Theorem: Regex.NFA.pathIn.of_snoc_char
Proof state before:
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
this : c = c' ∧ cs₁ = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
Tactic:
simp [this]
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✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
have h₁ := congrArg List.reverse h
Proof state after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : (cs₁ ++ [c]).reverse = (cs₂ ++ (cs₃ ++ [c'])).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
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✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : (cs₁ ++ [c]).reverse = (cs₂ ++ (cs₃ ++ [c'])).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
simp at h₁
Proof state after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
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✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
have h₂ := congrArg List.reverse h₁.right
Proof state after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁.reverse.reverse = (cs₃.reverse ++ cs₂.reverse).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
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✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁.reverse.reverse = (cs₃.reverse ++ cs₂.reverse).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
simp at h₂
Proof state after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁ = cs₂ ++ cs₃
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
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✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁ = cs₂ ++ cs₃
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
exact ⟨h₁.left, h₂⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
h : nfa.reaches i m
⊢ nfa.pathIn 0 (↑nfa.start) (↑i) m
Tactic:
induction h with
| nil cls => simp [pathIn_iff_εClosure.mpr cls]
| @snoc i j k c m _ step cls ih =>
  simp [charStep] at step
  have ih' : nfa.pathIn (min 0 j) nfa.start j (m ++ [c]) :=
    ih.snoc_char i.isLt step
  simp at ih'
  have := ih'.trans (pathIn_iff_εClosure.mpr cls)
  simp at this
  exact this
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case nil
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
i✝ : Fin nfa.nodes.size
cls : ↑i✝ ∈ nfa.εClosure ↑nfa.start
⊢ nfa.pathIn 0 ↑nfa.start ↑i✝ []
Tactic:
simp [pathIn_iff_εClosure.mpr cls]
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
step : j ∈ nfa.charStep (↑i) c
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
simp [charStep] at step
Proof state after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
have ih' : nfa.pathIn (min 0 j) nfa.start j (m ++ [c]) :=
  ih.snoc_char i.isLt step
Proof state after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn (min 0 j) (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn (min 0 j) (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
simp at ih'
Proof state after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
have := ih'.trans (pathIn_iff_εClosure.mpr cls)
Proof state after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c] ++ [])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c] ++ [])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
simp at this
Proof state after:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Theorem: Regex.NFA.pathIn_of_reaches
Proof state before:
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
Tactic:
exact this
Proof state after:
no goals
Theorem: Regex.NFA.reaches_of_pathIn
Proof state before:
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
h : nfa.pathIn 0 (↑nfa.start) (↑i) m
⊢ nfa.reaches i m
Tactic:
induction m using List.list_reverse_induction generalizing i with
| base => exact .nil (pathIn_iff_εClosure.mp h)
| ind m c ih =>
  have ⟨j, k, path, step, cls⟩ := pathIn.of_snoc_char h
  let j' : Fin nfa.nodes.size := ⟨j, path.lt_right nfa.start.isLt⟩
  have prev := ih (i := j') path
  exact .snoc prev step cls
Proof state after:
no goals
Theorem: Regex.NFA.reaches_of_pathIn
Proof state before:
case base
nfa : NFA
i : Fin nfa.nodes.size
h : nfa.pathIn 0 ↑nfa.start ↑i []
⊢ nfa.reaches i []
Tactic:
exact .nil (pathIn_iff_εClosure.mp h)
Proof state after:
no goals
Theorem: Regex.NFA.reaches_of_pathIn
Proof state before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
⊢ nfa.reaches i (m ++ [c])
Tactic:
have ⟨j, k, path, step, cls⟩ := pathIn.of_snoc_char h
Proof state after:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
⊢ nfa.reaches i (m ++ [c])
Theorem: Regex.NFA.reaches_of_pathIn
Proof state before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
⊢ nfa.reaches i (m ++ [c])
Tactic:
let j' : Fin nfa.nodes.size := ⟨j, path.lt_right nfa.start.isLt⟩
Proof state after:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
⊢ nfa.reaches i (m ++ [c])
Theorem: Regex.NFA.reaches_of_pathIn
Proof state before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
⊢ nfa.reaches i (m ++ [c])
Tactic:
have prev := ih (i := j') path
Proof state after:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
prev : nfa.reaches j' m
⊢ nfa.reaches i (m ++ [c])
Theorem: Regex.NFA.reaches_of_pathIn
Proof state before:
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
prev : nfa.reaches j' m
⊢ nfa.reaches i (m ++ [c])
Tactic:
exact .snoc prev step cls
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_reaches
Proof state before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
⊢ Data.Expr.matches cs r
Tactic:
have hi : i.val = 0 := (done_iff_zero_compile eq i).mp h₂
Proof state after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
⊢ Data.Expr.matches cs r