Theorem: Regex.NFA.lt_zero_size_compile (RegexCorrectness/NFA/Compile.lean)

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
⊢ 0 < nfa.nodes.size
Tactic:
unfold compile at eq
State after:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
⊢ 0 < nfa.nodes.size

State before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
⊢ 0 < nfa.nodes.size
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r
State after:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
⊢ 0 < nfa.nodes.size

State before:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
⊢ 0 < nfa.nodes.size
Tactic:
have : 0 < result.val.nodes.size := Nat.zero_lt_of_lt result.property
State after:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
this : 0 < (↑result).nodes.size
⊢ 0 < nfa.nodes.size

State before:
r : Data.Expr
nfa : NFA
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
this : 0 < (↑result).nodes.size
⊢ 0 < nfa.nodes.size
Tactic:
exact eq ▸ this
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals