Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
τ : PropAssignment ν
x : ν
⊢ τ ⊨ φ → (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ → x ∈ vars φ
Tactic:
intro hτ hτ'
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
τ : PropAssignment ν
x : ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ x ∈ vars φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
τ : PropAssignment ν
x : ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ x ∈ vars φ
Tactic:
induction φ generalizing τ with
| tr => exfalso; exact hτ' satisfies_tr
| fls => exfalso; exact not_satisfies_fls hτ
| var y =>
  simp_all only [vars, satisfies_var, Finset.mem_singleton]
  by_contra h
  exact hτ' (hτ ▸ τ.set_get_of_ne (!τ x) h)
| _ =>
  simp_all only
    [satisfies_conj, satisfies_disj, satisfies_impl', satisfies_biImpl', vars, Finset.mem_union]
  push_neg at hτ'
  aesop
State after:
no goals

State before:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ x ∈ vars tr
Tactic:
exfalso
State after:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ False

State before:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ False
Tactic:
exact hτ' satisfies_tr
State after:
no goals

State before:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ fls
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ fls
⊢ x ∈ vars fls
Tactic:
exfalso
State after:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ fls
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ fls
⊢ False

State before:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ fls
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ fls
⊢ False
Tactic:
exact not_satisfies_fls hτ
State after:
no goals

State before:
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ ⊨ var y
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ var y
⊢ x ∈ vars (var y)
Tactic:
simp_all only [vars, satisfies_var, Finset.mem_singleton]
State after:
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
⊢ x = y

State before:
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
⊢ x = y
Tactic:
by_contra h
State after:
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
h : ¬x = y
⊢ False

State before:
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
h : ¬x = y
⊢ False
Tactic:
exact hτ' (hτ ▸ τ.set_get_of_ne (!τ x) h)
State after:
no goals

State before:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ biImpl φ₁✝ φ₂✝
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ biImpl φ₁✝ φ₂✝
⊢ x ∈ vars (biImpl φ₁✝ φ₂✝)
Tactic:
simp_all only
  [satisfies_conj, satisfies_disj, satisfies_impl', satisfies_biImpl', vars, Finset.mem_union]
State after:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ φ₁✝ ∧ τ ⊨ φ₂✝ ∨ ¬τ ⊨ φ₁✝ ∧ ¬τ ⊨ φ₂✝
hτ' :
  ¬((PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∧ (PropAssignment.set τ x !τ x) ⊨ φ₂✝ ∨
      ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝)
⊢ x ∈ vars φ₁✝ ∨ x ∈ vars φ₂✝

State before:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ φ₁✝ ∧ τ ⊨ φ₂✝ ∨ ¬τ ⊨ φ₁✝ ∧ ¬τ ⊨ φ₂✝
hτ' :
  ¬((PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∧ (PropAssignment.set τ x !τ x) ⊨ φ₂✝ ∨
      ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝)
⊢ x ∈ vars φ₁✝ ∨ x ∈ vars φ₂✝
Tactic:
push_neg at hτ'
State after:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ φ₁✝ ∧ τ ⊨ φ₂✝ ∨ ¬τ ⊨ φ₁✝ ∧ ¬τ ⊨ φ₂✝
hτ' :
  (¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∨ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝) ∧
    ((PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∨ (PropAssignment.set τ x !τ x) ⊨ φ₂✝)
⊢ x ∈ vars φ₁✝ ∨ x ∈ vars φ₂✝

State before:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ φ₁✝ ∧ τ ⊨ φ₂✝ ∨ ¬τ ⊨ φ₁✝ ∧ ¬τ ⊨ φ₂✝
hτ' :
  (¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∨ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝) ∧
    ((PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∨ (PropAssignment.set τ x !τ x) ⊨ φ₂✝)
⊢ x ∈ vars φ₁✝ ∨ x ∈ vars φ₂✝
Tactic:
aesop
State after:
no goals