internlm/Lean-Github huggingface dataset:
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
hi : ↑i = 0
⊢ Data.Expr.matches cs r
Tactic:
have : nfa.pathIn 0 nfa.start i cs := pathIn_of_reaches 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
this : nfa.pathIn 0 (↑nfa.start) (↑i) cs
⊢ Data.Expr.matches cs r
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
hi : ↑i = 0
this : nfa.pathIn 0 (↑nfa.start) (↑i) cs
⊢ Data.Expr.matches cs r
Tactic:
have := pathToNext_of_compile_of_pathIn eq (hi ▸ this)
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
this✝ : nfa.pathIn 0 (↑nfa.start) (↑i) cs
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Data.Expr.matches cs r
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
hi : ↑i = 0
this✝ : nfa.pathIn 0 (↑nfa.start) (↑i) cs
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ Data.Expr.matches cs r
Tactic:
exact (matches_iff_pathToNext eq).mpr this
Proof state after:
no goals
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have := (matches_iff_pathToNext eq).mp m
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this : nfa.pathToNext 0 1 (↑nfa.start) cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have := pathIn_of_pathToNext this
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn (min 1 0) (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn (min 1 0) (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
simp at this
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
let i' : Fin nfa.nodes.size := ⟨0, lt_zero_size_compile eq⟩
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝ : nfa.pathToNext 0 1 (↑nfa.start) cs
this : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have := reaches_of_pathIn (i := i') this
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
have hdone := (done_iff_zero_compile eq i').mpr rfl
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
hdone : nfa[i'] = Node.done
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Theorem: Regex.NFA.reaches_of_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
this✝¹ : nfa.pathToNext 0 1 (↑nfa.start) cs
this✝ : nfa.pathIn 0 (↑nfa.start) 0 cs
i' : Fin nfa.nodes.size := ⟨0, ⋯⟩
this : nfa.reaches i' cs
hdone : nfa[i'] = Node.done
⊢ ∃ i, nfa.reaches i cs ∧ nfa[i] = Node.done
Tactic:
exact ⟨i', this, hdone⟩
Proof state after:
no goals
Theorem: Regex.NFA.eq_next_of_pathToNext
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
path : (↑result).pathToNext next' nfa.nodes.size i cs
⊢ next' = ↑next
Tactic:
obtain ⟨i', pcs, scs, _, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
⊢ next' = ↑next
Theorem: Regex.NFA.eq_next_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
⊢ next' = ↑next
Tactic:
have := eq_or_ge_of_step_pushRegex eq (le_of_pathIn_right path) step.h₂ step.step
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
this : next' = ↑next ∨ nfa.nodes.size ≤ next'
⊢ next' = ↑next
Theorem: Regex.NFA.eq_next_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
this : next' = ↑next ∨ nfa.nodes.size ≤ next'
⊢ next' = ↑next
Tactic:
cases this with
| inl eq => exact eq
| inr ge => exfalso; exact Nat.not_le_of_lt assm ge
Proof state after:
no goals
Theorem: Regex.NFA.eq_next_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq✝ : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
eq : next' = ↑next
⊢ next' = ↑next
Tactic:
exact eq
Proof state after:
no goals
Theorem: Regex.NFA.eq_next_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
ge : nfa.nodes.size ≤ next'
⊢ next' = ↑next
Tactic:
exfalso
Proof state after:
case intro.intro.intro.intro.intro.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
ge : nfa.nodes.size ≤ next'
⊢ False
Theorem: Regex.NFA.eq_next_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
ge : nfa.nodes.size ≤ next'
⊢ False
Tactic:
exact Nat.not_le_of_lt assm ge
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_split
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i : ℕ
cs : List Char
start : ℕ
eq : nfa.pushRegex next r = result
assm₁ : i' < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
path : (↑result).pathIn start i i' cs
⊢ ∃ cs₁ cs₂, cs = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) i' cs₂
Tactic:
induction path with
| base _ => exact absurd assm₁ (Nat.not_lt_of_le assm₂)
| @step i j k cs cs' step rest ih =>
  have := eq_or_ge_of_step_pushRegex eq assm₂ step.h₂ step.step
  cases this with
  | inl eq =>
    simp [eq] at step rest
    have pathToNext : pathToNext result next nfa.nodes.size i cs :=
      ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
    exact ⟨cs, cs', rfl, pathToNext, rest⟩
  | inr ge =>
    obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
    exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_split
Proof state before:
case base
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i : ℕ
cs : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i✝ : ℕ
h✝ : start ≤ i✝
assm₁ : i✝ < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i✝
⊢ ∃ cs₁ cs₂,
    [] = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i✝ cs₁ ∧ (↑result).pathIn start (↑next) i✝ cs₂
Tactic:
exact absurd assm₁ (Nat.not_lt_of_le assm₂)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
have := eq_or_ge_of_step_pushRegex eq assm₂ step.h₂ step.step
Proof state after:
case step
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
this : j = ↑next ∨ nfa.nodes.size ≤ j
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
this : j = ↑next ∨ nfa.nodes.size ≤ j
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
cases this with
| inl eq =>
  simp [eq] at step rest
  have pathToNext : pathToNext result next nfa.nodes.size i cs :=
    ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
  exact ⟨cs, cs', rfl, pathToNext, rest⟩
| inr ge =>
  obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
  exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
simp [eq] at step rest
Proof state after:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
have pathToNext : pathToNext result next nfa.nodes.size i cs :=
  ⟨i, [], cs, rfl, .base assm₂, step.castStart' assm₂⟩
Proof state after:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size i cs
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq✝ : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
eq : j = ↑next
step : (↑result).stepIn start i (↑next) cs
rest : (↑result).pathIn start (↑next) k cs'
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size i cs
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
exact ⟨cs, cs', rfl, pathToNext, rest⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step.inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
obtain ⟨cs₁, cs₂, eqs, pathToNext, pathIn⟩ := ih assm₁ ge
Proof state after:
case step.inr.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size j cs₁
pathIn : (↑result).pathIn start (↑next) k cs₂
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Theorem: Regex.NFA.pathIn_split
Proof state before:
case step.inr.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size j cs₁
pathIn : (↑result).pathIn start (↑next) k cs₂
⊢ ∃ cs₁ cs₂,
    cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
Tactic:
exact ⟨cs ++ cs₁, cs₂, by simp [eqs], pathToNext.cons (step.castStart' assm₂), pathIn⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_split
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i✝ : ℕ
cs✝ : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn start i j cs
rest : (↑result).pathIn start j k cs'
ih :
  k < nfa.nodes.size →
    nfa.nodes.size ≤ j →
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size j cs₁ ∧ (↑result).pathIn start (↑next) k cs₂
assm₁ : k < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i
ge : nfa.nodes.size ≤ j
cs₁ cs₂ : List Char
eqs : cs' = cs₁ ++ cs₂
pathToNext : (↑result).pathToNext (↑next) nfa.nodes.size j cs₁
pathIn : (↑result).pathIn start (↑next) k cs₂
⊢ cs ++ cs' = cs ++ cs₁ ++ cs₂
Tactic:
simp [eqs]
Proof state after:
no goals
Theorem: Regex.NFA.rStart_of_push_star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∃ rStart, nfa.nodes.size + 1 ≤ rStart ∧ (↑result)[nfa.nodes.size] = Node.split rStart ↑next
Tactic:
apply pushRegex.star eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa' : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'.nodes.size),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ →
              ∃ rStart, nfa.nodes.size + 1 ≤ rStart ∧ (↑result)[nfa.nodes.size] = Node.split rStart ↑next