internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.satisfies_conj
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⊓ φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂
Tactic:
simp [sEntails, satisfies, Inf.inf]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_disj
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⊔ φ₂ ↔ τ ⊨ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp [sEntails, satisfies, Sup.sup]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_impl
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⇨ φ₂ ↔ τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
simp only [sEntails, satisfies, eval_impl, HImp.himp]
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ (max (eval τ φ₂) !eval τ φ₁) = true ↔ eval τ φ₁ = true → eval τ φ₂ = true
Theorem: LeanSAT.Model.PropFun.satisfies_impl
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ (max (eval τ φ₂) !eval τ φ₁) = true ↔ eval τ φ₁ = true → eval τ φ₂ = true
Tactic:
cases (eval τ φ₁) <;> simp [himp_eq]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_impl'
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⇨ φ₂ ↔ (fun M φ => ¬M ⊨ φ) τ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp only [sEntails, satisfies, eval_impl, HImp.himp]
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ (max (eval τ φ₂) !eval τ φ₁) = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true
Theorem: LeanSAT.Model.PropFun.satisfies_impl'
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ (max (eval τ φ₂) !eval τ φ₁) = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true
Tactic:
cases (eval τ φ₁) <;> simp [himp_eq]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_biImpl
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ₁ φ₂ ↔ (τ ⊨ φ₁ ↔ τ ⊨ φ₂)
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eq_top_iff
Proof state before:
ν : Type u_1
φ : PropFun ν
h : φ = ⊤
⊢ ∀ (τ : PropAssignment ν), τ ⊨ φ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eq_top_iff
Proof state before:
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ
⊢ φ = ⊤
Tactic:
ext
Proof state after:
case a
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ
τ✝ : PropAssignment ν
⊢ τ✝ ⊨ φ ↔ τ✝ ⊨ ⊤
Theorem: LeanSAT.Model.PropFun.eq_top_iff
Proof state before:
case a
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ
τ✝ : PropAssignment ν
⊢ τ✝ ⊨ φ ↔ τ✝ ⊨ ⊤
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eq_bot_iff
Proof state before:
ν : Type u_1
φ : PropFun ν
h : φ = ⊥
⊢ ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eq_bot_iff
Proof state before:
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
⊢ φ = ⊥
Tactic:
ext
Proof state after:
case a
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
τ✝ : PropAssignment ν
⊢ τ✝ ⊨ φ ↔ τ✝ ⊨ ⊥
Theorem: LeanSAT.Model.PropFun.eq_bot_iff
Proof state before:
case a
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
τ✝ : PropAssignment ν
⊢ τ✝ ⊨ φ ↔ τ✝ ⊨ ⊥
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.biImpl_eq_impls
Proof state before:
ν : Type u_1
φ ψ : PropFun ν
⊢ biImpl φ ψ = (φ ⇨ ψ) ⊓ (ψ ⇨ φ)
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ψ ↔ τ ⊨ (φ ⇨ ψ) ⊓ (ψ ⇨ φ)
Theorem: LeanSAT.Model.PropFun.biImpl_eq_impls
Proof state before:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ψ ↔ τ ⊨ (φ ⇨ ψ) ⊓ (ψ ⇨ φ)
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.biImpl_top_left
Proof state before:
ν : Type u_1
φ : PropFun ν
⊢ biImpl ⊤ φ = φ
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl ⊤ φ ↔ τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.biImpl_top_left
Proof state before:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl ⊤ φ ↔ τ ⊨ φ
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.biImpl_top_right
Proof state before:
ν : Type u_1
φ : PropFun ν
⊢ biImpl φ ⊤ = φ
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ⊤ ↔ τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.biImpl_top_right
Proof state before:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ⊤ ↔ τ ⊨ φ
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.biImpl_bot_left
Proof state before:
ν : Type u_1
φ : PropFun ν
⊢ biImpl ⊥ φ = φᶜ
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl ⊥ φ ↔ τ ⊨ φᶜ
Theorem: LeanSAT.Model.PropFun.biImpl_bot_left
Proof state before:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl ⊥ φ ↔ τ ⊨ φᶜ
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.biImpl_bot_right
Proof state before:
ν : Type u_1
φ : PropFun ν
⊢ biImpl φ ⊥ = φᶜ
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ⊥ ↔ τ ⊨ φᶜ
Theorem: LeanSAT.Model.PropFun.biImpl_bot_right
Proof state before:
case a
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ⊥ ↔ τ ⊨ φᶜ
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.ne_top_left_of_disj_ne_top
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ φ₁ ⊔ φ₂ ≠ ⊤ → φ₁ ≠ ⊤
Tactic:
intro h
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
h : φ₁ ⊔ φ₂ ≠ ⊤
⊢ φ₁ ≠ ⊤
Theorem: LeanSAT.Model.PropFun.ne_top_left_of_disj_ne_top
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
h : φ₁ ⊔ φ₂ ≠ ⊤
⊢ φ₁ ≠ ⊤
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.ne_top_right_of_disj_ne_top
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ φ₁ ⊔ φ₂ ≠ ⊤ → φ₂ ≠ ⊤
Tactic:
intro h
Proof state after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
h : φ₁ ⊔ φ₂ ≠ ⊤
⊢ φ₂ ≠ ⊤
Theorem: LeanSAT.Model.PropFun.ne_top_right_of_disj_ne_top
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
h : φ₁ ⊔ φ₂ ≠ ⊤
⊢ φ₂ ≠ ⊤
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.var.inj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
⊢ Function.Injective var
Tactic:
intro v1 v2 h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = var v2
⊢ v1 = v2
Theorem: LeanSAT.Model.PropFun.var.inj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = var v2
⊢ v1 = v2
Tactic:
rw [ext_iff] at h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
⊢ v1 = v2
Theorem: LeanSAT.Model.PropFun.var.inj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
⊢ v1 = v2
Tactic:
have := h (fun v => v = v1)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
this : (fun v => decide (v = v1)) ⊨ var v1 ↔ (fun v => decide (v = v1)) ⊨ var v2
⊢ v1 = v2
Theorem: LeanSAT.Model.PropFun.var.inj
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ var v2
this : (fun v => decide (v = v1)) ⊨ var v1 ↔ (fun v => decide (v = v1)) ⊨ var v2
⊢ v1 = v2
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.var_eq_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' ↔ v = v'
Tactic:
constructor
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' → v = v'

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ v = v' → var v = var v'
Theorem: LeanSAT.Model.PropFun.var_eq_var
Proof state before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ var v = var v' → v = v'
Tactic:
intro
Proof state after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ v = v'
Theorem: LeanSAT.Model.PropFun.var_eq_var
Proof state before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ v = v'
Tactic:
apply var.inj
Proof state after:
case mp.a
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ var v = var v'
Theorem: LeanSAT.Model.PropFun.var_eq_var
Proof state before:
case mp.a
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
a✝ : var v = var v'
⊢ var v = var v'
Tactic:
assumption
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.var_eq_var
Proof state before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
v v' : ν
⊢ v = v' → var v = var v'
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eq_compl_iff_neq
Proof state before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ φ₁ = φ₂ᶜ → φ₁ ≠ φ₂
Tactic:
rintro rfl h
Proof state after:
ν : Type u_1
φ₂ : PropFun ν
h : φ₂ᶜ = φ₂
⊢ False
Theorem: LeanSAT.Model.PropFun.eq_compl_iff_neq
Proof state before:
ν : Type u_1
φ₂ : PropFun ν
h : φ₂ᶜ = φ₂
⊢ False
Tactic:
rw [ext_iff] at h
Proof state after:
ν : Type u_1
φ₂ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ₂ᶜ ↔ τ ⊨ φ₂
⊢ False
Theorem: LeanSAT.Model.PropFun.eq_compl_iff_neq
Proof state before:
ν : Type u_1
φ₂ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ₂ᶜ ↔ τ ⊨ φ₂
⊢ False
Tactic:
simp at h
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.var_ne_var_compl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
⊢ var v1 ≠ (var v2)ᶜ
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = (var v2)ᶜ
⊢ False
Theorem: LeanSAT.Model.PropFun.var_ne_var_compl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = (var v2)ᶜ
⊢ False
Tactic:
rw [ext_iff] at h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
⊢ False
Theorem: LeanSAT.Model.PropFun.var_ne_var_compl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
⊢ False
Tactic:
have := h (fun v => v = v1 || v = v2)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v1 ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v2)ᶜ
⊢ False
Theorem: LeanSAT.Model.PropFun.var_ne_var_compl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v1 ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v2)ᶜ
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.var_compl_ne_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
⊢ (var v1)ᶜ ≠ var v2
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : (var v1)ᶜ = var v2
⊢ False
Theorem: LeanSAT.Model.PropFun.var_compl_ne_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : (var v1)ᶜ = var v2
⊢ False
Tactic:
rw [ext_iff] at h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ (var v1)ᶜ ↔ τ ⊨ var v2
⊢ False
Theorem: LeanSAT.Model.PropFun.var_compl_ne_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ (var v1)ᶜ ↔ τ ⊨ var v2
⊢ False
Tactic:
have := h (fun v => v = v1 || v = v2)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ (var v1)ᶜ ↔ τ ⊨ var v2
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v1)ᶜ ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v2
⊢ False
Theorem: LeanSAT.Model.PropFun.var_compl_ne_var
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ (var v1)ᶜ ↔ τ ⊨ var v2
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v1)ᶜ ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v2
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_all
Proof state before:
ν : Type u_1
a : Multiset (PropFun ν)
τ : PropAssignment ν
⊢ τ ⊨ all a ↔ ∀ i ∈ a, τ ⊨ i
Tactic:
induction a using Multiset.induction with
| empty => simp [all]
| cons => simp_all [all]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_all
Proof state before:
case empty
ν : Type u_1
τ : PropAssignment ν
⊢ τ ⊨ all 0 ↔ ∀ i ∈ 0, τ ⊨ i
Tactic:
simp [all]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_all
Proof state before:
case cons
ν : Type u_1
τ : PropAssignment ν
a✝¹ : PropFun ν
s✝ : Multiset (PropFun ν)
a✝ : τ ⊨ all s✝ ↔ ∀ i ∈ s✝, τ ⊨ i
⊢ τ ⊨ all (a✝¹ ::ₘ s✝) ↔ ∀ i ∈ a✝¹ ::ₘ s✝, τ ⊨ i
Tactic:
simp_all [all]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_any
Proof state before:
ν : Type u_1
a : Multiset (PropFun ν)
τ : PropAssignment ν
⊢ τ ⊨ any a ↔ ∃ i ∈ a, τ ⊨ i
Tactic:
induction a using Multiset.induction with
| empty => simp [any]
| cons => simp_all [any]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_any
Proof state before:
case empty
ν : Type u_1
τ : PropAssignment ν
⊢ τ ⊨ any 0 ↔ ∃ i ∈ 0, τ ⊨ i
Tactic:
simp [any]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_any
Proof state before:
case cons
ν : Type u_1
τ : PropAssignment ν
a✝¹ : PropFun ν
s✝ : Multiset (PropFun ν)
a✝ : τ ⊨ any s✝ ↔ ∃ i ∈ s✝, τ ⊨ i
⊢ τ ⊨ any (a✝¹ ::ₘ s✝) ↔ ∃ i ∈ a✝¹ ::ₘ s✝, τ ⊨ i
Tactic:
simp_all [any]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.not_satisfiable_iff_eq_bot
Proof state before:
ν : Type u_1
F : PropFun ν
⊢ ¬satisfiable F ↔ F = ⊥
Tactic:
simp [satisfiable]
Proof state after:
ν : Type u_1
F : PropFun ν
⊢ (∀ (x : PropAssignment ν), ¬x ⊨ F) ↔ F = ⊥
Theorem: LeanSAT.Model.PropFun.not_satisfiable_iff_eq_bot
Proof state before:
ν : Type u_1
F : PropFun ν
⊢ (∀ (x : PropAssignment ν), ¬x ⊨ F) ↔ F = ⊥
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eq_bot_of_eqsat
Proof state before:
ν : Type u_1
F C : PropFun ν
⊢ eqsat F (F ⊓ C) → F ⊓ C = ⊥ → F = ⊥
Tactic:
rintro ⟨h₁, _⟩ hFC
Proof state after:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable (F ⊓ C)
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
Theorem: LeanSAT.Model.PropFun.eq_bot_of_eqsat
Proof state before:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable (F ⊓ C)
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
Tactic:
rw [hFC] at h₁
Proof state after:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
Theorem: LeanSAT.Model.PropFun.eq_bot_of_eqsat
Proof state before:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
Tactic:
have := mt h₁ bot_not_satisfiable
Proof state after:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
this : ¬satisfiable F
⊢ F = ⊥
Theorem: LeanSAT.Model.PropFun.eq_bot_of_eqsat
Proof state before:
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
this : ¬satisfiable F
⊢ F = ⊥
Tactic:
exact not_satisfiable_iff_eq_bot.mp (mt h₁ bot_not_satisfiable)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.eqsat_of_entails
Proof state before:
ν : Type u_1
F C : PropFun ν
⊢ F ≤ C → eqsat F (F ⊓ C)
Tactic:
intro h_entails
Proof state after:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ eqsat F (F ⊓ C)
Theorem: LeanSAT.Model.PropFun.eqsat_of_entails
Proof state before:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ eqsat F (F ⊓ C)
Tactic:
simp only [eqsat, satisfiable, ge_iff_le, satisfies_conj]
Proof state after:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ (∃ τ, τ ⊨ F) ↔ ∃ τ, τ ⊨ F ∧ τ ⊨ C
Theorem: LeanSAT.Model.PropFun.eqsat_of_entails
Proof state before:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ (∃ τ, τ ⊨ F) ↔ ∃ τ, τ ⊨ F ∧ τ ⊨ C
Tactic:
exact ⟨fun ⟨τ, hτ⟩ => ⟨τ, hτ, h_entails τ hτ⟩, fun ⟨τ, hτ, _⟩ => ⟨τ, hτ⟩⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_ofBool
Proof state before:
ν✝ : Type u_1
τ : PropAssignment ν✝
b : Bool
⊢ eval τ (ofBool b) = b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun p L hc) = p τ
Tactic:
unfold ofFun
Proof state after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun.aux p L fun v h => ⋯.elim) = p τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun.aux p L fun v h => ⋯.elim) = p τ
Tactic:
suffices ∀ {rem passn},
  (∀ v h, passn v h = τ v ) →
  eval τ (ofFun.aux p rem passn) = p τ
  from this (fun v h => by have := h (hc v); contradiction)
Proof state after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
Tactic:
intro rem passn ht
Proof state after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
rem : List V
passn : (v : V) → v ∉ rem → Bool
ht : ∀ (v : V) (h : v ∉ rem), passn v h = τ v
⊢ eval τ (ofFun.aux p rem passn) = p τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
rem : List V
passn : (v : V) → v ∉ rem → Bool
ht : ∀ (v : V) (h : v ∉ rem), passn v h = τ v
⊢ eval τ (ofFun.aux p rem passn) = p τ
Tactic:
induction rem with
| nil => simp [ofFun.aux]; congr; funext v; simp [*]
| cons head tail ih =>
  simp
  cases hhead : τ head <;> (simp; apply ih; intro v h; split <;> simp [*])
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this :
  ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
v : V
h : v ∉ L
⊢ (fun v h => ⋯.elim) v h = τ v
Tactic:
have := h (hc v)
Proof state after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this✝ :
  ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
v : V
h : v ∉ L
this : False
⊢ (fun v h => ⋯.elim) v h = τ v
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this✝ :
  ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
v : V
h : v ∉ L
this : False
⊢ (fun v h => ⋯.elim) v h = τ v
Tactic:
contradiction
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case nil
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ eval τ (ofFun.aux p [] passn) = p τ
Tactic:
simp [ofFun.aux]
Proof state after:
case nil
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (p fun v => passn v ⋯) = p τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case nil
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (p fun v => passn v ⋯) = p τ
Tactic:
congr
Proof state after:
case nil.e_a
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (fun v => passn v ⋯) = τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case nil.e_a
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (fun v => passn v ⋯) = τ
Tactic:
funext v
Proof state after:
case nil.e_a.h
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
v : V
⊢ passn v ⋯ = τ v
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case nil.e_a.h
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
v : V
⊢ passn v ⋯ = τ v
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case cons
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
⊢ eval τ (ofFun.aux p (head :: tail) passn) = p τ
Tactic:
simp
Proof state after:
case cons
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
⊢ (τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) ||
      !τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then false else passn v' ⋯)) =
    p τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case cons
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
⊢ (τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) ||
      !τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then false else passn v' ⋯)) =
    p τ
Tactic:
cases hhead : τ head <;> (simp; apply ih; intro v h; split <;> simp [*])
Proof state after:
no goals