Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited (FOL/Parsing/DFT.lean)

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
induction stack, visited using dft_aux.induct g
State after:
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
⊢ ↑(dft_aux g [] visited✝).toFinset ⊆ reachable_from_list g [] ∪ ↑visited✝.toFinset

case case2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∈ visited✝
ih1✝ : ↑(dft_aux g xs✝ visited✝).toFinset ⊆ reachable_from_list g xs✝ ∪ ↑visited✝.toFinset
⊢ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset ⊆ reachable_from_list g (x✝ :: xs✝) ∪ ↑visited✝.toFinset

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ :
  ↑(dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x✝ ++ xs✝) ∪ ↑(x✝ :: visited✝).toFinset
⊢ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset ⊆ reachable_from_list g (x✝ :: xs✝) ∪ ↑visited✝.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑(dft_aux g [] visited).toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Tactic:
case _ visited =>
  simp only [dft_aux]
  simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆ reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
case _ visited x stack c1 ih =>
  simp only [reachable_from_list_of_cons g x stack]
  simp only [dft_aux]
  simp only [if_pos c1]
  simp only [Set.union_assoc ]
  exact Set.subset_union_of_subset_right ih (reachable_from_list g [x])
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑(dft_aux g [] visited).toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Tactic:
simp only [dft_aux]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑visited.toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑visited.toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Tactic:
simp
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆ reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [reachable_from_list_of_cons g x stack]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [dft_aux]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [if_pos c1]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [Set.union_assoc ]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ (reachable_from_list g stack ∪ ↑visited.toFinset)

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ (reachable_from_list g stack ∪ ↑visited.toFinset)
Tactic:
exact Set.subset_union_of_subset_right ih (reachable_from_list g [x])
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆ reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [dft_aux]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [if_neg c1]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [reachable_from_list_of_append g (direct_succ_list g x) stack] at ih
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [reachable_from_list_of_cons g x stack]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
trans (reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ (x :: visited).toFinset.toSet)
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset

Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
Tactic:
exact ih
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
have s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x] := reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list g x
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [Set.subset_def] at *
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ∀ x_1 ∈ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset,
    x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset,
    x_1 ∈ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ∀ x_1 ∈ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset,
    x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset,
    x_1 ∈ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp at *
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
ih :
  ∀ x_1 ∈ dft_aux g (direct_succ_list g x ++ stack) (x :: visited),
    x_1 = x ∨ (x_1 ∈ reachable_from_list g (direct_succ_list g x) ∨ x_1 ∈ reachable_from_list g stack) ∨ x_1 ∈ visited
⊢ ((x ∈ reachable_from_list g [x] ∨ x ∈ reachable_from_list g stack) ∨ x ∈ visited) ∧
    ∀ (a : Node),
      (a ∈ reachable_from_list g (direct_succ_list g x) ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited →
        (a ∈ reachable_from_list g [x] ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
ih :
  ∀ x_1 ∈ dft_aux g (direct_succ_list g x ++ stack) (x :: visited),
    x_1 = x ∨ (x_1 ∈ reachable_from_list g (direct_succ_list g x) ∨ x_1 ∈ reachable_from_list g stack) ∨ x_1 ∈ visited
⊢ ((x ∈ reachable_from_list g [x] ∨ x ∈ reachable_from_list g stack) ∨ x ∈ visited) ∧
    ∀ (a : Node),
      (a ∈ reachable_from_list g (direct_succ_list g x) ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited →
        (a ∈ reachable_from_list g [x] ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited
Tactic:
tauto
State after:
no goals