internlm/Lean-Github huggingface dataset:
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1
Tactic:
refine' .intro (.step _ _ r' rfl) ⟨q', hq', _⟩
Proof state after:
case some.mp.refine'_1
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ q' ∈ (toNFA M).δ (q, x)

case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ?some.mp.refine'_1 r' ⋯)
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp.refine'_1
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ q' ∈ (toNFA M).δ (q, x)

case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ?some.mp.refine'_1 r' ⋯)
Tactic:
simp [toNFA]
Proof state after:
case some.mp.refine'_1
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ M.δ (q, x) = some q'

case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp.refine'_1
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ M.δ (q, x) = some q'

case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
Tactic:
assumption
Proof state after:
case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
Tactic:
simp [bind_eq_bind]
Proof state after:
case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ constrRun xs q' = some r'
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp.refine'_2
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ constrRun xs q' = some r'
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ (∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1) →
    Option.isSome (del_star_curried M (x :: xs) q) = true
Tactic:
intro ⟨r, q', HQ', h⟩
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true
Tactic:
simp [del_star_curried, bind_eq_bind, hq']
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M xs q'✝) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M xs q'✝) = true
Tactic:
apply del_star_curried_isSome_iff_constrRun_isSome.mpr
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (constrRun xs q'✝) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (constrRun xs q'✝) = true
Tactic:
rw [isSome_iff_exists]
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ ∃ a, constrRun xs q'✝ = some a
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ ∃ a, constrRun xs q'✝ = some a
Tactic:
simp [hq'] at HQ'
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q'✝ = some a
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q'✝ = some a
Tactic:
rw [HQ']
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q' = some a
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q' = some a
Tactic:
simp [bind_eq_bind] at h
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
Tactic:
have ⟨r', _, _⟩ := h
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
r' : NFA.Run (toNFA M) q' xs
left✝ : constrRun xs q' = some r'
right✝ : NFA.Run.step q ⋯ r' ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q'✝ : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
r' : NFA.Run (toNFA M) q' xs
left✝ : constrRun xs q' = some r'
right✝ : NFA.Run.step q ⋯ r' ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
Tactic:
exists r'
Proof state after:
no goals
Theorem: DFA.del_star_isSome_iff_constrRun_isSome
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
⊢ Option.isSome (del_star M (q, w)) = true ↔ Option.isSome (constrRun w q) = true
Tactic:
simp [del_star]
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
⊢ Option.isSome (del_star_curried M w q) = true ↔ Option.isSome (constrRun w q) = true
Theorem: DFA.del_star_isSome_iff_constrRun_isSome
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
⊢ Option.isSome (del_star_curried M w q) = true ↔ Option.isSome (constrRun w q) = true
Tactic:
apply del_star_curried_isSome_iff_constrRun_isSome
Proof state after:
no goals
Theorem: DFA.in_language_iff_del_star_final
Proof 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
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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 _
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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
Proof state after:
no goals
Theorem: DFA.in_language_iff_del_star_final
Proof 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⟩
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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⟩
Proof 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)
Theorem: DFA.in_language_iff_del_star_final
Proof 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 _
Proof state after:
no goals
Theorem: DFA.in_language_iff_del_star_final
Proof 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⟩
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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₀
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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⟩)
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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]
Proof 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
Theorem: DFA.in_language_iff_del_star_final
Proof 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
Proof state after:
no goals
Theorem: DFA.lang_subs_toGrammar_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ AcceptedLanguage M ⊆ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
intro _ ⟨ run, h ⟩
Proof state after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Theorem: DFA.lang_subs_toGrammar_lang
Proof state before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
constructor
Proof state after:
case val
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
Theorem: DFA.lang_subs_toGrammar_lang
Proof state before:
case val
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
Tactic:
exact run.toDerivation _ h
Proof state after:
no goals
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 : RegularProduction.cons v (a, v') ∈ (toGrammar M).productions
⊢ M.δ (v, a) = some v'
Tactic:
simp [toGrammar, transitionToRule] at 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'
⊢ M.δ (v, a) = some v'