internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ → i = nfa.nodes.size ∧ cs = []
Tactic:
intro placeholder compiled patched nfa' isLt inBounds property
  eq₁ eq₂ eq₃ eq₄ eq'
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
⊢ i = nfa.nodes.size ∧ cs = []
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
⊢ i = nfa.nodes.size ∧ cs = []
Tactic:
cases Nat.lt_or_ge i (nfa.nodes.size + 1) with
| inl lt =>
  have eqi := Nat.eq_of_le_of_lt_succ step.h₁ lt
  obtain ⟨_, node⟩ := rStart_of_spec eq
  cases step with
  | charStep _ _ step => simp [eqi, node, NFA.Node.charStep] at step
  | εStep _ _ step => simp [eqi]
| inr ge =>
  exfalso
  have eqs : placeholder.val.nodes.size = nfa.nodes.size + 1 := by
    simp [eq₁]
  have h₂ : i < compiled.val.nodes.size := by
    have := step.h₂
    simp [eq', eq₄, eq₃] at this
    exact this
  have eqn : result.val[i]'step.h₂ = compiled.val[i] := by
    simp [eq', get_eq_nodes_get, eq₄]
    simp [eq₃]
    rw [Array.get_set_ne]
    simp
    exact Nat.ne_of_lt ge
  have := eq_or_ge_of_step_pushRegex eq₂.symm (eqs ▸ ge) h₂ (eqn ▸ step.step)
  simp [eqs] at this
  cases this with
  | inl eq => exact Nat.lt_irrefl _ (eq ▸ next.isLt)
  | inr gt => exact Nat.lt_irrefl _ (Nat.lt_trans gt next.isLt)
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
⊢ i = nfa.nodes.size ∧ cs = []
Tactic:
have eqi := Nat.eq_of_le_of_lt_succ step.h₁ lt
Proof state after:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
⊢ i = nfa.nodes.size ∧ cs = []
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
⊢ i = nfa.nodes.size ∧ cs = []
Tactic:
obtain ⟨_, node⟩ := rStart_of_spec eq
Proof state after:
case inl.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
⊢ i = nfa.nodes.size ∧ cs = []
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inl.intro
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
⊢ i = nfa.nodes.size ∧ cs = []
Tactic:
cases step with
| charStep _ _ step => simp [eqi, node, NFA.Node.charStep] at step
| εStep _ _ step => simp [eqi]
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inl.intro.charStep
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
eq : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
c✝ : Char
h₁✝ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : ↑next ∈ (↑result)[i].charStep c✝
⊢ i = nfa.nodes.size ∧ [c✝] = []
Tactic:
simp [eqi, node, NFA.Node.charStep] at step
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inl.intro.εStep
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
eq : nfa.pushRegex next r.star = result
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
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' : result = ⟨nfa', property⟩
lt : i < nfa.nodes.size + 1
eqi : i = nfa.nodes.size
left✝ : nfa.nodes.size + 1 ≤ rStart_of eq
node : (↑result)[nfa.nodes.size] = Node.split (rStart_of eq) ↑next
h₁✝ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
step : ↑next ∈ (↑result)[i].εStep
⊢ i = nfa.nodes.size ∧ [] = []
Tactic:
simp [eqi]
Proof state after:
no goals
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
⊢ i = nfa.nodes.size ∧ cs = []
Tactic:
exfalso
Proof state after:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
⊢ False
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
⊢ False
Tactic:
have eqs : placeholder.val.nodes.size = nfa.nodes.size + 1 := by
  simp [eq₁]
Proof state after:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
⊢ False
Theorem: Regex.NFA.matches_of_path.star
Proof state before:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
⊢ False
Tactic:
have h₂ : i < compiled.val.nodes.size := by
  have := step.h₂
  simp [eq', eq₄, eq₃] at this
  exact this
Proof state after:
case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs✝ : List Char
eq✝ : nfa.pushRegex next r.star = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
i : ℕ
cs : List Char
eq : nfa.pushRegex next r.star = result
step : (↑result).stepIn nfa.nodes.size i (↑next) 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
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' : result = ⟨nfa', property⟩
ge : i ≥ nfa.nodes.size + 1
eqs : (↑placeholder).nodes.size = nfa.nodes.size + 1
h₂ : i < (↑compiled).nodes.size
⊢ False