internlm/Lean-Github huggingface dataset:
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.pushRegex next Data.Expr.epsilon))[↑(↑(nfa.pushRegex next Data.Expr.epsilon)).start].εStep
Tactic:
simp [pushRegex, Node.εStep]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case group
r : Data.Expr
cs s✝ : List Char
r✝ : Data.Expr
i✝ : ℕ
m✝ : Data.Expr.matches s✝ r✝
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) s✝
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group i✝ r✝) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) s✝
Tactic:
exact pathToNext_of_matches.group eq ih
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case alternateLeft
r : Data.Expr
cs cs✝ : List Char
r₁✝ r₂✝ : Data.Expr
a✝ : Data.Expr.matches cs✝ r₁✝
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
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁✝.alternate r₂✝) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs✝
Tactic:
exact pathToNext_of_matches.alternateLeft eq ih
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case alternateRight
r : Data.Expr
cs cs✝ : List Char
r₁✝ r₂✝ : Data.Expr
a✝ : Data.Expr.matches cs✝ r₂✝
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
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁✝.alternate r₂✝) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs✝
Tactic:
exact pathToNext_of_matches.alternateRight eq ih
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case concat
r : Data.Expr
cs cs₁ cs₂ : List Char
r₁ r₂ : Data.Expr
a✝¹ : Data.Expr.matches cs₁ r₁
a✝ : Data.Expr.matches cs₂ r₂
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
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
exact pathToNext_of_matches.concat eq ih₁ ih₂
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case starEpsilon
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = 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 starEpsilon
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = 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 starEpsilon
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = 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 starEpsilon
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case starEpsilon
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
apply pushRegex.star eq
Proof state after:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ∀ (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⟩ → ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r✝.star = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ∀ (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⟩ → ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
intro placeholder compiled patched nfa' isLt inBounds property
  _ _ eq₃ eq₄ eq
Proof state after:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
⊢ ↑next ∈ (↑nfa'✝)[↑(↑nfa'✝).start].εStep
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
⊢ ↑next ∈ (↑nfa'✝)[↑(↑nfa'✝).start].εStep
Tactic:
rw[eq]
Proof state after:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
⊢ ↑next ∈ (↑⟨nfa', property⟩)[↑(↑⟨nfa', property⟩).start].εStep
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
⊢ ↑next ∈ (↑⟨nfa', property⟩)[↑(↑⟨nfa', property⟩).start].εStep
Tactic:
have : nfa'.start.val = nfa.nodes.size := by
  rw [eq₄]
Proof state after:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this✝ : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
this : ↑nfa'.start = nfa.nodes.size
⊢ ↑next ∈ (↑⟨nfa', property⟩)[↑(↑⟨nfa', property⟩).start].εStep
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this✝ : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
this : ↑nfa'.start = nfa.nodes.size
⊢ ↑next ∈ (↑⟨nfa', property⟩)[↑(↑⟨nfa', property⟩).start].εStep
Tactic:
simp [this, eq₄, get_eq_nodes_get, eq₃, Node.εStep]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
r : Data.Expr
cs : List Char
r✝ : Data.Expr
nfa : NFA
next : Fin nfa.nodes.size
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r✝.star = nfa'✝
this : nfa.nodes.size ≤ ↑(↑nfa'✝).start
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
a✝¹ : placeholder = nfa.pushNode Node.fail ⋯
a✝ : 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⟩
⊢ ↑nfa'.start = nfa.nodes.size
Tactic:
rw [eq₄]
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_matches
Proof state before:
case starConcat
r✝ : Data.Expr
cs cs₁ cs₂ : List Char
r : Data.Expr
a✝¹ : Data.Expr.matches cs₁ r
a✝ : Data.Expr.matches cs₂ r.star
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 : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = nfa'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
exact pathToNext_of_matches.starConcat eq ih₁ ih₂
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
unfold NFA.compile at eq
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Theorem: Regex.NFA.pathToNext_of_compile_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r with h
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Theorem: Regex.NFA.pathToNext_of_compile_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
have := pathToNext_of_matches h.symm m
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result).pathToNext (↑⟨0, ⋯⟩) done.nodes.size (↑(↑result).start) cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Theorem: Regex.NFA.pathToNext_of_compile_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result).pathToNext (↑⟨0, ⋯⟩) done.nodes.size (↑(↑result).start) cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
rw [eq] at this
Proof state after:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
this : nfa.pathToNext (↑⟨0, ⋯⟩) done.nodes.size (↑nfa.start) cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Theorem: Regex.NFA.pathToNext_of_compile_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
m : Data.Expr.matches cs r
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
h : result = done.pushRegex ⟨0, ⋯⟩ r
this : nfa.pathToNext (↑⟨0, ⋯⟩) done.nodes.size (↑nfa.start) cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
exact this
Proof state after:
no goals
Theorem: Regex.NFA.pathToNext_of_compile_matches
Proof state before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
m : Data.Expr.matches cs r
⊢ 0 < done.nodes.size
Tactic:
decide
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.mem_dense_of_lt
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ↑i < s.count
⊢ s.dense[i] ∈ s
Tactic:
simp [mem, sparse_dense, h]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.dense_inj
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
⊢ i = j
Tactic:
have : s.sparse[s.dense[i]] = s.sparse[s.dense[j]] := by rw [eq]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : s.sparse[s.dense[i]] = s.sparse[s.dense[j]]
⊢ i = j
Theorem: Regex.Data.SparseSet.dense_inj
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : s.sparse[s.dense[i]] = s.sparse[s.dense[j]]
⊢ i = j
Tactic:
simp [s.sparse_dense i hi, s.sparse_dense j hj] at this
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : i = j
⊢ i = j
Theorem: Regex.Data.SparseSet.dense_inj
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : i = j
⊢ i = j
Tactic:
exact this
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.dense_inj
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
⊢ s.sparse[s.dense[i]] = s.sparse[s.dense[j]]
Tactic:
rw [eq]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.dense_surj
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : j ∈ s
⊢ ∃ i, ↑i < s.count ∧ s.dense[i] = j
Tactic:
simp [mem] at h
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : ↑s.sparse[↑j] < s.count ∧ s.dense[↑s.sparse[↑j]] = j
⊢ ∃ i, ↑i < s.count ∧ s.dense[i] = j
Theorem: Regex.Data.SparseSet.dense_surj
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : ↑s.sparse[↑j] < s.count ∧ s.dense[↑s.sparse[↑j]] = j
⊢ ∃ i, ↑i < s.count ∧ s.dense[i] = j
Tactic:
exists s.sparse[j]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
⊢ s.dense[s.sparse[j]] = j
Tactic:
let f (i : Fin n) : Fin n := s.dense[i]
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ s.dense[s.sparse[j]] = j
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ s.dense[s.sparse[j]] = j
Tactic:
have inj : inj f := by
  intro x y eq
  exact dense_inj (Nat.lt_of_lt_of_le x.isLt h) (Nat.lt_of_lt_of_le y.isLt h) eq
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
⊢ s.dense[s.sparse[j]] = j
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
⊢ s.dense[s.sparse[j]] = j
Tactic:
have surj : surj f := surj_of_inj _ inj
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
⊢ s.dense[s.sparse[j]] = j
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
⊢ s.dense[s.sparse[j]] = j
Tactic:
have ⟨i, eq⟩ := surj j
Proof state after:
n : Nat
s : SparseSet n
i✝ j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
i : Fin n
eq : f i = j
⊢ s.dense[s.sparse[j]] = j
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i✝ j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
i : Fin n
eq : f i = j
⊢ s.dense[s.sparse[j]] = j
Tactic:
simp [f, ←eq, s.sparse_dense i (Nat.lt_of_lt_of_le i.isLt h)]
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ inj f
Tactic:
intro x y eq
Proof state after:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
x y : Fin n
eq : f x = f y
⊢ x = y
Theorem: Regex.Data.SparseSet.dense_sparse_of_full
Proof state before:
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
x y : Fin n
eq : f x = f y
⊢ x = y
Tactic:
exact dense_inj (Nat.lt_of_lt_of_le x.isLt h) (Nat.lt_of_lt_of_le y.isLt h) eq
Proof state after:
no goals
Theorem: Regex.Data.SparseSet.lt_of_mem
Proof state before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ¬i ∈ s
⊢ s.count < n
Tactic:
simp [SparseSet.mem] at h
Proof state after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
⊢ s.count < n
Theorem: Regex.Data.SparseSet.lt_of_mem
Proof state before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
⊢ s.count < n
Tactic:
by_contra nlt
Proof state after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
⊢ False
Theorem: Regex.Data.SparseSet.lt_of_mem
Proof state before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
⊢ False
Tactic:
have ge := Nat.le_of_not_lt nlt
Proof state after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ False
Theorem: Regex.Data.SparseSet.lt_of_mem
Proof state before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ False
Tactic:
apply h (Nat.lt_of_lt_of_le s.sparse[i].isLt ge)
Proof state after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ s.dense[↑s.sparse[↑i]] = i