internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.pathIn.trans
Proof state before:
case step
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i✝ j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ k✝ cs₂✝
ih : nfa.pathIn start k✝ k cs' → nfa.pathIn start j✝ k (cs₂✝ ++ cs')
path₂ : nfa.pathIn start k✝ k cs'
⊢ nfa.pathIn start i✝ k (cs₁✝ ++ cs₂✝ ++ cs')
Tactic:
simp
Proof state after:
case step
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i✝ j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ k✝ cs₂✝
ih : nfa.pathIn start k✝ k cs' → nfa.pathIn start j✝ k (cs₂✝ ++ cs')
path₂ : nfa.pathIn start k✝ k cs'
⊢ nfa.pathIn start i✝ k (cs₁✝ ++ (cs₂✝ ++ cs'))
Theorem: Regex.NFA.pathIn.trans
Proof state before:
case step
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i✝ j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ k✝ cs₂✝
ih : nfa.pathIn start k✝ k cs' → nfa.pathIn start j✝ k (cs₂✝ ++ cs')
path₂ : nfa.pathIn start k✝ k cs'
⊢ nfa.pathIn start i✝ k (cs₁✝ ++ (cs₂✝ ++ cs'))
Tactic:
exact .step step (ih path₂)
Proof state after:
no goals
Theorem: Regex.NFA.le_of_pathToNext
Proof state before:
nfa : NFA
next i : ℕ
cs : List Char
start : ℕ
path : nfa.pathToNext next start i cs
⊢ start ≤ i
Tactic:
obtain ⟨_, _, _, _, path, _⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next i : ℕ
cs : List Char
start w✝² : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : nfa.pathIn start i w✝² w✝¹
right✝ : nfa.stepIn start w✝² next w✝
⊢ start ≤ i
Theorem: Regex.NFA.le_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next i : ℕ
cs : List Char
start w✝² : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : nfa.pathIn start i w✝² w✝¹
right✝ : nfa.stepIn start w✝² next w✝
⊢ start ≤ i
Tactic:
exact le_of_pathIn_left path
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.cons
Proof state before:
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
path : nfa.pathToNext next start j cs₂
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step'⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
eqs : cs₂ = pcs ++ scs
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext.cons
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
eqs : cs₂ = pcs ++ scs
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)
Tactic:
subst eqs
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ (pcs ++ scs))
Theorem: Regex.NFA.pathToNext.cons
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ (pcs ++ scs))
Tactic:
cases step with
| charStep h₁ h₂ step =>
  exact ⟨i', _ :: pcs, scs, rfl, .step (.charStep h₁ h₂ step) path, step'⟩
| εStep h₁ h₂ step =>
  exact ⟨i', pcs, scs, rfl, .step (.εStep h₁ h₂ step) path, step'⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.cons
Proof state before:
case intro.intro.intro.intro.intro.charStep
nfa : NFA
i j next start i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
c✝ : Char
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ nfa.pathToNext next start i ([c✝] ++ (pcs ++ scs))
Tactic:
exact ⟨i', _ :: pcs, scs, rfl, .step (.charStep h₁ h₂ step) path, step'⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.cons
Proof state before:
case intro.intro.intro.intro.intro.εStep
nfa : NFA
i j next start i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathToNext next start i ([] ++ (pcs ++ scs))
Tactic:
exact ⟨i', pcs, scs, rfl, .step (.εStep h₁ h₂ step) path, step'⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.cast
Proof state before:
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
path : nfa.pathToNext next start i cs
⊢ nfa'.pathToNext next start i cs
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa'.pathToNext next start i cs
Theorem: Regex.NFA.pathToNext.cast
Proof state before:
case intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa'.pathToNext next start i cs
Tactic:
obtain ⟨h', eq'⟩ := eq _ (le_of_pathIn_right path) step.h₂
Proof state after:
case intro.intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
h' : i' < nfa'.nodes.size
eq' : nfa[i'] = nfa'[i']
⊢ nfa'.pathToNext next start i cs
Theorem: Regex.NFA.pathToNext.cast
Proof state before:
case intro.intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
h' : i' < nfa'.nodes.size
eq' : nfa[i'] = nfa'[i']
⊢ nfa'.pathToNext next start i cs
Tactic:
exact ⟨i', pcs, scs, eqs, pathIn.cast start eq path, step.cast h' eq'⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.cast'
Proof state before:
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
path : nfa'.pathToNext next start i cs
⊢ nfa.pathToNext next start i cs
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa'.pathIn start i i' pcs
step : nfa'.stepIn start i' next scs
⊢ nfa.pathToNext next start i cs
Theorem: Regex.NFA.pathToNext.cast'
Proof state before:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa'.pathIn start i i' pcs
step : nfa'.stepIn start i' next scs
⊢ nfa.pathToNext next start i cs
Tactic:
have path' := path.cast' assm le eq
Proof state after:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa'.pathIn start i i' pcs
step : nfa'.stepIn start i' next scs
path' : nfa.pathIn start i i' pcs
⊢ nfa.pathToNext next start i cs
Theorem: Regex.NFA.pathToNext.cast'
Proof state before:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa'.pathIn start i i' pcs
step : nfa'.stepIn start i' next scs
path' : nfa.pathIn start i i' pcs
⊢ nfa.pathToNext next start i cs
Tactic:
have lt : i' < nfa.nodes.size := path'.lt_right assm
Proof state after:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa'.pathIn start i i' pcs
step : nfa'.stepIn start i' next scs
path' : nfa.pathIn start i i' pcs
lt : i' < nfa.nodes.size
⊢ nfa.pathToNext next start i cs
Theorem: Regex.NFA.pathToNext.cast'
Proof state before:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa'.pathIn start i i' pcs
step : nfa'.stepIn start i' next scs
path' : nfa.pathIn start i i' pcs
lt : i' < nfa.nodes.size
⊢ nfa.pathToNext next start i cs
Tactic:
exact ⟨i', pcs, scs, eqs, path', step.cast lt (eq i' step.h₁ lt).symm⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.castStart
Proof state before:
next : ℕ
nfa : NFA
start start' i : ℕ
cs : List Char
le : start' ≤ start
path : nfa.pathToNext next start i cs
⊢ nfa.pathToNext next start' i cs
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
next : ℕ
nfa : NFA
start start' i : ℕ
cs : List Char
le : start' ≤ start
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start' i cs
Theorem: Regex.NFA.pathToNext.castStart
Proof state before:
case intro.intro.intro.intro.intro
next : ℕ
nfa : NFA
start start' i : ℕ
cs : List Char
le : start' ≤ start
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start' i cs
Tactic:
exact ⟨i', pcs, scs, eqs, path.castStart le, step.castStart le⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.castLE
Proof state before:
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
path : nfa.pathToNext next start i cs
⊢ nfa.pathToNext next start' i cs
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start' i cs
Theorem: Regex.NFA.pathToNext.castLE
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start' i cs
Tactic:
have path' := path.castLE assm inBounds
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
path' : nfa.pathIn start' i i' pcs
⊢ nfa.pathToNext next start' i cs
Theorem: Regex.NFA.pathToNext.castLE
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
path' : nfa.pathIn start' i i' pcs
⊢ nfa.pathToNext next start' i cs
Tactic:
exact ⟨i', pcs, scs, eqs, path', step.castStart' (le_of_pathIn_right path')⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.trans
Proof state before:
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
path₁ : nfa.pathToNext j start i cs
path₂ : nfa.pathToNext k start j cs'
⊢ nfa.pathToNext k start i (cs ++ cs')
Tactic:
obtain ⟨i₁, pcs₁, scs₁, eqs₁, path₁, step₁⟩ := path₁
Proof state after:
case intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
path₂ : nfa.pathToNext k start j cs'
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
⊢ nfa.pathToNext k start i (cs ++ cs')
Theorem: Regex.NFA.pathToNext.trans
Proof state before:
case intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
path₂ : nfa.pathToNext k start j cs'
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
⊢ nfa.pathToNext k start i (cs ++ cs')
Tactic:
obtain ⟨i₂, pcs₂, scs₂, eqs₂, path₂, step₂⟩ := path₂
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ nfa.pathToNext k start i (cs ++ cs')
Theorem: Regex.NFA.pathToNext.trans
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ nfa.pathToNext k start i (cs ++ cs')
Tactic:
exact ⟨i₂, pcs₁ ++ (scs₁ ++ pcs₂), scs₂, by simp [eqs₁, eqs₂], path₁.trans (.step step₁ path₂), step₂⟩
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext.trans
Proof state before:
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ cs ++ cs' = pcs₁ ++ (scs₁ ++ pcs₂) ++ scs₂
Tactic:
simp [eqs₁, eqs₂]
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_of_pathToNext
Proof state before:
next i : ℕ
cs : List Char
nfa : NFA
start : ℕ
path : nfa.pathToNext next start i cs
⊢ nfa.pathIn (min start next) i next cs
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
Proof state after:
case intro.intro.intro.intro.intro
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathIn (min start next) i next cs
Theorem: Regex.NFA.pathIn_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathIn (min start next) i next cs
Tactic:
cases step with
| charStep h₁ h₂ step => exact eqs ▸ path.snoc_char h₂ step
| εStep h₁ h₂ step => simp [eqs, path.snoc_ε h₂ step]
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro.charStep
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs : List Char
path : nfa.pathIn start i i' pcs
c✝ : Char
h₁ : start ≤ i'
h₂ : i' < nfa.nodes.size
step : next ∈ nfa[i'].charStep c✝
eqs : cs = pcs ++ [c✝]
⊢ nfa.pathIn (min start next) i next cs
Tactic:
exact eqs ▸ path.snoc_char h₂ step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn_of_pathToNext
Proof state before:
case intro.intro.intro.intro.intro.εStep
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs : List Char
path : nfa.pathIn start i i' pcs
h₁ : start ≤ i'
h₂ : i' < nfa.nodes.size
step : next ∈ nfa[i'].εStep
eqs : cs = pcs ++ []
⊢ nfa.pathIn (min start next) i next cs
Tactic:
simp [eqs, path.snoc_ε h₂ step]
Proof state after:
no goals
Theorem: Fin.eq_of_ge
Proof state before:
n : Nat
i : Fin (n + 1)
h : ↑i ≥ n
⊢ i = ⟨n, ⋯⟩
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case a
n : Nat
i : Fin (n + 1)
h : ↑i ≥ n
⊢ ↑i = ↑⟨n, ⋯⟩
Theorem: Fin.eq_of_ge
Proof state before:
case a
n : Nat
i : Fin (n + 1)
h : ↑i ≥ n
⊢ ↑i = ↑⟨n, ⋯⟩
Tactic:
exact Nat.le_antisymm (Nat.le_of_succ_le_succ i.isLt) h
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof state before:
n : Nat
f : Fin n → Fin n
h : inj f
⊢ surj f
Tactic:
induction n with
| zero =>
  intro y
  have : y.val < 0 := y.isLt
  contradiction
| succ n ih =>
  let n' : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  let f' (x : Fin n) : Fin n :=
    let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
    let y := f x'
    if isLt : y.val < n then
      ⟨y.val, isLt⟩
    else
      have eqx : f x' = n' := Fin.eq_of_not_lt isLt
      have isLt : f n' < n' := by
        by_contra nlt
        have eqn : f n' = n' := Fin.eq_of_not_lt nlt
        have : f x' = f n' := by rw [eqx, eqn]
        have : x' = n' := h _ _ this
        have : x.val = n := by
          have : x'.val = n'.val := by rw [this]
          exact this
        exact Nat.lt_irrefl _ (this ▸ x.isLt)
      ⟨f ⟨n, Nat.lt_succ_self n⟩, isLt⟩
  have : inj f' := by
    intro x y eq
    let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
    let y' : Fin (n + 1) := ⟨y.val, Nat.lt_trans y.isLt (Nat.lt_succ_self n)⟩
    if hx : f x' < n then
      if hy : f y' < n then
        simp [f', hx, hy] at eq
        have := h _ _ (Fin.eq_of_val_eq eq)
        simp at this
        exact Fin.eq_of_val_eq this
      else
        simp [f', hx, hy] at eq
        have := h _ _ (Fin.eq_of_val_eq eq)
        simp at this
        exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
    else
      if hy : f y' < n then
        simp [f', hx, hy] at eq
        have := h _ _ (Fin.eq_of_val_eq eq)
        simp at this
        exact absurd (this.symm ▸ y.isLt) (Nat.lt_irrefl _)
      else
        have eqx := Fin.eq_of_not_lt hx
        have eqy := Fin.eq_of_not_lt hy
        have : f x' = f y' := by rw [eqx, eqy]
        have : x' = y' := h _ _ this
        have : x.val = y.val := by
          have : x'.val = y'.val := by rw [this]
          exact this
        exact Fin.eq_of_val_eq this
  have surj : surj f' := ih _ this
  intro y
  have : y.val ≤ n := Nat.le_of_succ_le_succ y.isLt
  if isLt : y.val < n then
    let ⟨x, eq⟩ := surj ⟨y.val, isLt⟩
    simp [f'] at eq
    split at eq
    case inl =>
      simp at eq
      exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, Fin.eq_of_val_eq eq⟩
    case inr =>
      simp at eq
      exact ⟨n', Fin.eq_of_val_eq eq⟩
  else
    have := Fin.eq_of_not_lt isLt
    simp [this]
    if isLt' : f n' < n then
      let ⟨x, eq⟩ := surj ⟨(f n').val, isLt'⟩
      simp [f'] at eq
      split at eq
      case inl =>
        simp at eq
        have := Fin.val_eq_of_eq (h _ _ (Fin.eq_of_val_eq eq))
        simp at this
        exact absurd (this ▸ x.isLt) (Nat.lt_irrefl _)
      case inr nlt =>
        have := Fin.eq_of_not_lt nlt
        exact ⟨⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩, this⟩
    else
      exact ⟨n', Fin.eq_of_not_lt isLt'⟩
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof state before:
case zero
f : Fin 0 → Fin 0
h : inj f
⊢ surj f
Tactic:
intro y
Proof state after:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
⊢ ∃ x, f x = y
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof state before:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
⊢ ∃ x, f x = y
Tactic:
have : y.val < 0 := y.isLt
Proof state after:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
this : ↑y < 0
⊢ ∃ x, f x = y
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof state before:
case zero
f : Fin 0 → Fin 0
h : inj f
y : Fin 0
this : ↑y < 0
⊢ ∃ x, f x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof state before:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
⊢ surj f
Tactic:
let n' : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
Proof state after:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
⊢ surj f
Theorem: Regex.Data.SparseSet.Bijection.surj_of_inj
Proof state before:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
⊢ surj f
Tactic:
let f' (x : Fin n) : Fin n :=
  let x' : Fin (n + 1) := ⟨x.val, Nat.lt_trans x.isLt (Nat.lt_succ_self n)⟩
  let y := f x'
  if isLt : y.val < n then
    ⟨y.val, isLt⟩
  else
    have eqx : f x' = n' := Fin.eq_of_not_lt isLt
    have isLt : f n' < n' := by
      by_contra nlt
      have eqn : f n' = n' := Fin.eq_of_not_lt nlt
      have : f x' = f n' := by rw [eqx, eqn]
      have : x' = n' := h _ _ this
      have : x.val = n := by
        have : x'.val = n'.val := by rw [this]
        exact this
      exact Nat.lt_irrefl _ (this ▸ x.isLt)
    ⟨f ⟨n, Nat.lt_succ_self n⟩, isLt⟩
Proof state after:
case succ
n : Nat
ih : ∀ (f : Fin n → Fin n), inj f → surj f
f : Fin (n + 1) → Fin (n + 1)
h : inj f
n' : Fin (n + 1) := ⟨n, ⋯⟩
f' : Fin n → Fin n :=
  fun x =>
    let x' := ⟨↑x, ⋯⟩;
    let y := f x';
    if isLt : ↑y < n then ⟨↑y, isLt⟩
    else
      let_fun eqx := ⋯;
      let_fun isLt := ⋯;
      ⟨↑(f ⟨n, ⋯⟩), isLt⟩
⊢ surj f