internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.le_of_pathIn_right
Proof state before:
case base
nfa : NFA
i j : ℕ
cs : List Char
start i✝ : ℕ
h : start ≤ i✝
⊢ start ≤ i✝
Tactic:
exact h
Proof state after:
no goals
Theorem: Regex.NFA.le_of_pathIn_right
Proof state before:
case step
nfa : NFA
i j : ℕ
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 : start ≤ k✝
⊢ start ≤ k✝
Tactic:
exact ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castStart
Proof state before:
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ start
path : nfa.pathIn start i j cs
⊢ nfa.pathIn start' i j cs
Tactic:
induction path with
| base h => exact .base (Nat.le_trans le h)
| step step _ ih => exact .step (step.castStart le) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castStart
Proof state before:
case base
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ start
i✝ : ℕ
h : start ≤ i✝
⊢ nfa.pathIn start' i✝ i✝ []
Tactic:
exact .base (Nat.le_trans le h)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castStart
Proof state before:
case step
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ 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' j✝ k✝ cs₂✝
⊢ nfa.pathIn start' i✝ k✝ (cs₁✝ ++ cs₂✝)
Tactic:
exact .step (step.castStart le) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast
Proof state before:
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
path : nfa.pathIn start i j cs
⊢ nfa'.pathIn start i j cs
Tactic:
induction path with
| base h => exact .base h
| step step _ ih =>
  let ⟨h, eq⟩ := eq _ step.h₁ step.h₂
  exact .step (step.cast h eq) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast
Proof state before:
case base
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i✝ : ℕ
h : start ≤ i✝
⊢ nfa'.pathIn start i✝ i✝ []
Tactic:
exact .base h
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast
Proof state before:
case step
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
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 j✝ k✝ cs₂✝
⊢ nfa'.pathIn start i✝ k✝ (cs₁✝ ++ cs₂✝)
Tactic:
let ⟨h, eq⟩ := eq _ step.h₁ step.h₂
Proof state after:
case step
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
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 j✝ k✝ cs₂✝
h : i✝ < nfa'.nodes.size
eq : nfa[i✝] = nfa'[i✝]
⊢ nfa'.pathIn start i✝ k✝ (cs₁✝ ++ cs₂✝)
Theorem: Regex.NFA.pathIn.cast
Proof state before:
case step
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
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 j✝ k✝ cs₂✝
h : i✝ < nfa'.nodes.size
eq : nfa[i✝] = nfa'[i✝]
⊢ nfa'.pathIn start i✝ k✝ (cs₁✝ ++ cs₂✝)
Tactic:
exact .step (step.cast h eq) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
i j : ℕ
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'.pathIn start i j cs
⊢ nfa.pathIn start i j cs
Tactic:
induction path with
| base h => exact .base h
| @step i j k cs cs' step _ ih =>
  have eq := eq _ step.h₁ assm
  have : j < nfa.nodes.size := by
    cases step with
    | @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
    | εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
  exact .step (step.cast assm eq.symm) (ih this)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
case base
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
⊢ nfa.pathIn start i✝ i✝ []
Tactic:
exact .base h
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
have eq := eq _ step.h₁ assm
Proof state after:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
⊢ nfa.pathIn start i k (cs ++ cs')
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
have : j < nfa.nodes.size := by
  cases step with
  | @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
  | εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
Proof state after:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
this : j < nfa.nodes.size
⊢ nfa.pathIn start i k (cs ++ cs')
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
this : j < nfa.nodes.size
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
exact .step (step.cast assm eq.symm) (ih this)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs cs' : List Char
step : nfa'.stepIn start i j cs
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
⊢ j < nfa.nodes.size
Tactic:
cases step with
| @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
| εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
case charStep
i✝ j✝ : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs' : List Char
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
c : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa'.nodes.size
step : j ∈ nfa'[i].charStep c
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_charStep (eq.symm ▸ step)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.cast'
Proof state before:
case εStep
i✝ j✝ : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs' : List Char
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
h₁✝ : start ≤ i
h₂✝ : i < nfa'.nodes.size
step : j ∈ nfa'[i].εStep
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_εStep (eq.symm ▸ step)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
cs : List Char
nfa : NFA
start start' i i' : ℕ
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.pathIn start i i' cs
⊢ nfa.pathIn start' i i' cs
Tactic:
induction path with
| base _ => exact .base assm
| @step i j k cs cs' step rest ih =>
  have h₂ := step.h₂
  have : start' ≤ j := by
    cases step with
    | charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
    | εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
  exact .step (step.castStart' assm) (ih this)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
case base
cs : List Char
nfa : NFA
start start' i 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✝ : ℕ
h✝ : start ≤ i✝
assm : start' ≤ i✝
⊢ nfa.pathIn start' i✝ i✝ []
Tactic:
exact .base assm
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
⊢ nfa.pathIn start' i k (cs ++ cs')
Tactic:
have h₂ := step.h₂
Proof state after:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ nfa.pathIn start' i k (cs ++ cs')
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ nfa.pathIn start' i k (cs ++ cs')
Tactic:
have : start' ≤ j := by
  cases step with
  | charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
  | εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
Proof state after:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
this : start' ≤ j
⊢ nfa.pathIn start' i k (cs ++ cs')
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
this : start' ≤ j
⊢ nfa.pathIn start' i k (cs ++ cs')
Tactic:
exact .step (step.castStart' assm) (ih this)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
cs✝ : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ start' ≤ j
Tactic:
cases step with
| charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
| εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
case charStep
cs : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs' : List Char
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ start' ≤ j
Tactic:
exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.castLE
Proof state before:
case εStep
cs : List Char
nfa : NFA
start start' i✝ 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 j k : ℕ
cs' : List Char
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ start' ≤ j
Tactic:
exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
cs : List Char
nfa : NFA
start i i' : ℕ
assm : i < nfa.nodes.size
path : nfa.pathIn start i i' cs
⊢ i' < nfa.nodes.size
Tactic:
induction path with
| base _ => exact assm
| @step i j _ _ _ step _ ih =>
  have : j < nfa.nodes.size := by
    cases step with
    | charStep _ _ step => exact lt_of_charStep step
    | εStep _ _ step => exact lt_of_εStep step
  exact ih this
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
case base
cs : List Char
nfa : NFA
start i i' i✝ : ℕ
h✝ : start ≤ i✝
assm : i✝ < nfa.nodes.size
⊢ i✝ < nfa.nodes.size
Tactic:
exact assm
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
have : j < nfa.nodes.size := by
  cases step with
  | charStep _ _ step => exact lt_of_charStep step
  | εStep _ _ step => exact lt_of_εStep step
Proof state after:
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
exact ih this
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
cases step with
| charStep _ _ step => exact lt_of_charStep step
| εStep _ _ step => exact lt_of_εStep step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
case charStep
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₂✝ : List Char
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_charStep step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.lt_right
Proof state before:
case εStep
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₂✝ : List Char
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_εStep step
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.snoc_char
Proof state before:
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start : ℕ
assm : j < nfa.nodes.size
step : k ∈ nfa[j].charStep c
path : nfa.pathIn start i j cs
⊢ nfa.pathIn (min start k) i k (cs ++ [c])
Tactic:
induction path with
| base h =>
  simp
  exact .step (.charStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
| @step i j k' cs'' cs''' step' rest ih =>
  simp
  have ih := ih assm step
  exact pathIn.step (step'.castStart (Nat.min_le_left _ _)) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.snoc_char
Proof state before:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k ([] ++ [c])
Tactic:
simp
Proof state after:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k [c]
Theorem: Regex.NFA.pathIn.snoc_char
Proof state before:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k [c]
Tactic:
exact .step (.charStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.snoc_char
Proof state before:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : Char
start i j k' : ℕ
cs'' cs''' : List Char
step' : nfa.stepIn start i j cs''
rest : nfa.pathIn start j k' cs'''
ih : ∀ (assm : k' < nfa.nodes.size), k ∈ nfa[k'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
⊢ nfa.pathIn (min start k) i k (cs'' ++ cs''' ++ [c])
Tactic:
simp
Proof state after:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : Char
start i j k' : ℕ
cs'' cs''' : List Char
step' : nfa.stepIn start i j cs''
rest : nfa.pathIn start j k' cs'''
ih : ∀ (assm : k' < nfa.nodes.size), k ∈ nfa[k'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))
Theorem: Regex.NFA.pathIn.snoc_char
Proof state before:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : Char
start i j k' : ℕ
cs'' cs''' : List Char
step' : nfa.stepIn start i j cs''
rest : nfa.pathIn start j k' cs'''
ih : ∀ (assm : k' < nfa.nodes.size), k ∈ nfa[k'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))
Tactic:
have ih := ih assm step
Proof state after:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : Char
start i j k' : ℕ
cs'' cs''' : List Char
step' : nfa.stepIn start i j cs''
rest : nfa.pathIn start j k' cs'''
ih✝ : ∀ (assm : k' < nfa.nodes.size), k ∈ nfa[k'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
ih : nfa.pathIn (min start k) j k (cs''' ++ [c])
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))
Theorem: Regex.NFA.pathIn.snoc_char
Proof state before:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : Char
start i j k' : ℕ
cs'' cs''' : List Char
step' : nfa.stepIn start i j cs''
rest : nfa.pathIn start j k' cs'''
ih✝ : ∀ (assm : k' < nfa.nodes.size), k ∈ nfa[k'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
ih : nfa.pathIn (min start k) j k (cs''' ++ [c])
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))
Tactic:
exact pathIn.step (step'.castStart (Nat.min_le_left _ _)) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.snoc_ε
Proof state before:
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start : ℕ
assm : j < nfa.nodes.size
step : k ∈ nfa[j].εStep
path : nfa.pathIn start i j cs
⊢ nfa.pathIn (min start k) i k cs
Tactic:
induction path with
| base h =>
  exact .step (.εStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
| step step' rest ih =>
  have ih := ih assm step
  exact .step (step'.castStart (Nat.min_le_left _ _)) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.snoc_ε
Proof state before:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].εStep
⊢ nfa.pathIn (min start k) i✝ k []
Tactic:
exact .step (.εStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.snoc_ε
Proof state before:
case step
j k : ℕ
nfa : NFA
i : ℕ
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 : ∀ (assm : k✝ < nfa.nodes.size), k ∈ nfa[k✝].εStep → nfa.pathIn (min start k) j✝ k cs₂✝
assm : k✝ < nfa.nodes.size
step : k ∈ nfa[k✝].εStep
⊢ nfa.pathIn (min start k) i✝ k (cs₁✝ ++ cs₂✝)
Tactic:
have ih := ih assm step
Proof state after:
case step
j k : ℕ
nfa : NFA
i : ℕ
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✝ : ∀ (assm : k✝ < nfa.nodes.size), k ∈ nfa[k✝].εStep → nfa.pathIn (min start k) j✝ k cs₂✝
assm : k✝ < nfa.nodes.size
step : k ∈ nfa[k✝].εStep
ih : nfa.pathIn (min start k) j✝ k cs₂✝
⊢ nfa.pathIn (min start k) i✝ k (cs₁✝ ++ cs₂✝)
Theorem: Regex.NFA.pathIn.snoc_ε
Proof state before:
case step
j k : ℕ
nfa : NFA
i : ℕ
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✝ : ∀ (assm : k✝ < nfa.nodes.size), k ∈ nfa[k✝].εStep → nfa.pathIn (min start k) j✝ k cs₂✝
assm : k✝ < nfa.nodes.size
step : k ∈ nfa[k✝].εStep
ih : nfa.pathIn (min start k) j✝ k cs₂✝
⊢ nfa.pathIn (min start k) i✝ k (cs₁✝ ++ cs₂✝)
Tactic:
exact .step (step'.castStart (Nat.min_le_left _ _)) ih
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.trans
Proof state before:
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start : ℕ
path₁ : nfa.pathIn start i j cs
path₂ : nfa.pathIn start j k cs'
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
induction path₁ with
| base _ => exact path₂
| step step _ ih =>
  simp
  exact .step step (ih path₂)
Proof state after:
no goals
Theorem: Regex.NFA.pathIn.trans
Proof state before:
case base
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ : ℕ
h✝ : start ≤ i✝
path₂ : nfa.pathIn start i✝ k cs'
⊢ nfa.pathIn start i✝ k ([] ++ cs')
Tactic:
exact path₂
Proof state after:
no goals