Theorem: final_state_accepts_iff (FormalSystems/Chomsky/Regular/Nerode.lean)

State before:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ let M := canonicalAutomaton nc;
  ∀ (w : Word { x // x ∈ M.Z }), TotalDFA.del_star' M (M.q₀, w) ∈ M.F ↔ w ∈ L
Tactic:
intro M w
State after:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ TotalDFA.del_star' M (M.q₀, w) ∈ M.F ↔ w ∈ L

State before:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ TotalDFA.del_star' M (M.q₀, w) ∈ M.F ↔ w ∈ L
Tactic:
rw [initial_state_eq, final_state_eq]
State after:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ { val := ⟦w⟧, property := ⋯ } ∈ M.F ↔ w ∈ L

State before:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ { val := ⟦w⟧, property := ⋯ } ∈ M.F ↔ w ∈ L
Tactic:
simp [M, canonicalAutomaton]
State after:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ ⟦w⟧ ∈ Fintype.elems ∧ FinalClass L ⟦w⟧ ↔ w ∈ L

State before:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ ⟦w⟧ ∈ Fintype.elems ∧ FinalClass L ⟦w⟧ ↔ w ∈ L
Tactic:
simp [Fintype.complete]
State after:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ FinalClass L ⟦w⟧ ↔ w ∈ L

State before:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ FinalClass L ⟦w⟧ ↔ w ∈ L
Tactic:
unfold FinalClass
State after:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ Quotient.lift (fun x => x ∈ L) ⋯ ⟦w⟧ ↔ w ∈ L

State before:
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ Quotient.lift (fun x => x ∈ L) ⋯ ⟦w⟧ ↔ w ∈ L
Tactic:
rw [@Quotient.lift_mk _ _ (myhillNerodeEquivalence L) _ _ _]
State after:
no goals