internlm/Lean-Github huggingface dataset:
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
Tactic:
apply ih₁.cast
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ ∀ (i : ℕ),
    (↑placeholder).nodes.size ≤ i →
      ∀ (h₂ : i < (↑compiled).nodes.size), ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ ∀ (i : ℕ),
    (↑placeholder).nodes.size ≤ i →
      ∀ (h₂ : i < (↑compiled).nodes.size), ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]
Tactic:
intro i h₁ h₂
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]
Theorem: Regex.NFA.pathToNext_of_matches.starConcat
Proof state before:
case h
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Tactic:
simp
Proof state after:
case h
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Theorem: Regex.NFA.pathToNext_of_matches.starConcat
Proof state before:
case h
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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Tactic:
apply Nat.ne_of_lt (Nat.lt_of_lt_of_le placeholder.property 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₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
Tactic:
exact ih₂
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₂
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
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ nfa.nodes.size ≤ ↑nfa'.start
Tactic:
simp [eqStart]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next r = nfa'
m : Data.Expr.matches cs r
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
induction m generalizing nfa next with
| sparse cls c hmem =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨
    nfa'.val.start,
    [],
    [c],
    rfl,
    .base this,
    .charStep this nfa'.val.start.isLt ?_
  ⟩
  rw [←eq]
  simp [pushRegex, Node.charStep, hmem]
| char c =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨
    nfa'.val.start,
    [],
    [c],
    rfl,
    .base this,
    .charStep this nfa'.val.start.isLt ?_
  ⟩
  rw [←eq]
  simp [pushRegex, Node.charStep]
| epsilon =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨nfa'.val.start, [], [], rfl, .base this, .εStep this nfa'.val.start.isLt ?_⟩
  rw [←eq]
  simp [pushRegex, Node.εStep]
| group _ ih => exact pathToNext_of_matches.group eq ih
| alternateLeft _ ih => exact pathToNext_of_matches.alternateLeft eq ih
| alternateRight _ ih => exact pathToNext_of_matches.alternateRight eq ih
| concat cs₁ cs₂ r₁ r₂ _ _ ih₁ ih₂ => exact pathToNext_of_matches.concat eq ih₁ ih₂
| starEpsilon =>
  have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
  refine ⟨nfa'.val.start, [], [], rfl, .base this, .εStep this nfa'.val.start.isLt ?_⟩
  apply pushRegex.star eq
  intro placeholder compiled patched nfa' isLt inBounds property
    _ _ eq₃ eq₄ eq
  rw[eq]
  have : nfa'.start.val = nfa.nodes.size := by
    rw [eq₄]
  simp [this, eq₄, get_eq_nodes_get, eq₃, Node.εStep]
| starConcat cs₁ cs₂ r _ _ ih₁ ih₂ => exact pathToNext_of_matches.starConcat eq ih₁ ih₂
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
Tactic:
have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
Proof state after:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
Tactic:
refine ⟨
  nfa'.val.start,
  [],
  [c],
  rfl,
  .base this,
  .charStep this nfa'.val.start.isLt ?_
⟩
Proof state after:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].charStep c
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].charStep c
Tactic:
rw [←eq]
Proof state after:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈
    (↑(nfa.pushRegex next (Data.Expr.classes cls)))[↑(↑(nfa.pushRegex next (Data.Expr.classes cls))).start].charStep c
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈
    (↑(nfa.pushRegex next (Data.Expr.classes cls)))[↑(↑(nfa.pushRegex next (Data.Expr.classes cls))).start].charStep c
Tactic:
simp [pushRegex, Node.charStep, hmem]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
Tactic:
have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
Proof state after:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
Tactic:
refine ⟨
  nfa'.val.start,
  [],
  [c],
  rfl,
  .base this,
  .charStep this nfa'.val.start.isLt ?_
⟩
Proof state after:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].charStep c
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].charStep c
Tactic:
rw [←eq]
Proof state after:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑(nfa.pushRegex next (Data.Expr.char c)))[↑(↑(nfa.pushRegex next (Data.Expr.char c))).start].charStep c
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case char
r : Data.Expr
cs : List Char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑(nfa.pushRegex next (Data.Expr.char c)))[↑(↑(nfa.pushRegex next (Data.Expr.char c))).start].charStep c
Tactic:
simp [pushRegex, Node.charStep]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case epsilon
r : Data.Expr
cs : List Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
Tactic:
have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
Proof state after:
case epsilon
r : Data.Expr
cs : List Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case epsilon
r : Data.Expr
cs : List Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
Tactic:
refine ⟨nfa'.val.start, [], [], rfl, .base this, .εStep this nfa'.val.start.isLt ?_⟩
Proof state after:
case epsilon
r : Data.Expr
cs : List Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case epsilon
r : Data.Expr
cs : List Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
rw [←eq]
Proof state after:
case epsilon
r : Data.Expr
cs : List Char
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑(nfa.pushRegex next Data.Expr.epsilon))[↑(↑(nfa.pushRegex next Data.Expr.epsilon)).start].εStep