internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert hd tl)
Tactic:
simp
Proof state after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ hd.length ∨ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ hd.length ∨ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl
Tactic:
right
Proof state after:
case h
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl
Theorem: FOL.NV.finset_var_name_max_len_mem
Proof state before:
case h
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl
Tactic:
exact ih c1
Proof state after:
no goals
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
Tactic:
obtain s1 := finset_var_name_max_len_mem x xs h
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
Tactic:
simp only [tsub_lt_tsub_iff_right s1]
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs < finset_var_name_max_len xs + 1
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs < finset_var_name_max_len xs + 1
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ fresh x c xs ∉ xs
Tactic:
unfold fresh
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs
Tactic:
simp
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
Tactic:
simp only [if_pos h]
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ fresh { toString := x.toString ++ c.toString } c xs ∉ xs
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ fresh { toString := x.toString ++ c.toString } c xs ∉ xs
Tactic:
apply fresh_not_mem
Proof state after:
no goals
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ fresh x c xs ∉ xs
Tactic:
unfold fresh
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs
Tactic:
simp
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
Tactic:
simp [if_neg h]
Proof state after:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ x ∉ xs
Theorem: FOL.NV.fresh_not_mem
Proof state before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ x ∉ xs
Tactic:
exact h
Proof state after:
no goals
Theorem: NFA.mem_accepts
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : NFA α σ
input : List α
⊢ e.accepts input ↔ ∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list
Tactic:
rfl
Proof state after:
no goals
Theorem: EpsilonNFA.eval_one_no_eps_def
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈ e.eval_one_no_eps starting_state_list symbol ↔
    ∃ state ∈ starting_state_list, stop_state ∈ symbol_arrow_list_to_fun e.symbol_arrow_list state symbol
Tactic:
simp only [eval_one_no_eps]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, stop_state ∈ symbol_arrow_list_to_fun e.symbol_arrow_list state symbol
Theorem: EpsilonNFA.eval_one_no_eps_def
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, stop_state ∈ symbol_arrow_list_to_fun e.symbol_arrow_list state symbol
Tactic:
simp
Proof state after:
no goals
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈ e.eval_one_no_eps starting_state_list symbol ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state
Tactic:
simp only [EpsilonNFA.eval_one_no_eps]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state
Tactic:
simp only [EpsilonNFA.toAbstract]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
simp only [symbol_arrow_list_to_fun]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map
            (fun state =>
              (List.filterMap
                    (fun arrow =>
                      if arrow.start_state = state ∧ arrow.symbol = symbol then some arrow.stop_state_list else none)
                    e.symbol_arrow_list).join.dedup)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map
            (fun state =>
              (List.filterMap
                    (fun arrow =>
                      if arrow.start_state = state ∧ arrow.symbol = symbol then some arrow.stop_state_list else none)
                    e.symbol_arrow_list).join.dedup)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
simp
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) →
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list

case mpr
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) →
    ∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
case mp
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) →
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
Tactic:
rintro ⟨_, h1, _, ⟨⟨⟩, h2, ⟨rfl, rfl⟩, rfl⟩, h3⟩
Proof state after:
case mp.intro.intro.intro.intro.intro.mk.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
stop_state start_state✝ : σ
symbol✝ : α
stop_state_list✝ : List σ
h2 : { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ } ∈ e.symbol_arrow_list
h1 :
  { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.start_state ∈
    starting_state_list
h3 :
  stop_state ∈ { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.stop_state_list
⊢ ∃ state ∈ starting_state_list,
    ∃ stop_state_list,
      { start_state := state,
            symbol := { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.symbol,
            stop_state_list := stop_state_list } ∈
          e.symbol_arrow_list ∧
        stop_state ∈ stop_state_list
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
case mp.intro.intro.intro.intro.intro.mk.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
stop_state start_state✝ : σ
symbol✝ : α
stop_state_list✝ : List σ
h2 : { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ } ∈ e.symbol_arrow_list
h1 :
  { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.start_state ∈
    starting_state_list
h3 :
  stop_state ∈ { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.stop_state_list
⊢ ∃ state ∈ starting_state_list,
    ∃ stop_state_list,
      { start_state := state,
            symbol := { start_state := start_state✝, symbol := symbol✝, stop_state_list := stop_state_list✝ }.symbol,
            stop_state_list := stop_state_list } ∈
          e.symbol_arrow_list ∧
        stop_state ∈ stop_state_list
Tactic:
exact ⟨_, h1, _, h2, h3⟩
Proof state after:
no goals
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
case mpr
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) →
    ∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l
Tactic:
rintro ⟨_, h1, _, h2, h3⟩
Proof state after:
case mpr.intro.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state w✝¹ : σ
h1 : w✝¹ ∈ starting_state_list
w✝ : List σ
h2 : { start_state := w✝¹, symbol := symbol, stop_state_list := w✝ } ∈ e.symbol_arrow_list
h3 : stop_state ∈ w✝
⊢ ∃ a ∈ starting_state_list,
    ∃ l,
      (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
        stop_state ∈ l
Theorem: EpsilonNFA.eval_one_no_eps_iff
Proof state before:
case mpr.intro.intro.intro.intro
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state w✝¹ : σ
h1 : w✝¹ ∈ starting_state_list
w✝ : List σ
h2 : { start_state := w✝¹, symbol := symbol, stop_state_list := w✝ } ∈ e.symbol_arrow_list
h3 : stop_state ∈ w✝
⊢ ∃ a ∈ starting_state_list,
    ∃ l,
      (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
        stop_state ∈ l
Tactic:
exact ⟨_, h1, _, ⟨_, h2, ⟨rfl, rfl⟩, rfl⟩, h3⟩
Proof state after:
no goals
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ state ∈ e.epsilon_closure starting_state_list ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Tactic:
simp only [epsilon_closure]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ state ∈ dft (epsilon_arrow_list_to_graph e.epsilon_arrow_list) starting_state_list ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ state ∈ dft (epsilon_arrow_list_to_graph e.epsilon_arrow_list) starting_state_list ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Tactic:
simp only [dft_iff]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ (∃ s ∈ starting_state_list,
      Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ b ∈ l) s
        state) ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state : σ
⊢ (∃ s ∈ starting_state_list,
      Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ b ∈ l) s
        state) ↔
    ∃ start_state ∈ starting_state_list, e.toAbstract.EpsilonClosure start_state state
Tactic:
congr! with a b c
Proof state after:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔ e.toAbstract.epsilon b c
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔ e.toAbstract.epsilon b c
Tactic:
simp [toAbstract]
Proof state after:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔
    ∃ stop_state_list,
      { start_state := b, stop_state_list := stop_state_list } ∈ e.epsilon_arrow_list ∧ c ∈ stop_state_list
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔
    ∃ stop_state_list,
      { start_state := b, stop_state_list := stop_state_list } ∈ e.epsilon_arrow_list ∧ c ∈ stop_state_list
Tactic:
induction e.epsilon_arrow_list <;> simp [*, epsilon_arrow_list_to_graph, or_and_right, exists_or]
Proof state after:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a.cons
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
⊢ ((∃ x, (b = head✝.start_state ∧ x = head✝.stop_state_list) ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list) ↔
    (∃ x, { start_state := b, stop_state_list := x } = head✝ ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a.cons
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
⊢ ((∃ x, (b = head✝.start_state ∧ x = head✝.stop_state_list) ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list) ↔
    (∃ x, { start_state := b, stop_state_list := x } = head✝ ∧ c ∈ x) ∨
      ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
Tactic:
apply or_congr_left <| exists_congr fun a => and_congr_left fun _ => ?_
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a✝ b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
a : List σ
x✝ : c ∈ a
⊢ b = head✝.start_state ∧ a = head✝.stop_state_list ↔ { start_state := b, stop_state_list := a } = head✝
Theorem: EpsilonNFA.epsilon_closure_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a✝ b c : σ
head✝ : EpsilonArrow σ
tail✝ : List (EpsilonArrow σ)
tail_ih✝ :
  (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph tail✝ ∧ c ∈ l) ↔
    ∃ stop_state_list, { start_state := b, stop_state_list := stop_state_list } ∈ tail✝ ∧ c ∈ stop_state_list
a : List σ
x✝ : c ∈ a
⊢ b = head✝.start_state ∧ a = head✝.stop_state_list ↔ { start_state := b, stop_state_list := a } = head✝
Tactic:
constructor <;> [rintro ⟨rfl, rfl⟩; rintro rfl] <;> [rfl; constructor <;> rfl]
Proof state after:
no goals