internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
rw [eq]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
⊢ (↑⟨↑nfa₁, property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa₁, property⟩).start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
⊢ (↑⟨↑nfa₁, property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa₁, property⟩).start) (cs₁ ++ cs₂)
Tactic:
simp
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Tactic:
have ih₁ : pathToNext nfa₁ nfa₂.val.start nfa.nodes.size nfa₁.val.start cs₁ :=
  (ih₁ eq₁.symm).castStart (Nat.le_of_lt nfa₂.property)
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Tactic:
have ih₂ : pathToNext nfa₂ next nfa.nodes.size nfa₂.val.start cs₂ := ih₂ eq₂.symm
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Tactic:
have ih₂ : pathToNext nfa₁ next nfa.nodes.size nfa₂.val.start cs₂ := by
  apply ih₂.cast
  intro i _ h₂
  exists Nat.lt_trans h₂ nfa₁.property
  rw [pushRegex_get_lt eq₁.symm _ h₂]
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂✝ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
ih₂ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂✝ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
ih₂ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) (cs₁ ++ cs₂)
Tactic:
exact ih₁.trans ih₂
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
Tactic:
apply ih₂.cast
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ ∀ (i : ℕ),
    nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), ∃ (h' : i < (↑nfa₁).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
⊢ ∀ (i : ℕ),
    nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), ∃ (h' : i < (↑nfa₁).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
Tactic:
intro i _ h₂
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ ∃ (h' : i < (↑nfa₁).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ ∃ (h' : i < (↑nfa₁).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
Tactic:
exists Nat.lt_trans h₂ nfa₁.property
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ (↑nfa₂)[i] = (↑nfa₁)[i]
Theorem: Regex.NFA.pathToNext_of_matches.concat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next (r₁.concat r₂) = nfa'
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : nfa' = ⟨↑nfa₁, property⟩
ih₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) nfa.nodes.size (↑(↑nfa₁).start) cs₁
ih₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs₂
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ (↑nfa₂)[i] = (↑nfa₁)[i]
Tactic:
rw [pushRegex_get_lt eq₁.symm _ h₂]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches.starConcat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
have ih₂ : pathToNext nfa' next nfa.nodes.size nfa'.val.start cs₂ := ih₂ eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Theorem: Regex.NFA.pathToNext_of_matches.starConcat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
apply pushRegex.star eq
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = nfa'
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa'_1 : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'_1.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'_1 = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            nfa' = ⟨nfa'_1, property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)