internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_of_disjoint
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ τ' v = τ v
Tactic:
exfalso
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ False
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_of_disjoint
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ False
Tactic:
apply h.ne_of_mem hv hv' rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_compl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ agreeOn (↑xs)ᶜ (setMany τ xs τ') τ
Tactic:
apply agreeOn_setMany_of_disjoint
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ Disjoint (↑xs)ᶜ ↑xs
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_compl
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ Disjoint (↑xs)ᶜ ↑xs
Tactic:
exact disjoint_compl_left
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.map_set
Proof state before:
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ map f (set τ (f v) b) = set (map f τ) v b
Tactic:
unfold map
Proof state after:
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ set τ (f v) b ∘ f = set (τ ∘ f) v b
Theorem: LeanSAT.Model.PropAssignment.map_set
Proof state before:
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ set τ (f v) b ∘ f = set (τ ∘ f) v b
Tactic:
unfold set
Proof state after:
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ (fun y => if y = f v then b else τ y) ∘ f = fun y => if y = v then b else (τ ∘ f) y
Theorem: LeanSAT.Model.PropAssignment.map_set
Proof state before:
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ (fun y => if y = f v then b else τ y) ∘ f = fun y => if y = v then b else (τ ∘ f) y
Tactic:
ext
Proof state after:
case h
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
x✝ : ν₂
⊢ ((fun y => if y = f v then b else τ y) ∘ f) x✝ = if x✝ = v then b else (τ ∘ f) x✝
Theorem: LeanSAT.Model.PropAssignment.map_set
Proof state before:
case h
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
x✝ : ν₂
⊢ ((fun y => if y = f v then b else τ y) ∘ f) x✝ = if x✝ = v then b else (τ ∘ f) x✝
Tactic:
simp [finj.eq_iff]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
⊢ map f τ = map f' τ' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)
Tactic:
simp [map]
Proof state after:
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
⊢ τ ∘ f = τ' ∘ f' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
⊢ τ ∘ f = τ' ∘ f' ↔ ∀ (v : ν), τ (f v) = τ' (f' v)
Tactic:
constructor <;> intro h
Proof state after:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
⊢ ∀ (v : ν), τ (f v) = τ' (f' v)

case mpr
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
⊢ τ ∘ f = τ' ∘ f'
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
⊢ ∀ (v : ν), τ (f v) = τ' (f' v)
Tactic:
intro v
Proof state after:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
⊢ τ (f v) = τ' (f' v)
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
⊢ τ (f v) = τ' (f' v)
Tactic:
have := congrFun h v
Proof state after:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
this : (τ ∘ f) v = (τ' ∘ f') v
⊢ τ (f v) = τ' (f' v)
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
this : (τ ∘ f) v = (τ' ∘ f') v
⊢ τ (f v) = τ' (f' v)
Tactic:
simp_all
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
case mpr
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
⊢ τ ∘ f = τ' ∘ f'
Tactic:
ext v
Proof state after:
case mpr.h
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
v : ν
⊢ (τ ∘ f) v = (τ' ∘ f') v
Theorem: LeanSAT.Model.PropAssignment.map_eq_map
Proof state before:
case mpr.h
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : ∀ (v : ν), τ (f v) = τ' (f' v)
v : ν
⊢ (τ ∘ f) v = (τ' ∘ f') v
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_var
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
⊢ eval τ (var x) = τ x
Tactic:
simp [eval, var]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_tr
Proof state before:
ν : Type u_1
τ : PropAssignment ν
⊢ eval τ tr = true
Tactic:
simp [eval, tr]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_fls
Proof state before:
ν : Type u_1
τ : PropAssignment ν
⊢ eval τ fls = false
Tactic:
simp [eval, fls]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_neg
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ : PropFun ν
⊢ eval τ (neg φ) = !eval τ φ
Tactic:
have ⟨φ, h⟩ := Quotient.exists_rep φ
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ✝ : PropFun ν
φ : PropForm ν
h : ⟦φ⟧ = φ✝
⊢ eval τ (neg φ✝) = !eval τ φ✝
Theorem: LeanSAT.Model.PropFun.eval_neg
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ✝ : PropFun ν
φ : PropForm ν
h : ⟦φ⟧ = φ✝
⊢ eval τ (neg φ✝) = !eval τ φ✝
Tactic:
simp [← h, eval, neg]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_conj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁ φ₂ : PropFun ν
⊢ eval τ (conj φ₁ φ₂) = (eval τ φ₁ && eval τ φ₂)
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (conj φ₁✝ φ₂) = (eval τ φ₁✝ && eval τ φ₂)
Theorem: LeanSAT.Model.PropFun.eval_conj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (conj φ₁✝ φ₂) = (eval τ φ₁✝ && eval τ φ₂)
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (conj φ₁✝ φ₂✝) = (eval τ φ₁✝ && eval τ φ₂✝)
Theorem: LeanSAT.Model.PropFun.eval_conj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (conj φ₁✝ φ₂✝) = (eval τ φ₁✝ && eval τ φ₂✝)
Tactic:
simp [← h₁, ← h₂, conj, eval]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_disj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁ φ₂ : PropFun ν
⊢ eval τ (disj φ₁ φ₂) = (eval τ φ₁ || eval τ φ₂)
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (disj φ₁✝ φ₂) = (eval τ φ₁✝ || eval τ φ₂)
Theorem: LeanSAT.Model.PropFun.eval_disj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (disj φ₁✝ φ₂) = (eval τ φ₁✝ || eval τ φ₂)
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (disj φ₁✝ φ₂✝) = (eval τ φ₁✝ || eval τ φ₂✝)
Theorem: LeanSAT.Model.PropFun.eval_disj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (disj φ₁✝ φ₂✝) = (eval τ φ₁✝ || eval τ φ₂✝)
Tactic:
simp [← h₁, ← h₂, eval, disj]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_impl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁ φ₂ : PropFun ν
⊢ eval τ (impl φ₁ φ₂) = eval τ φ₁ ⇨ eval τ φ₂
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (impl φ₁✝ φ₂) = eval τ φ₁✝ ⇨ eval τ φ₂
Theorem: LeanSAT.Model.PropFun.eval_impl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (impl φ₁✝ φ₂) = eval τ φ₁✝ ⇨ eval τ φ₂
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (impl φ₁✝ φ₂✝) = eval τ φ₁✝ ⇨ eval τ φ₂✝
Theorem: LeanSAT.Model.PropFun.eval_impl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (impl φ₁✝ φ₂✝) = eval τ φ₁✝ ⇨ eval τ φ₂✝
Tactic:
simp [← h₁, ← h₂, eval, impl]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eval_biImpl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁ φ₂ : PropFun ν
⊢ (eval τ (biImpl φ₁ φ₂) = true) = (eval τ φ₁ = eval τ φ₂)
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ (eval τ (biImpl φ₁✝ φ₂) = true) = (eval τ φ₁✝ = eval τ φ₂)
Theorem: LeanSAT.Model.PropFun.eval_biImpl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ (eval τ (biImpl φ₁✝ φ₂) = true) = (eval τ φ₁✝ = eval τ φ₂)
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
Proof state after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (eval τ (biImpl φ₁✝ φ₂✝) = true) = (eval τ φ₁✝ = eval τ φ₂✝)
Theorem: LeanSAT.Model.PropFun.eval_biImpl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (eval τ (biImpl φ₁✝ φ₂✝) = true) = (eval τ φ₁✝ = eval τ φ₂✝)
Tactic:
simp [← h₁, ← h₂, eval, biImpl]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.ext
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ (∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂) → φ₁ = φ₂
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
Proof state after:
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ ↔ τ ⊨ φ₂) → φ₁✝ = φ₂
Theorem: LeanSAT.Model.PropFun.ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ ↔ τ ⊨ φ₂) → φ₁✝ = φ₂
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
Proof state after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ ↔ τ ⊨ φ₂✝) → φ₁✝ = φ₂✝
Theorem: LeanSAT.Model.PropFun.ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ ↔ τ ⊨ φ₂✝) → φ₁✝ = φ₂✝
Tactic:
simp only [← h₁, ← h₂]
Proof state after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧) → ⟦φ₁⟧ = ⟦φ₂⟧
Theorem: LeanSAT.Model.PropFun.ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧) → ⟦φ₁⟧ = ⟦φ₂⟧
Tactic:
intro h
Proof state after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ⟦φ₁⟧ = ⟦φ₂⟧
Theorem: LeanSAT.Model.PropFun.ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ⟦φ₁⟧ = ⟦φ₂⟧
Tactic:
apply Quotient.sound ∘ PropForm.equivalent_ext.mpr
Proof state after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
apply h
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails_ext
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
Proof state after:
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ entails φ₁✝ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.entails_ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ entails φ₁✝ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
Proof state after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ entails φ₁✝ φ₂✝ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂✝
Theorem: LeanSAT.Model.PropFun.entails_ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ entails φ₁✝ φ₂✝ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂✝
Tactic:
simp only [← h₁, ← h₂, entails_mk]
Proof state after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ PropForm.entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ → τ ⊨ ⟦φ₂⟧
Theorem: LeanSAT.Model.PropFun.entails_ext
Proof state before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ PropForm.entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ → τ ⊨ ⟦φ₂⟧
Tactic:
exact PropForm.entails_ext
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails.antisymm
Proof state before:
ν✝ : Type u_1
φ ψ : PropFun ν✝
⊢ entails φ ψ → entails ψ φ → φ = ψ
Tactic:
intro h₁ h₂
Proof state after:
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
⊢ φ = ψ
Theorem: LeanSAT.Model.PropFun.entails.antisymm
Proof state before:
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
⊢ φ = ψ
Tactic:
ext τ
Proof state after:
case a
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
τ : PropAssignment ν✝
⊢ τ ⊨ φ ↔ τ ⊨ ψ
Theorem: LeanSAT.Model.PropFun.entails.antisymm
Proof state before:
case a
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
τ : PropAssignment ν✝
⊢ τ ⊨ φ ↔ τ ⊨ ψ
Tactic:
exact ⟨entails_ext.mp h₁ τ, entails_ext.mp h₂ τ⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails_disj_left
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ φ₁ ≤ eval x✝ (disj φ₁ φ₂)
Tactic:
simp only [eval_disj]
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ φ₁ ≤ (eval x✝ φ₁ || eval x✝ φ₂)
Theorem: LeanSAT.Model.PropFun.entails_disj_left
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ φ₁ ≤ (eval x✝ φ₁ || eval x✝ φ₂)
Tactic:
exact le_sup_left
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails_disj_right
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ φ₂ ≤ eval x✝ (disj φ₁ φ₂)
Tactic:
simp only [eval_disj]
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ φ₂ ≤ (eval x✝ φ₁ || eval x✝ φ₂)
Theorem: LeanSAT.Model.PropFun.entails_disj_right
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ φ₂ ≤ (eval x✝ φ₁ || eval x✝ φ₂)
Tactic:
exact le_sup_right
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.disj_entails
Proof state before:
ν✝ : Type u_1
φ₁ φ₃ φ₂ : PropFun ν✝
h₁ : entails φ₁ φ₃
h₂ : entails φ₂ φ₃
τ : PropAssignment ν✝
⊢ eval τ (disj φ₁ φ₂) ≤ eval τ φ₃
Tactic:
simp only [eval_disj]
Proof state after:
ν✝ : Type u_1
φ₁ φ₃ φ₂ : PropFun ν✝
h₁ : entails φ₁ φ₃
h₂ : entails φ₂ φ₃
τ : PropAssignment ν✝
⊢ (eval τ φ₁ || eval τ φ₂) ≤ eval τ φ₃
Theorem: LeanSAT.Model.PropFun.disj_entails
Proof state before:
ν✝ : Type u_1
φ₁ φ₃ φ₂ : PropFun ν✝
h₁ : entails φ₁ φ₃
h₂ : entails φ₂ φ₃
τ : PropAssignment ν✝
⊢ (eval τ φ₁ || eval τ φ₂) ≤ eval τ φ₃
Tactic:
exact sup_le (h₁ τ) (h₂ τ)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.conj_entails_left
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ (conj φ₁ φ₂) ≤ eval x✝ φ₁
Tactic:
simp only [eval_conj]
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ (eval x✝ φ₁ && eval x✝ φ₂) ≤ eval x✝ φ₁
Theorem: LeanSAT.Model.PropFun.conj_entails_left
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ (eval x✝ φ₁ && eval x✝ φ₂) ≤ eval x✝ φ₁
Tactic:
exact inf_le_left
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.conj_entails_right
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ (conj φ₁ φ₂) ≤ eval x✝ φ₂
Tactic:
simp only [eval_conj]
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ (eval x✝ φ₁ && eval x✝ φ₂) ≤ eval x✝ φ₂
Theorem: LeanSAT.Model.PropFun.conj_entails_right
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ (eval x✝ φ₁ && eval x✝ φ₂) ≤ eval x✝ φ₂
Tactic:
exact inf_le_right
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails_conj
Proof state before:
ν✝ : Type u_1
φ₁ φ₂ φ₃ : PropFun ν✝
h₁ : entails φ₁ φ₂
h₂ : entails φ₁ φ₃
τ : PropAssignment ν✝
⊢ eval τ φ₁ ≤ eval τ (conj φ₂ φ₃)
Tactic:
simp only [eval_conj]
Proof state after:
ν✝ : Type u_1
φ₁ φ₂ φ₃ : PropFun ν✝
h₁ : entails φ₁ φ₂
h₂ : entails φ₁ φ₃
τ : PropAssignment ν✝
⊢ eval τ φ₁ ≤ (eval τ φ₂ && eval τ φ₃)
Theorem: LeanSAT.Model.PropFun.entails_conj
Proof state before:
ν✝ : Type u_1
φ₁ φ₂ φ₃ : PropFun ν✝
h₁ : entails φ₁ φ₂
h₂ : entails φ₁ φ₃
τ : PropAssignment ν✝
⊢ eval τ φ₁ ≤ (eval τ φ₂ && eval τ φ₃)
Tactic:
exact le_inf (h₁ τ) (h₂ τ)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails_disj_conj
Proof state before:
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ (conj (disj φ₁ φ₂) (disj φ₁ φ₃)) ≤ eval x✝ (disj φ₁ (conj φ₂ φ₃))
Tactic:
simp only [eval_conj, eval_disj]
Proof state after:
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ ((eval x✝ φ₁ || eval x✝ φ₂) && (eval x✝ φ₁ || eval x✝ φ₃)) ≤ (eval x✝ φ₁ || eval x✝ φ₂ && eval x✝ φ₃)
Theorem: LeanSAT.Model.PropFun.entails_disj_conj
Proof state before:
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ ((eval x✝ φ₁ || eval x✝ φ₂) && (eval x✝ φ₁ || eval x✝ φ₃)) ≤ (eval x✝ φ₁ || eval x✝ φ₂ && eval x✝ φ₃)
Tactic:
exact le_sup_inf
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.conj_neg_entails_fls
Proof state before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ (conj φ (neg φ)) ≤ eval τ fls
Tactic:
simp only [eval_conj, eval_neg]
Proof state after:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ (eval τ φ && !eval τ φ) ≤ eval τ fls
Theorem: LeanSAT.Model.PropFun.conj_neg_entails_fls
Proof state before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ (eval τ φ && !eval τ φ) ≤ eval τ fls
Tactic:
exact BooleanAlgebra.inf_compl_le_bot (eval τ φ)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.tr_entails_disj_neg
Proof state before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ eval τ (disj φ (neg φ))
Tactic:
simp only [eval_disj, eval_neg]
Proof state after:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ (eval τ φ || !eval τ φ)
Theorem: LeanSAT.Model.PropFun.tr_entails_disj_neg
Proof state before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ (eval τ φ || !eval τ φ)
Tactic:
exact BooleanAlgebra.top_le_sup_compl (eval τ φ)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.impl_eq
Proof state before:
ν : Type u_1
φ ψ : PropFun ν
⊢ impl φ ψ = disj ψ (neg φ)
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ impl φ ψ ↔ τ ⊨ disj ψ (neg φ)
Theorem: LeanSAT.Model.PropFun.impl_eq
Proof state before:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ impl φ ψ ↔ τ ⊨ disj ψ (neg φ)
Tactic:
simp only [sEntails, satisfies, eval_impl, eval_disj, eval_neg]
Proof state after:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ eval τ φ ⇨ eval τ ψ = true ↔ (eval τ ψ || !eval τ φ) = true
Theorem: LeanSAT.Model.PropFun.impl_eq
Proof state before:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ eval τ φ ⇨ eval τ ψ = true ↔ (eval τ ψ || !eval τ φ) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_var
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
⊢ τ ⊨ var x ↔ τ x = true
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_set
Proof state before:
ν : Type u_1
x : ν
τ : PropAssignment ν
inst✝ : DecidableEq ν
⊢ PropAssignment.set τ x ⊤ ⊨ var x
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_tr
Proof state before:
ν : Type u_1
τ : PropAssignment ν
⊢ τ ⊨ ⊤
Tactic:
simp [sEntails, satisfies, Top.top]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_neg
Proof state before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φᶜ ↔ (fun M φ => ¬M ⊨ φ) τ φ
Tactic:
simp [sEntails, satisfies, HasCompl.compl]
Proof state after:
no goals