internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ) → ∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ
Tactic:
intro ⟨τ, hτ, hτ'⟩
Proof state after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ
Tactic:
simp only [satisfies_neg, not_not] at hτ hτ' ⊢
Proof state after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
let τ' := τ.set x (!τ x)
Proof state after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
have : (!τ' x) = τ x := by
  simp only [τ', τ.set_get x, Bool.not_not]
Proof state after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ ∃ τ, ¬τ ⊨ φ ∧ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
refine ⟨τ', hτ', ?_⟩
Proof state after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ (PropAssignment.set τ' x !τ' x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ (PropAssignment.set τ' x !τ' x) ⊨ φ
Tactic:
rw [τ.set_set, this, τ.set_same]
Proof state after:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a.mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
this : (!τ' x) = τ x
⊢ τ ⊨ φ
Tactic:
exact hτ
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
τ' : PropAssignment ν := PropAssignment.set τ x !τ x
⊢ (!τ' x) = τ x
Tactic:
simp only [τ', τ.set_get x, Bool.not_not]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_conj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⊓ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
intro x
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊓ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_conj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊓ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂
Tactic:
simp only [Finset.mem_union, mem_semVars, satisfies_conj, not_and_or]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, (τ ⊨ φ₁ ∧ τ ⊨ φ₂) ∧ (¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ∨ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂)) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.semVars_conj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, (τ ⊨ φ₁ ∧ τ ⊨ φ₂) ∧ (¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ∨ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂)) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_disj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⊔ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
intro x
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊔ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_disj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊔ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂
Tactic:
simp only [Finset.mem_union, mem_semVars]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ₁ ⊔ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ⊔ φ₂) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.semVars_disj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ₁ ⊔ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ⊔ φ₂) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_impl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [himp_eq]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_impl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
have := semVars_disj (φ₁ᶜ) φ₂
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₁ᶜ ⊔ φ₂) ⊆ semVars φ₁ᶜ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_impl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₁ᶜ ⊔ φ₂) ⊆ semVars φ₁ᶜ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [sup_comm, semVars_neg] at this
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_impl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
exact this
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (biImpl φ₁ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [biImpl_eq_impls]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars ((φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars ((φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
apply subset_trans (semVars_conj _ _)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ∪ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ∪ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
apply Finset.union_subset
Proof state after:
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂

case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂

case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
. apply semVars_impl
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
. rw [Finset.union_comm]
  apply semVars_impl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
apply semVars_impl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [Finset.union_comm]
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₂ ∪ semVars φ₁
Theorem: LeanSAT.Model.PropFun.semVars_biImpl
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₂ ∪ semVars φ₁
Tactic:
apply semVars_impl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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 τ
Proof 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 φ) τ' ⊨ φ
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof state before:
case empty
ν : Type u_1
inst✝¹ inst✝ : DecidableEq ν
τ' : PropAssignment ν
φ : PropFun ν
τ : PropAssignment ν
⊢ PropAssignment.setMany τ ∅ τ' ⊨ φ ↔ PropAssignment.setMany τ (∅ ∩ semVars φ) τ' ⊨ φ
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof 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 φ) τ' ⊨ φ
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof 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 φ) τ' ⊨ φ
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof 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 φ) τ' ⊨ φ
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof 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 τ' ⊨ φ
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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
Proof 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 τ' ⊨ φ
Theorem: LeanSAT.Model.PropFun.setMany_satisfies_iff_inter_semVars
Proof 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]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ ↔ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
constructor
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
case mp =>
  intro h
  exact ⟨fun σ₁ h₁ => h σ₁ |>.mp ⟨σ₁, σ₁.agreeOn_refl X, h₁⟩,
    fun σ₂ h₂ => h σ₂ |>.mpr ⟨σ₂, σ₂.agreeOn_refl X, h₂⟩⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂
Tactic:
case mpr =>
  intro ⟨h₁, h₂⟩
  intro τ
  constructor
  case mp =>
    intro ⟨σ₁, hAgree₁, hσ₁⟩
    have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
    exact ⟨σ₂, hAgree₂.trans hAgree₁, hσ₂⟩
  case mpr =>
    intro ⟨σ₂, hAgree₂, hσ₂⟩
    have ⟨σ₁, hAgree₁, hσ₁⟩ := h₂ σ₂ hσ₂
    exact ⟨σ₁, hAgree₁.trans hAgree₂, hσ₁⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h : equivalentOver X φ₁ φ₂
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h : equivalentOver X φ₁ φ₂
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
exact ⟨fun σ₁ h₁ => h σ₁ |>.mp ⟨σ₁, σ₁.agreeOn_refl X, h₁⟩,
  fun σ₂ h₂ => h σ₂ |>.mpr ⟨σ₂, σ₂.agreeOn_refl X, h₂⟩⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂
Tactic:
intro ⟨h₁, h₂⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
⊢ equivalentOver X φ₁ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
⊢ equivalentOver X φ₁ φ₂
Tactic:
intro τ
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) ↔ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) ↔ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
constructor
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂) → ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
case mp =>
  intro ⟨σ₁, hAgree₁, hσ₁⟩
  have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
  exact ⟨σ₂, hAgree₂.trans hAgree₁, hσ₂⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂) → ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
case mpr =>
  intro ⟨σ₂, hAgree₂, hσ₂⟩
  have ⟨σ₁, hAgree₁, hσ₁⟩ := h₂ σ₂ hσ₂
  exact ⟨σ₁, hAgree₁.trans hAgree₂, hσ₁⟩
Proof state after:
no goals