internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.semVars_mk
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ
Tactic:
have := semVars'_subset_vars φ
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ
Theorem: LeanSAT.Model.PropFun.semVars_mk
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ
Tactic:
unfold semVars
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ Set.Finite.toFinset ⋯ ⊆ PropForm.vars φ
Theorem: LeanSAT.Model.PropFun.semVars_mk
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ Set.Finite.toFinset ⋯ ⊆ PropForm.vars φ
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φ ↔ ∃ τ, τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
simp [Set.Finite.mem_toFinset, semVars, semVars']
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∉ semVars φ ↔ ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
simp [mem_semVars, -Bool.forall_bool]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) ↔
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) ↔
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
constructor
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) →
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ) →
    ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) →
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
intro h τ b
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
if b = τ x then
  simp_all
else
  have : b = !τ x := by apply Bool.eq_not_iff.mpr; assumption
  constructor <;> convert h _ ; simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : b = τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
simp_all
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
have : b = !τ x := by apply Bool.eq_not_iff.mpr; assumption
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
constructor <;> convert h _
Proof state after:
case h'.h.e'_4
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
a✝ : PropAssignment.set τ x b ⊨ φ
⊢ τ = PropAssignment.set (PropAssignment.set τ x b) x !PropAssignment.set τ x b x
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
case h'.h.e'_4
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
a✝ : PropAssignment.set τ x b ⊨ φ
⊢ τ = PropAssignment.set (PropAssignment.set τ x b) x !PropAssignment.set τ x b x
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ b = !τ x
Tactic:
apply Bool.eq_not_iff.mpr
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ b ≠ τ x
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ b ≠ τ x
Tactic:
assumption
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ) →
    ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
Tactic:
intro h τ hτφ
Proof state after:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
have := h τ (!τ x)
Proof state after:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
this : (PropAssignment.set τ x !τ x) ⊨ φ ↔ τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.not_mem_semVars
Proof state before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
this : (PropAssignment.set τ x !τ x) ⊨ φ ↔ τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ σ₁ ⊨ φ → (fun M φ => ¬M ⊨ φ) σ₂ φ → ∃ x, σ₁ x ≠ σ₂ x ∧ x ∈ semVars φ
Tactic:
have ⟨φ', hMk⟩ := Quotient.exists_rep φ
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → (fun M φ => ¬M ⊨ φ) σ₂ φ → ∃ x, σ₁ x ≠ σ₂ x ∧ x ∈ semVars φ
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → (fun M φ => ¬M ⊨ φ) σ₂ φ → ∃ x, σ₁ x ≠ σ₂ x ∧ x ∈ semVars φ
Tactic:
dsimp
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → ¬σ₂ ⊨ φ → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars φ
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ → ¬σ₂ ⊨ φ → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars φ
Tactic:
rw [← hMk, satisfies_mk, satisfies_mk]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ' → ¬σ₂ ⊨ φ' → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
⊢ σ₁ ⊨ φ' → ¬σ₂ ⊨ φ' → ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Tactic:
intro h₁ h₂
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Tactic:
have ⟨x, τ, hNe, hτ, hτ'⟩ := PropForm.exists_flip h₁ h₂
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ x, ¬σ₁ x = σ₂ x ∧ x ∈ semVars ⟦φ'⟧
Tactic:
use x, hNe
Proof state after:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ x ∈ semVars ⟦φ'⟧
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ x ∈ semVars ⟦φ'⟧
Tactic:
simp only [mem_semVars]
Proof state after:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ τ, τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
case right
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ ∃ τ, τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧
Tactic:
use τ
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ ⟦φ'⟧ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ ⟦φ'⟧
Tactic:
rw [satisfies_mk, satisfies_mk]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ φ' ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ'
Theorem: LeanSAT.Model.PropFun.exists_semVar
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
φ' : PropForm ν
hMk : ⟦φ'⟧ = φ
h₁ : σ₁ ⊨ φ'
h₂ : ¬σ₂ ⊨ φ'
x : ν
τ : PropAssignment ν
hNe : σ₁ x ≠ σ₂ x
hτ : τ ⊨ φ'
hτ' : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ'
⊢ τ ⊨ φ' ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ'
Tactic:
exact ⟨hτ, hτ'⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → (σ₁ ⊨ φ ↔ σ₂ ⊨ φ)
Tactic:
suffices ∀ {σ₁ σ₂}, σ₁.agreeOn φ.semVars σ₂ → σ₁ ⊨ φ → σ₂ ⊨ φ from
  fun h => ⟨this h, this h.symm⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ ∀ {σ₁ σ₂ : PropAssignment ν}, PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → σ₁ ⊨ φ → σ₂ ⊨ φ
Theorem: LeanSAT.Model.PropFun.agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ ∀ {σ₁ σ₂ : PropAssignment ν}, PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → σ₁ ⊨ φ → σ₂ ⊨ φ
Tactic:
intro σ₁ σ₂ h h₁
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
⊢ σ₂ ⊨ φ
Theorem: LeanSAT.Model.PropFun.agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
⊢ σ₂ ⊨ φ
Tactic:
by_contra h₂
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
⊢ False
Theorem: LeanSAT.Model.PropFun.agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
⊢ False
Tactic:
have ⟨x, hNe, hMem⟩ := exists_semVar h₁ h₂
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
x : ν
hNe : σ₁ x ≠ σ₂ x
hMem : x ∈ semVars φ
⊢ False
Theorem: LeanSAT.Model.PropFun.agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁✝ σ₂✝ σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
h₁ : σ₁ ⊨ φ
h₂ : ¬σ₂ ⊨ φ
x : ν
hNe : σ₁ x ≠ σ₂ x
hMem : x ∈ semVars φ
⊢ False
Tactic:
exact hNe (h x hMem)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_of_agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂ → eval σ₁ φ = eval σ₂ φ
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ
Theorem: LeanSAT.Model.PropFun.eval_of_agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
have := agreeOn_semVars h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : σ₁ ⊨ φ ↔ σ₂ ⊨ φ
⊢ eval σ₁ φ = eval σ₂ φ
Theorem: LeanSAT.Model.PropFun.eval_of_agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : σ₁ ⊨ φ ↔ σ₂ ⊨ φ
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
dsimp only [SemanticEntails.entails, satisfies] at this
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : eval σ₁ φ = true ↔ eval σ₂ φ = true
⊢ eval σ₁ φ = eval σ₂ φ
Theorem: LeanSAT.Model.PropFun.eval_of_agreeOn_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(semVars φ)) σ₁ σ₂
this : eval σ₁ φ = true ↔ eval σ₂ φ = true
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ semVars (var x) = {x}
Tactic:
ext y
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y ∈ semVars (var x) ↔ y ∈ {x}
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y ∈ semVars (var x) ↔ y ∈ {x}
Tactic:
simp only [Finset.mem_singleton, mem_semVars, satisfies_var]
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) ↔ y = x
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) ↔ y = x
Tactic:
refine ⟨?mp, ?mpr⟩
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y = x → ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x
Tactic:
case mp =>
  intro ⟨τ, hτ, hτ'⟩
  by_contra h
  have := τ.set_get_of_ne (!τ y) h
  exact hτ' (hτ ▸ this)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y = x → ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Tactic:
case mpr =>
  intro h; cases h
  use (fun _ => true)
  simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x
Tactic:
intro ⟨τ, hτ, hτ'⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
⊢ y = x
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
⊢ y = x
Tactic:
by_contra h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
⊢ False
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
⊢ False
Tactic:
have := τ.set_get_of_ne (!τ y) h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
this : PropAssignment.set τ y (!τ y) x = τ x
⊢ False
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
this : PropAssignment.set τ y (!τ y) x = τ x
⊢ False
Tactic:
exact hτ' (hτ ▸ this)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y = x → ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
h : y = x
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
h : y = x
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Tactic:
cases h
Proof state after:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ x (!τ x) x = true
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ x (!τ x) x = true
Tactic:
use (fun _ => true)
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ true = true ∧ ¬PropAssignment.set (fun x => true) x (!true) x = true
Theorem: LeanSAT.Model.PropFun.semVars_var
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ true = true ∧ ¬PropAssignment.set (fun x => true) x (!true) x = true
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_tr
Proof state before:
ν✝ : Sort ?u.572673
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
⊢ semVars ⊤ = ∅
Tactic:
ext
Proof state after:
case a
ν✝ : Sort ?u.572673
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
a✝ : ν
⊢ a✝ ∈ semVars ⊤ ↔ a✝ ∈ ∅
Theorem: LeanSAT.Model.PropFun.semVars_tr
Proof state before:
case a
ν✝ : Sort ?u.572673
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
a✝ : ν
⊢ a✝ ∈ semVars ⊤ ↔ a✝ ∈ ∅
Tactic:
simp [mem_semVars]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_fls
Proof state before:
ν✝ : Sort ?u.573761
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
⊢ semVars ⊥ = ∅
Tactic:
ext
Proof state after:
case a
ν✝ : Sort ?u.573761
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
a✝ : ν
⊢ a✝ ∈ semVars ⊥ ↔ a✝ ∈ ∅
Theorem: LeanSAT.Model.PropFun.semVars_fls
Proof state before:
case a
ν✝ : Sort ?u.573761
inst✝¹ : DecidableEq ν✝
ν : Type u_1
inst✝ : DecidableEq ν
a✝ : ν
⊢ a✝ ∈ semVars ⊥ ↔ a✝ ∈ ∅
Tactic:
simp [mem_semVars]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
⊢ semVars φᶜ = semVars φ
Tactic:
ext x
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φᶜ ↔ x ∈ semVars φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φᶜ ↔ x ∈ semVars φ
Tactic:
simp only [mem_semVars]
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ) ↔ ∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ
Theorem: LeanSAT.Model.PropFun.semVars_neg
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φᶜ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φᶜ) ↔ ∃ τ, τ ⊨ φ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
constructor <;> {
  intro ⟨τ, hτ, hτ'⟩
  simp only [satisfies_neg, not_not] at hτ hτ' ⊢
  let τ' := τ.set x (!τ x)
  have : (!τ' x) = τ x := by
    simp only [τ', τ.set_get x, Bool.not_not]
  refine ⟨τ', hτ', ?_⟩
  rw [τ.set_set, this, τ.set_same]
  exact hτ
}
Proof state after:
no goals