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

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
have h (i : Nat) (isLt : i < NFA.done.nodes.size) : done[i] = Node.done ↔ i = 0 := by
  simp [NFA.done] at *
  suffices i = 0 by
    subst this
    simp
    rfl
  simp [NFA.done] at isLt
  match i with
  | 0 => rfl
  | i + 1 => contradiction
State after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
unfold compile at eq
State after:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0

State before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
set result := NFA.done.pushRegex ⟨0, by decide⟩ r with eq'
State after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa[i] = Node.done ↔ ↑i = 0

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
have := done_iff_zero_pushRegex eq'.symm (by decide) h i (eq ▸ i.isLt)
State after:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result)[↑i] = Node.done ↔ ↑i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
this : (↑result)[↑i] = Node.done ↔ ↑i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0
Tactic:
exact eq ▸ this
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ done[i] = Node.done ↔ i = 0
Tactic:
simp [NFA.done] at *
State after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[i] = Node.done ↔ i = 0

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[i] = Node.done ↔ i = 0
Tactic:
suffices i = 0 by
  subst this
  simp
  rfl
State after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ i = 0

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ i = 0
Tactic:
simp [NFA.done] at isLt
State after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i = 0
⊢ i = 0

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i = 0
⊢ i = 0
Tactic:
match i with
| 0 => rfl
| i + 1 => contradiction
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
this : i = 0
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[i] = Node.done ↔ i = 0
Tactic:
subst this
State after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done ↔ 0 = 0

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done ↔ 0 = 0
Tactic:
simp
State after:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
isLt : 0 < done.nodes.size
⊢ { nodes := #[Node.done], start := 0, inBounds := done.proof_3 }[0] = Node.done
Tactic:
rfl
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : 0 = 0
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝¹ : Fin nfa.nodes.size
i✝ i : ℕ
isLt : i + 1 = 0
⊢ i + 1 = 0
Tactic:
contradiction
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
result : { nfa' // done.nodes.size < nfa'.nodes.size } := done.pushRegex ⟨0, ⋯⟩ r
eq : ↑result = nfa
eq' : result = done.pushRegex ⟨0, ⋯⟩ r
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals