internlm/Lean-Github huggingface dataset:
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl = u * w
vw_in_l : v * w ∈ L
vw_eq_uw : v * w = u * w
⊢ False
Tactic:
exact pre <| Eq.symm <| Word.mul_right_cancel vw_eq_uw
Proof state after:
no goals
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
⊢ False
Tactic:
have uw_in_l := h2.mpr $ e ▸ singl_inter.right
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
⊢ False
Tactic:
have uw_eq_vw := e ▸ h (u*w) ⟨ Or.inl rfl, uw_in_l ⟩
Proof state after:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
uw_eq_vw : u * w = v * w
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if
Proof state before:
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
e : singl ∈ {v * w}
uw_in_l : u * w ∈ L
uw_eq_vw : u * w = v * w
⊢ False
Tactic:
exact pre <| Word.mul_right_cancel uw_eq_vw
Proof state after:
no goals
Theorem: MyhillNerodeRelation.not_congruent_if'
Proof state before:
α : Type u_1
L : Language α
u v : Word α
⊢ (∃ w, u * w ∈ L ∧ v * w ∉ L) → ¬u ≃( L ) v
Tactic:
intro ⟨ w, uw_in_l, vw_nin_l ⟩ contra
Proof state after:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ False
Theorem: MyhillNerodeRelation.not_congruent_if'
Proof state before:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ False
Tactic:
apply vw_nin_l
Proof state after:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ v * w ∈ L
Theorem: MyhillNerodeRelation.not_congruent_if'
Proof state before:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ v * w ∈ L
Tactic:
apply (contra w).mp
Proof state after:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ u * w ∈ L
Theorem: MyhillNerodeRelation.not_congruent_if'
Proof state before:
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ u * w ∈ L
Tactic:
exact uw_in_l
Proof state after:
no goals
Theorem: MyhillNerodeRelation.mem_language
Proof state before:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
⊢ u ∈ L ↔ v ∈ L
Tactic:
have := h ε
Proof state after:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u * ε ∈ L ↔ v * ε ∈ L
⊢ u ∈ L ↔ v ∈ L
Theorem: MyhillNerodeRelation.mem_language
Proof state before:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u * ε ∈ L ↔ v * ε ∈ L
⊢ u ∈ L ↔ v ∈ L
Tactic:
simp at this
Proof state after:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u ∈ L ↔ v ∈ L
⊢ u ∈ L ↔ v ∈ L
Theorem: MyhillNerodeRelation.mem_language
Proof state before:
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u ∈ L ↔ v ∈ L
⊢ u ∈ L ↔ v ∈ L
Tactic:
assumption
Proof state after:
no goals
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v✝ : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w v : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, v)) = ↑{ val := ⟦w * v⟧, property := ⋯ }
Tactic:
induction v generalizing w
Proof state after:
case nil
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, [])) =
    ↑{ val := ⟦w * []⟧, property := ⋯ }

case cons
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
tail_ih✝ :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) =
    ↑{ val := ⟦w * (head✝ :: tail✝)⟧, property := ⋯ }
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, [])) =
    ↑{ val := ⟦w * []⟧, property := ⋯ }
Tactic:
case nil => simp [<-Word.eps_eq_nil, Word.monoid.mul_one]; rfl
Proof state after:
no goals
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) =
    ↑{ val := ⟦w * (head✝ :: tail✝)⟧, property := ⋯ }
Tactic:
case cons _ _ ih =>
  simp [HMul.hMul, Mul.mul]
  simp [TotalDFA.del_star']
  rw [List.append_cons]
  apply ih
Proof state after:
no goals
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, [])) =
    ↑{ val := ⟦w * []⟧, property := ⋯ }
Tactic:
simp [<-Word.eps_eq_nil, Word.monoid.mul_one]
Proof state after:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, ε)) = ⟦w⟧
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, ε)) = ⟦w⟧
Tactic:
rfl
Proof state after:
no goals
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) =
    ↑{ val := ⟦w * (head✝ :: tail✝)⟧, property := ⋯ }
Tactic:
simp [HMul.hMul, Mul.mul]
Proof state after:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) = ⟦w ++ head✝ :: tail✝⟧
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝ :: tail✝)) = ⟦w ++ head✝ :: tail✝⟧
Tactic:
simp [TotalDFA.del_star']
Proof state after:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ head✝ :: tail✝⟧
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ head✝ :: tail✝⟧
Tactic:
rw [List.append_cons]
Proof state after:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ [head✝] ++ tail✝⟧
Theorem: del_star_eq
Proof state before:
α✝ : Type ?u.20791
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
head✝ : { x // x ∈ (canonicalAutomaton nc).Z }
tail✝ : List { x // x ∈ (canonicalAutomaton nc).Z }
ih :
  ∀ (w : Word { x // x ∈ (canonicalAutomaton nc).Z }),
    ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, tail✝)) =
      ↑{ val := ⟦w * tail✝⟧, property := ⋯ }
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc)
        (TotalDFA.δ' (canonicalAutomaton nc) ({ val := ⟦w⟧, property := ⋯ }, head✝), tail✝)) =
    ⟦w ++ [head✝] ++ tail✝⟧
Tactic:
apply ih
Proof state after:
no goals
Theorem: final_state_eq
Proof state before:
α✝ : Type ?u.29550
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦ε⟧, property := ⋯ }, w)) = ↑{ val := ⟦w⟧, property := ⋯ }
Tactic:
simp [del_star_eq]
Proof state after:
no goals
Theorem: final_state_accepts_iff
Proof 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
Proof 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
Theorem: final_state_accepts_iff
Proof 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]
Proof 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
Theorem: final_state_accepts_iff
Proof 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]
Proof 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
Theorem: final_state_accepts_iff
Proof 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]
Proof 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
Theorem: final_state_accepts_iff
Proof 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
Proof 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
Theorem: final_state_accepts_iff
Proof 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) _ _ _]
Proof state after:
no goals
Theorem: canonicalAutomaton_accepted_language
Proof state before:
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA = L
Tactic:
apply Set.ext
Proof state after:
case h
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ ∀ (x : Word { x // x ∈ (canonicalAutomaton nc).Z }), x ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ x ∈ L
Theorem: canonicalAutomaton_accepted_language
Proof state before:
case h
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ ∀ (x : Word { x // x ∈ (canonicalAutomaton nc).Z }), x ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ x ∈ L
Tactic:
intro w
Proof state after:
case h
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ w ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ w ∈ L
Theorem: canonicalAutomaton_accepted_language
Proof state before:
case h
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ w ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ w ∈ L
Tactic:
rw [TotalDFA.in_language_iff_del_star_final, final_state_accepts_iff]
Proof state after:
no goals
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ ↔ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Tactic:
constructor
Proof state after:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs

case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs

case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Tactic:
. intro h; rw [h]; exact ⟨ rfl, rfl ⟩
Proof state after:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Tactic:
. intro ⟨ h₁, h₂ ⟩
  match p₁ with
  | ⟨ l, r, _ ⟩ => simp at h₁; simp at h₂; simp_rw [h₁, h₂]
Proof state after:
no goals
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Tactic:
intro h
Proof state after:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Tactic:
rw [h]
Proof state after:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₂.lhs = p₂.lhs ∧ p₂.rhs = p₂.rhs
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₂.lhs = p₂.lhs ∧ p₂.rhs = p₂.rhs
Tactic:
exact ⟨ rfl, rfl ⟩
Proof state after:
no goals
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Tactic:
intro ⟨ h₁, h₂ ⟩
Proof state after:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h₁ : p₁.lhs = p₂.lhs
h₂ : p₁.rhs = p₂.rhs
⊢ p₁ = p₂
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h₁ : p₁.lhs = p₂.lhs
h₂ : p₁.rhs = p₂.rhs
⊢ p₁ = p₂
Tactic:
match p₁ with
| ⟨ l, r, _ ⟩ => simp at h₁; simp at h₂; simp_rw [h₁, h₂]
Proof state after:
no goals
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.lhs = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Tactic:
simp at h₁
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq
Proof state before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Tactic:
simp at h₂
Proof state after:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : r = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂