internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case mp
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ → l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
intro hlit
Proof state after:
case mp
l₁ l₂ : ILit
hlit : ILit.index l₁ = ILit.index l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case mp
l₁ l₂ : ILit
hlit : ILit.index l₁ = ILit.index l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
simp at hlit
Proof state after:
case mp
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case mp
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
by_cases hpol : polarity l₁ = polarity l₂
Proof state after:
case pos
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂

case neg
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case pos
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
left
Proof state after:
case pos.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case pos.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂
Tactic:
ext
Proof state after:
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ toVar l₁ = toVar l₂

case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ polarity l₁ = polarity l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ toVar l₁ = toVar l₂
Tactic:
exact hlit
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ polarity l₁ = polarity l₂
Tactic:
exact hpol
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case neg
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
right
Proof state after:
case neg.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ negate l₁ = l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case neg.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ negate l₁ = l₂
Tactic:
ext
Proof state after:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ toVar (negate l₁) = toVar l₂

case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ toVar (negate l₁) = toVar l₂
Tactic:
simpa
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
Tactic:
rw [← Bool.bnot_eq] at hpol
Proof state after:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : (!polarity l₁) = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : (!polarity l₁) = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
Tactic:
simp [hpol]
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case mpr
l₁ l₂ : ILit
⊢ l₁ = l₂ ∨ negate l₁ = l₂ → ILit.index l₁ = ILit.index l₂
Tactic:
rintro (rfl | rfl)
Proof state after:
case mpr.inl
l₁ : ILit
⊢ ILit.index l₁ = ILit.index l₁

case mpr.inr
l₁ : ILit
⊢ ILit.index l₁ = ILit.index (negate l₁)
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case mpr.inl
l₁ : ILit
⊢ ILit.index l₁ = ILit.index l₁
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
case mpr.inr
l₁ : ILit
⊢ ILit.index l₁ = ILit.index (negate l₁)
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_of_agreeOn_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂ → eval σ₁ φ = eval σ₂ φ
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ
Theorem: LeanSAT.Model.PropForm.eval_of_agreeOn_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
induction φ <;> simp_all [PropAssignment.agreeOn, eval, vars]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_set_of_not_mem_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
⊢ x ∉ vars φ → eval (PropAssignment.set τ x b) φ = eval τ φ
Tactic:
intro hNMem
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ eval (PropAssignment.set τ x b) φ = eval τ φ
Theorem: LeanSAT.Model.PropForm.eval_set_of_not_mem_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ eval (PropAssignment.set τ x b) φ = eval τ φ
Tactic:
apply eval_of_agreeOn_vars
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ PropAssignment.agreeOn (↑(vars φ)) (PropAssignment.set τ x b) τ
Theorem: LeanSAT.Model.PropForm.eval_set_of_not_mem_vars
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ PropAssignment.agreeOn (↑(vars φ)) (PropAssignment.set τ x b) τ
Tactic:
intro y hY
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
⊢ PropAssignment.set τ x b y = τ y
Theorem: LeanSAT.Model.PropForm.eval_set_of_not_mem_vars
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
⊢ PropAssignment.set τ x b y = τ y
Tactic:
have : y ≠ x := fun h => hNMem (h ▸ hY)
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
this : y ≠ x
⊢ PropAssignment.set τ x b y = τ y
Theorem: LeanSAT.Model.PropForm.eval_set_of_not_mem_vars
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
this : y ≠ x
⊢ PropAssignment.set τ x b y = τ y
Tactic:
simp [PropAssignment.set, this]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.agreeOn_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂ → (σ₁ ⊨ φ ↔ σ₂ ⊨ φ)
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ σ₁ ⊨ φ ↔ σ₂ ⊨ φ
Theorem: LeanSAT.Model.PropForm.agreeOn_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ σ₁ ⊨ φ ↔ σ₂ ⊨ φ
Tactic:
simp [SemanticEntails.entails, satisfies, eval_of_agreeOn_vars h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
τ : PropAssignment ν
x : ν
⊢ τ ⊨ φ → (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ → x ∈ vars φ
Tactic:
intro hτ hτ'
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
τ : PropAssignment ν
x : ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ x ∈ vars φ
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof state before:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ x ∈ vars tr
Tactic:
exfalso
Proof state after:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ tr
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ tr
⊢ False
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof state before:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ fls
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ fls
⊢ x ∈ vars fls
Tactic:
exfalso
Proof state after:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
τ : PropAssignment ν
hτ : τ ⊨ fls
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ fls
⊢ False
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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τ
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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]
Proof state after:
case var
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ y = true
hτ' : ¬PropAssignment.set τ x (!τ x) y = true
⊢ x = y
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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
Proof 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
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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]
Proof 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 φ₂✝
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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τ'
Proof 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 φ₂✝
Theorem: LeanSAT.Model.PropForm.mem_vars_of_flip
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
s : Finset ν := Finset.filter (fun x => σ₁ x ≠ σ₂ x) (vars φ)
hS : ∀ x ∈ s, σ₁ x ≠ σ₂ x
⊢ ∀ x ∈ vars φ \ s, σ₁ x = σ₂ x
Tactic:
simp_all [s]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₁ σ₂ : PropAssignment ν
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
s : Finset ν
hS : ∀ x ∈ s, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ s, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ s ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
induction s using Finset.induction generalizing σ₁
Proof state after:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ

case insert
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s✝, σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s✝, σ₁ x = σ₂ x) → ∃ x τ, x ∈ s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert a✝² s✝, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert a✝² s✝, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert a✝² s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ

case insert
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s✝, σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s✝, σ₁ x = σ₂ x) → ∃ x τ, x ∈ s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert a✝² s✝, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert a✝² s✝, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert a✝² s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
. have : σ₁.agreeOn φ.vars σ₂ := by rw [Finset.sdiff_empty] at hSC; exact hSC
  have : σ₂ ⊨ φ := (agreeOn_vars this).mp h₁
  exact False.elim (h₂ this)
Proof state after:
case insert
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s✝, σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s✝, σ₁ x = σ₂ x) → ∃ x τ, x ∈ s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert a✝² s✝, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert a✝² s✝, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert a✝² s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
case insert
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
a✝² : ν
s✝ : Finset ν
a✝¹ : a✝² ∉ s✝
a✝ :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s✝, σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s✝, σ₁ x = σ₂ x) → ∃ x τ, x ∈ s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert a✝² s✝, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert a✝² s✝, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert a✝² s✝ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
next x₀ s' hx₀ ih =>
  let σ₁' := σ₁.set x₀ (!σ₁ x₀)
  by_cases h₁' : σ₁' ⊨ φ
  case neg =>
    use x₀, σ₁
    simp [h₁, h₁']
  case pos =>
    have hS' : ∀ x ∈ s', σ₁' x ≠ σ₂ x := fun x hMem => by
      have hX : x₀ ≠ x := fun h => hx₀ (h ▸ hMem)
      simp only [σ₁', σ₁.set_get_of_ne (!σ₁ x₀) hX]
      exact hS _ (Finset.mem_insert_of_mem hMem)
    have hSC' : ∀ x ∈ φ.vars \ s', σ₁' x = σ₂ x := fun x hMem => by
      by_cases hX : x₀ = x
      case pos =>
        have := hS _ (Finset.mem_insert_self _ _)
        simp only [σ₁', ← hX, PropAssignment.set_get, Bool.bnot_eq,
                    this, not_false_eq_true]
      case neg =>
        simp only [σ₁', σ₁.set_get_of_ne _ hX]
        aesop
    have ⟨x, τ, hx, H⟩ := ih h₁' hS' hSC'
    exact ⟨x, τ, Finset.mem_insert_of_mem hx, H⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
have : σ₁.agreeOn φ.vars σ₂ := by rw [Finset.sdiff_empty] at hSC; exact hSC
Proof state after:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
this : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
this : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
have : σ₂ ⊨ φ := (agreeOn_vars this).mp h₁
Proof state after:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
this✝ : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
this : σ₂ ⊨ φ
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
case empty
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
this✝ : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
this : σ₂ ⊨ φ
⊢ ∃ x τ, x ∈ ∅ ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
exact False.elim (h₂ this)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ ∅, σ₁ x = σ₂ x
⊢ PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
Tactic:
rw [Finset.sdiff_empty] at hSC
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ, σ₁ x = σ₂ x
⊢ PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ ∅, σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ, σ₁ x = σ₂ x
⊢ PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
Tactic:
exact hSC
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.exists_flip
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
let σ₁' := σ₁.set x₀ (!σ₁ x₀)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁✝ σ₂✝ : PropAssignment ν
h₁✝ : σ₁✝ ⊨ φ
h₂✝ : ¬σ₂✝ ⊨ φ
σ₂ : PropAssignment ν
h₂ : ¬σ₂ ⊨ φ
x₀ : ν
s' : Finset ν
hx₀ : x₀ ∉ s'
ih :
  ∀ {σ₁ : PropAssignment ν},
    σ₁ ⊨ φ →
      (∀ x ∈ s', σ₁ x ≠ σ₂ x) →
        (∀ x ∈ vars φ \ s', σ₁ x = σ₂ x) → ∃ x τ, x ∈ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
σ₁ : PropAssignment ν
h₁ : σ₁ ⊨ φ
hS : ∀ x ∈ insert x₀ s', σ₁ x ≠ σ₂ x
hSC : ∀ x ∈ vars φ \ insert x₀ s', σ₁ x = σ₂ x
σ₁' : PropAssignment ν := PropAssignment.set σ₁ x₀ !σ₁ x₀
⊢ ∃ x τ, x ∈ insert x₀ s' ∧ τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ