Theorem: DFA.in_language_iff_del_star_final (FormalSystems/Chomsky/Regular/DFA.lean)

State before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ AcceptedLanguage M ↔ ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F
Tactic:
constructor
State after:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ AcceptedLanguage M → ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F

case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M

State before:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ AcceptedLanguage M → ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F

case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M
Tactic:
. intro ⟨r, hr⟩
  refine' .intro r.last ⟨_, hr⟩
  exact last_state_eq_del_star _
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M
Tactic:
. intro ⟨qf, hdel, hf⟩
  let r := constrRun w M.q₀
  have : r.isSome :=
    del_star_isSome_iff_constrRun_isSome.mp
      (Option.isSome_iff_exists.mpr ⟨qf, hdel⟩)
  exists r.get this
  simp [last_state_eq_del_star (r.get this)] at hdel
  rw [hdel]; assumption
State after:
no goals

State before:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ AcceptedLanguage M → ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F
Tactic:
intro ⟨r, hr⟩
State after:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
r : Run M M.q₀ w
hr : NFA.Run.last r ∈ M.F
⊢ ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F

State before:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
r : Run M M.q₀ w
hr : NFA.Run.last r ∈ M.F
⊢ ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F
Tactic:
refine' .intro r.last ⟨_, hr⟩
State after:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
r : Run M M.q₀ w
hr : NFA.Run.last r ∈ M.F
⊢ NFA.Run.last r ∈ del_star M (M.q₀, w)

State before:
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
r : Run M M.q₀ w
hr : NFA.Run.last r ∈ M.F
⊢ NFA.Run.last r ∈ del_star M (M.q₀, w)
Tactic:
exact last_state_eq_del_star _
State after:
no goals

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M
Tactic:
intro ⟨qf, hdel, hf⟩
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
⊢ w ∈ AcceptedLanguage M

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
⊢ w ∈ AcceptedLanguage M
Tactic:
let r := constrRun w M.q₀
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
⊢ w ∈ AcceptedLanguage M

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
⊢ w ∈ AcceptedLanguage M
Tactic:
have : r.isSome :=
  del_star_isSome_iff_constrRun_isSome.mp
    (Option.isSome_iff_exists.mpr ⟨qf, hdel⟩)
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
⊢ w ∈ AcceptedLanguage M

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
⊢ w ∈ AcceptedLanguage M
Tactic:
exists r.get this
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
⊢ NFA.Run.last (Option.get r this) ∈ M.F

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hdel : qf ∈ del_star M (M.q₀, w)
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
⊢ NFA.Run.last (Option.get r this) ∈ M.F
Tactic:
simp [last_state_eq_del_star (r.get this)] at hdel
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
hdel : NFA.Run.last (Option.get r this) = qf
⊢ NFA.Run.last (Option.get r this) ∈ M.F

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
hdel : NFA.Run.last (Option.get r this) = qf
⊢ NFA.Run.last (Option.get r this) ∈ M.F
Tactic:
rw [hdel]
State after:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
hdel : NFA.Run.last (Option.get r this) = qf
⊢ qf ∈ M.F

State before:
case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
qf : { x // x ∈ M.Q }
hf : qf ∈ M.F
r : Option (NFA.Run (toNFA M) M.q₀ w) := constrRun w M.q₀
this : Option.isSome r = true
hdel : NFA.Run.last (Option.get r this) = qf
⊢ qf ∈ M.F
Tactic:
assumption
State after:
no goals