internlm/Lean-Github huggingface dataset:
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
⊢ nfa'[i] = Node.done ↔ i = 0
Tactic:
have : nfa'[i] = nfa[i] := by
  have : i < placeholder.val.nodes.size :=
    Nat.lt_trans lt placeholder.property
  have : i < compiled.val.nodes.size :=
    Nat.lt_trans this compiled.property
  calc nfa'[i]
    _ = compiled.val[i] := by
      simp [eq₄, NFA.get_eq_nodes_get, eq₃]
      rw [Array.get_set_ne]
      simp
      exact Nat.ne_of_gt lt
    _ = placeholder.val[i] := by apply pushRegex_get_lt eq₂.symm
    _ = nfa[i] := by
      simp [eq₁]
      apply pushNode_get_lt
Proof state after:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this : nfa'[i] = nfa[i]
⊢ nfa'[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this : nfa'[i] = nfa[i]
⊢ nfa'[i] = Node.done ↔ i = 0
Tactic:
rw [this]
Proof state after:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this : nfa'[i] = nfa[i]
⊢ nfa[i] = Node.done ↔ i = 0
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this : nfa'[i] = nfa[i]
⊢ nfa[i] = Node.done ↔ i = 0
Tactic:
exact h₂ i lt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
⊢ nfa'[i] = nfa[i]
Tactic:
have : i < placeholder.val.nodes.size :=
  Nat.lt_trans lt placeholder.property
Proof state after:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this : i < (↑placeholder).nodes.size
⊢ nfa'[i] = nfa[i]
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this : i < (↑placeholder).nodes.size
⊢ nfa'[i] = nfa[i]
Tactic:
have : i < compiled.val.nodes.size :=
  Nat.lt_trans this compiled.property
Proof state after:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ nfa'[i] = nfa[i]
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ nfa'[i] = nfa[i]
Tactic:
calc nfa'[i]
  _ = compiled.val[i] := by
    simp [eq₄, NFA.get_eq_nodes_get, eq₃]
    rw [Array.get_set_ne]
    simp
    exact Nat.ne_of_gt lt
  _ = placeholder.val[i] := by apply pushRegex_get_lt eq₂.symm
  _ = nfa[i] := by
    simp [eq₁]
    apply pushNode_get_lt
Proof state after:
no goals
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ nfa'[i] = (↑compiled)[i]
Tactic:
simp [eq₄, NFA.get_eq_nodes_get, eq₃]
Proof state after:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i] = (↑compiled).nodes[i]
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i] = (↑compiled).nodes[i]
Tactic:
rw [Array.get_set_ne]
Proof state after:
case h
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case h
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Tactic:
simp
Proof state after:
case h
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Theorem: Regex.NFA.done_iff_zero_pushRegex
Proof state before:
case h
r : Data.Expr
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      0 < nfa.nodes.size →
        (∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0) →
          ∀ (i : ℕ) (isLt : i < (↑result).nodes.size), (↑result)[i] = Node.done ↔ i = 0
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
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 : nfa.pushRegex next r.star = ⟨nfa', property⟩
i : ℕ
isLt : i < nfa'.nodes.size
lt : i < nfa.nodes.size
this✝ : i < (↑placeholder).nodes.size
this : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Tactic:
exact Nat.ne_of_gt lt
Proof state after:
no goals