Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ : PropAssignment ν
vs : Finset ν
τ' : PropAssignment ν
φ : PropFun ν
⊢ PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
Tactic:
induction vs using Finset.induction generalizing τ
State after:
case empty
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
τ : PropAssignment ν
⊢ PropAssignment.setMany τ ∅ τ' ⊨ φ ↔ PropAssignment.setMany τ (∅ ∩ semVars φ) τ' ⊨ φ

case insert
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ s✝ τ' ⊨ φ ↔ PropAssignment.setMany τ (s✝ ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
⊢ PropAssignment.setMany τ (insert a✝² s✝) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert a✝² s✝ ∩ semVars φ) τ' ⊨ φ

State before:
case insert
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ s✝ τ' ⊨ φ ↔ PropAssignment.setMany τ (s✝ ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
⊢ PropAssignment.setMany τ (insert a✝² s✝) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert a✝² s✝ ∩ semVars φ) τ' ⊨ φ
Tactic:
next x vs hx ih =>
if h : x ∈ φ.semVars then
  rw [Finset.insert_eq, Finset.union_inter_distrib_right
      , Finset.singleton_inter_of_mem h]
  simp [PropAssignment.setMany_union]; apply ih
else
simp [Finset.insert_eq, Finset.union_inter_distrib_right
    , Finset.singleton_inter_of_not_mem h
    , PropAssignment.setMany_union]
rw [← ih _, ← τ.set_setMany_comm _ _ _ _ hx]
rw [not_mem_semVars] at h
rw [h]
State after:
no goals

State before:
case empty
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
τ : PropAssignment ν
⊢ PropAssignment.setMany τ ∅ τ' ⊨ φ ↔ PropAssignment.setMany τ (∅ ∩ semVars φ) τ' ⊨ φ
Tactic:
simp
State after:
no goals

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
⊢ PropAssignment.setMany τ (insert x vs) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert x vs ∩ semVars φ) τ' ⊨ φ
Tactic:
if h : x ∈ φ.semVars then
  rw [Finset.insert_eq, Finset.union_inter_distrib_right
      , Finset.singleton_inter_of_mem h]
  simp [PropAssignment.setMany_union]; apply ih
else
simp [Finset.insert_eq, Finset.union_inter_distrib_right
    , Finset.singleton_inter_of_not_mem h
    , PropAssignment.setMany_union]
rw [← ih _, ← τ.set_setMany_comm _ _ _ _ hx]
rw [not_mem_semVars] at h
rw [h]
State after:
no goals

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany τ (insert x vs) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert x vs ∩ semVars φ) τ' ⊨ φ
Tactic:
rw [Finset.insert_eq, Finset.union_inter_distrib_right
    , Finset.singleton_inter_of_mem h]
State after:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany τ ({x} ∪ vs) τ' ⊨ φ ↔ PropAssignment.setMany τ ({x} ∪ vs ∩ semVars φ) τ' ⊨ φ

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany τ ({x} ∪ vs) τ' ⊨ φ ↔ PropAssignment.setMany τ ({x} ∪ vs ∩ semVars φ) τ' ⊨ φ
Tactic:
simp [PropAssignment.setMany_union]
State after:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany (PropAssignment.set τ x (τ' x)) vs τ' ⊨ φ ↔
    PropAssignment.setMany (PropAssignment.set τ x (τ' x)) (vs ∩ semVars φ) τ' ⊨ φ

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∈ semVars φ
⊢ PropAssignment.setMany (PropAssignment.set τ x (τ' x)) vs τ' ⊨ φ ↔
    PropAssignment.setMany (PropAssignment.set τ x (τ' x)) (vs ∩ semVars φ) τ' ⊨ φ
Tactic:
apply ih
State after:
no goals

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∉ semVars φ
⊢ PropAssignment.setMany τ (insert x vs) τ' ⊨ φ ↔ PropAssignment.setMany τ (insert x vs ∩ semVars φ) τ' ⊨ φ
Tactic:
simp [Finset.insert_eq, Finset.union_inter_distrib_right
    , Finset.singleton_inter_of_not_mem h
    , PropAssignment.setMany_union]
State after:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∉ semVars φ
⊢ PropAssignment.setMany (PropAssignment.set τ x (τ' x)) vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∉ semVars φ
⊢ PropAssignment.setMany (PropAssignment.set τ x (τ' x)) vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
Tactic:
rw [← ih _, ← τ.set_setMany_comm _ _ _ _ hx]
State after:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∉ semVars φ
⊢ PropAssignment.set (PropAssignment.setMany τ vs τ') x (τ' x) ⊨ φ ↔ PropAssignment.setMany τ vs τ' ⊨ φ

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : x ∉ semVars φ
⊢ PropAssignment.set (PropAssignment.setMany τ vs τ') x (τ' x) ⊨ φ ↔ PropAssignment.setMany τ vs τ' ⊨ φ
Tactic:
rw [not_mem_semVars] at h
State after:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
⊢ PropAssignment.set (PropAssignment.setMany τ vs τ') x (τ' x) ⊨ φ ↔ PropAssignment.setMany τ vs τ' ⊨ φ

State before:
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
x : ν
vs : Finset ν
hx : x ∉ vs
ih : ∀ (τ : PropAssignment ν), PropAssignment.setMany τ vs τ' ⊨ φ ↔ PropAssignment.setMany τ (vs ∩ semVars φ) τ' ⊨ φ
τ : PropAssignment ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
⊢ PropAssignment.set (PropAssignment.setMany τ vs τ') x (τ' x) ⊨ φ ↔ PropAssignment.setMany τ vs τ' ⊨ φ
Tactic:
rw [h]
State after:
no goals