internlm/Lean-Github huggingface dataset:
Theorem: DFA.toGrammar_prod_imp_transition
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'
Tactic:
have ⟨_, _, _, _, _, _, _, _, c1, c2, c3⟩ := h
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'
Theorem: DFA.toGrammar_prod_imp_transition
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ (v, a) = some v'
Tactic:
rw [<- c1, <- c2, <- c3]
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
Theorem: DFA.toGrammar_prod_imp_transition
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
v : { x // x ∈ (toGrammar M).V }
a : { x // x ∈ (toGrammar M).Z }
v' : { x // x ∈ (toGrammar M).V }
h :
  ∃ a_1,
    ∃ (b : a_1 ∈ M.Q),
      ∃ a_2,
        ∃ (b_1 : a_2 ∈ M.Z),
          ({ val := a_1, property := b }, { val := a_2, property := b_1 }) ∈ Fintype.elems ∧
            ∃ a_3,
              ∃ (h : a_3 ∈ M.Q),
                M.δ ({ val := a_1, property := b }, { val := a_2, property := b_1 }) =
                    some { val := a_3, property := ⋯ } ∧
                  { val := a_1, property := b } = v ∧
                    { val := a_2, property := b_1 } = a ∧ { val := a_3, property := ⋯ } = v'
w✝⁵ : qs
w✝⁴ : w✝⁵ ∈ M.Q
w✝³ : α
w✝² : w✝³ ∈ M.Z
left✝¹ : ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) ∈ Fintype.elems
w✝¹ : qs
w✝ : w✝¹ ∈ M.Q
left✝ : M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
c1 : { val := w✝⁵, property := w✝⁴ } = v
c2 : { val := w✝³, property := w✝² } = a
c3 : { val := w✝¹, property := ⋯ } = v'
⊢ M.δ ({ val := w✝⁵, property := w✝⁴ }, { val := w✝³, property := w✝² }) = some { val := w✝¹, property := ⋯ }
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
d : RegularGrammar.RegularDerivation (toGrammar M) s w
⊢ NFA.Run.last (fromDerivation M d) ∈ M.F
Tactic:
cases d
Proof state after:
case eps
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w✝ : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w✝)) ∈ M.F

case alpha
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v✝ h_w✝)) ∈ M.F

case step
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w✝ : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w✝ a✝)) ∈ M.F
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v h_w)) ∈ M.F
Tactic:
case eps h_v h_w =>
  simp [toGrammar, transitionToRule] at h_v
  simp [fromDerivation, NFA.Run.last]
  assumption
Proof state after:
no goals
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v h_w✝)) ∈ M.F
Tactic:
case alpha h_v _ =>
  simp [toGrammar, transitionToRule] at h_v
Proof state after:
no goals
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w a✝)) ∈ M.F
Tactic:
case step h_w =>
  simp [fromDerivation, NFA.Run.last]
  apply fromDerivation_result
Proof state after:
no goals
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v h_w)) ∈ M.F
Tactic:
simp [toGrammar, transitionToRule] at h_v
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w)) ∈ M.F
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w)) ∈ M.F
Tactic:
simp [fromDerivation, NFA.Run.last]
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ s ∈ M.F
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ s ∈ M.F
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v h_w✝)) ∈ M.F
Tactic:
simp [toGrammar, transitionToRule] at h_v
Proof state after:
no goals
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w a✝)) ∈ M.F
Tactic:
simp [fromDerivation, NFA.Run.last]
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M a✝) ∈ M.F
Theorem: DFA.Run.fromDerivation_result
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M a✝) ∈ M.F
Tactic:
apply fromDerivation_result
Proof state after:
no goals
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ Grammar.GeneratedLanguage (toGrammar M) ⊆ AcceptedLanguage M
Tactic:
intro _ h
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ a✝ ∈ AcceptedLanguage M
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ a✝ ∈ AcceptedLanguage M
Tactic:
apply Nonempty.elim h
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝) → a✝ ∈ AcceptedLanguage M
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝) → a✝ ∈ AcceptedLanguage M
Tactic:
intro d
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ a✝ ∈ AcceptedLanguage M
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ a✝ ∈ AcceptedLanguage M
Tactic:
constructor
Proof state after:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ NFA.Run.last ?w ∈ M.F

case w
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Run M M.q₀ a✝
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ NFA.Run.last ?w ∈ M.F

case w
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Run M M.q₀ a✝
Tactic:
apply Run.fromDerivation_result
Proof state after:
case h.d
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ RegularGrammar.RegularDerivation (toGrammar M) M.q₀ a✝
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
case h.d
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ RegularGrammar.RegularDerivation (toGrammar M) M.q₀ a✝
Tactic:
apply RegularGrammar.RegularDerivation.fromDerivation
Proof state after:
case h.d.derivation
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl M.q₀] ?h.d.w'

case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = ?h.d.w'

case h.d.w'
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Word ({ x // x ∈ (toGrammar M).V } ⊕ { x // x ∈ (toGrammar M).Z })
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
case h.d.derivation
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl M.q₀] ?h.d.w'

case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = ?h.d.w'

case h.d.w'
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Word ({ x // x ∈ (toGrammar M).V } ⊕ { x // x ∈ (toGrammar M).Z })
Tactic:
assumption
Proof state after:
case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = Sum.inr <$> a✝
Theorem: DFA.toGrammar_lang_subs_lang
Proof state before:
case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = Sum.inr <$> a✝
Tactic:
rfl
Proof state after:
no goals
Theorem: DFA.toGrammar_lang_eq_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ Grammar.GeneratedLanguage (toGrammar M) = AcceptedLanguage M
Tactic:
apply Set.ext
Proof state after:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ (toGrammar M).Z }), x ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x ∈ AcceptedLanguage M
Theorem: DFA.toGrammar_lang_eq_lang
Proof state before:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ (toGrammar M).Z }), x ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x ∈ AcceptedLanguage M
Tactic:
intros
Proof state after:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x✝ ∈ AcceptedLanguage M
Theorem: DFA.toGrammar_lang_eq_lang
Proof state before:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x✝ ∈ AcceptedLanguage M
Tactic:
constructor
Proof state after:
case h.mp
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Theorem: DFA.toGrammar_lang_eq_lang
Proof state before:
case h.mp
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
apply toGrammar_lang_subs_lang
Proof state after:
case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Theorem: DFA.toGrammar_lang_eq_lang
Proof state before:
case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
apply lang_subs_toGrammar_lang
Proof state after:
no goals
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star M.toDFA (q, w) = some (del_star' M (q, w))
Tactic:
simp [DFA.del_star]
Proof state after:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star_curried M.toDFA w q = some (del_star' M (q, w))
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star_curried M.toDFA w q = some (del_star' M (q, w))
Tactic:
induction w generalizing q
Proof state after:
case nil
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))

case cons
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
tail_ih✝ : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
ih : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))
Tactic:
case cons _ _ ih =>
  unfold DFA.del_star_curried
  rw [total_del_eq] 
  apply ih
Proof state after:
no goals
Theorem: TotalDFA.total_del_star_eq
Proof state before:
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))
Tactic:
rfl
Proof state after:
no goals