internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.LitVar.satisfies_map
Proof state before:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ (τ ⊨ if polarity l = true then var (f (toVar l)) else (var (f (toVar l)))ᶜ) ↔
    PropAssignment.map f τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ
Tactic:
split <;> simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.toPropFun_map
Proof state before:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
⊢ toPropFun (map f l) = PropFun.map f (toPropFun l)
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ τ ⊨ toPropFun (map f l) ↔ τ ⊨ PropFun.map f (toPropFun l)
Theorem: LeanSAT.LitVar.toPropFun_map
Proof state before:
case a
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ τ ⊨ toPropFun (map f l) ↔ τ ⊨ PropFun.map f (toPropFun l)
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
C : Clause L
⊢ x ∈ PropFun.semVars (toPropFun C) → ∃ l ∈ C, LitVar.toVar l = x
Tactic:
intro h
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
C : Clause L
h : x ∈ PropFun.semVars (toPropFun C)
⊢ ∃ l ∈ C, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
C : Clause L
h : x ∈ PropFun.semVars (toPropFun C)
⊢ ∃ l ∈ C, LitVar.toVar l = x
Tactic:
rcases C with ⟨data⟩
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Tactic:
have ⟨τ,hpos,hneg⟩ := (PropFun.mem_semVars _ _).mp h
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Tactic:
clear h
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Tactic:
simp_all [toPropFun, Array.mem_def]
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : ∃ a ∈ data, τ ⊨ LitVar.toPropFun a
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
⊢ ∃ l ∈ data, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : ∃ a ∈ data, τ ⊨ LitVar.toPropFun a
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
rcases hpos with ⟨l,hl,h⟩
Proof state after:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
⊢ ∃ l ∈ data, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
have := (PropFun.mem_semVars _ _).mpr ⟨τ,h,hneg l hl⟩
Proof state after:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
clear hneg h
Proof state after:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
l : L
hl : l ∈ data
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x
Theorem: LeanSAT.Clause.mem_semVars_toPropFun
Proof state before:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
l : L
hl : l ∈ data
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Clause.satisfies_iff
Proof state before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ toPropFun C ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Tactic:
rw [toPropFun]
Proof state after:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ any (Multiset.map LitVar.toPropFun ↑(Array.toList C)) ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.satisfies_iff
Proof state before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ any (Multiset.map LitVar.toPropFun ↑(Array.toList C)) ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Tactic:
simp [Array.mem_def]
Proof state after:
no goals
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ toPropFun C = ⊤ ↔ ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂
Tactic:
constructor
Proof state after:
case mp
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ toPropFun C = ⊤ → ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂

case mpr
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ (∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂) → toPropFun C = ⊤
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ toPropFun C = ⊤ → ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂
Tactic:
intro h
Proof state after:
case mp
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
h : toPropFun C = ⊤
⊢ ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
h : toPropFun C = ⊤
⊢ ∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂
Tactic:
rcases C with ⟨lits⟩
Proof state after:
case mp.mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
lits : List L
h : toPropFun { data := lits } = ⊤
⊢ ∃ l₁ ∈ { data := lits }, ∃ l₂ ∈ { data := lits }, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
lits : List L
h : toPropFun { data := lits } = ⊤
⊢ ∃ l₁ ∈ { data := lits }, ∃ l₂ ∈ { data := lits }, l₁ = -l₂
Tactic:
simp_all [toPropFun, Array.mem_def]
Proof state after:
case mp.mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
lits : List L
h : any ↑(List.map (fun x => LitVar.toPropFun x) lits) = ⊤
⊢ ∃ l₁ ∈ lits, ∃ l₂ ∈ lits, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.nil
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
h : any ↑(List.map (fun x => LitVar.toPropFun x) []) = ⊤
⊢ ∃ l₁ ∈ [], ∃ l₂ ∈ [], l₁ = -l₂
Tactic:
rw [ext_iff] at h
Proof state after:
case mp.mk.nil
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
h : ∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) []) ↔ τ ⊨ ⊤
⊢ ∃ l₁ ∈ [], ∃ l₂ ∈ [], l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.nil
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
h : ∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) []) ↔ τ ⊨ ⊤
⊢ ∃ l₁ ∈ [], ∃ l₂ ∈ [], l₁ = -l₂
Tactic:
simp [Array.mem_def] at h
Proof state after:
no goals
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
refine if hr : any _ = ⊤ then have := ih hr; ?_ else ?_
Proof state after:
case mp.mk.cons.refine_1
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
this : ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂

case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : ¬any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_1
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
this : ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
ih : any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤ → ∃ l₁ ∈ tl, ∃ l₂ ∈ tl, l₁ = -l₂
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : ¬any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
clear ih
Proof state after:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : ¬any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) = ⊤
hr : ¬any ↑(List.map (fun x => LitVar.toPropFun x) tl) = ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
rw [PropFun.ext_iff] at hr h
Proof state after:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : ∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) ↔ τ ⊨ ⊤
hr : ¬∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) tl) ↔ τ ⊨ ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : ∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) (hd :: tl)) ↔ τ ⊨ ⊤
hr : ¬∀ (τ : PropAssignment ν), τ ⊨ any ↑(List.map (fun x => LitVar.toPropFun x) tl) ↔ τ ⊨ ⊤
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
simp at hr h
Proof state after:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
hr : ∃ x, ∀ x_1 ∈ tl, ¬x ⊨ LitVar.toPropFun x_1
h : ∀ (τ : PropAssignment ν), τ ⊨ LitVar.toPropFun hd ∨ ∃ a ∈ tl, τ ⊨ LitVar.toPropFun a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
hr : ∃ x, ∀ x_1 ∈ tl, ¬x ⊨ LitVar.toPropFun x_1
h : ∀ (τ : PropAssignment ν), τ ⊨ LitVar.toPropFun hd ∨ ∃ a ∈ tl, τ ⊨ LitVar.toPropFun a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
rcases hr with ⟨τ,hr⟩
Proof state after:
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : ∀ (τ : PropAssignment ν), τ ⊨ LitVar.toPropFun hd ∨ ∃ a ∈ tl, τ ⊨ LitVar.toPropFun a
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
h : ∀ (τ : PropAssignment ν), τ ⊨ LitVar.toPropFun hd ∨ ∃ a ∈ tl, τ ⊨ LitVar.toPropFun a
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
replace h := h (τ.set (LitVar.toVar hd) (!LitVar.polarity hd))
Proof state after:
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
h :
  (PropAssignment.set τ (LitVar.toVar hd) !LitVar.polarity hd) ⊨ LitVar.toPropFun hd ∨
    ∃ a ∈ tl, (PropAssignment.set τ (LitVar.toVar hd) !LitVar.polarity hd) ⊨ LitVar.toPropFun a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
h :
  (PropAssignment.set τ (LitVar.toVar hd) !LitVar.polarity hd) ⊨ LitVar.toPropFun hd ∨
    ∃ a ∈ tl, (PropAssignment.set τ (LitVar.toVar hd) !LitVar.polarity hd) ⊨ LitVar.toPropFun a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
simp [LitVar.satisfies_iff, Bool.not_ne_self] at h
Proof state after:
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
h : ∃ a ∈ tl, PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar a) = LitVar.polarity a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
h : ∃ a ∈ tl, PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar a) = LitVar.polarity a
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
rcases h with ⟨hd',hd'_mem,h⟩
Proof state after:
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
hd' : L
hd'_mem : hd' ∈ tl
h : PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar hd') = LitVar.polarity hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hr : ∀ x ∈ tl, ¬τ ⊨ LitVar.toPropFun x
hd' : L
hd'_mem : hd' ∈ tl
h : PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar hd') = LitVar.polarity hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
replace hr := hr hd' hd'_mem
Proof state after:
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hd' : L
hd'_mem : hd' ∈ tl
h : PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar hd') = LitVar.polarity hd'
hr : ¬τ ⊨ LitVar.toPropFun hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hd' : L
hd'_mem : hd' ∈ tl
h : PropAssignment.set τ (LitVar.toVar hd) (!LitVar.polarity hd) (LitVar.toVar hd') = LitVar.polarity hd'
hr : ¬τ ⊨ LitVar.toPropFun hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
simp [LitVar.satisfies_iff, PropAssignment.set] at hr h
Proof state after:
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hd' : L
hd'_mem : hd' ∈ tl
h : (if LitVar.toVar hd' = LitVar.toVar hd then !LitVar.polarity hd else τ (LitVar.toVar hd')) = LitVar.polarity hd'
hr : ¬τ (LitVar.toVar hd') = LitVar.polarity hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mp.mk.cons.refine_2.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
hd : L
tl : List L
τ : PropAssignment ν
hd' : L
hd'_mem : hd' ∈ tl
h : (if LitVar.toVar hd' = LitVar.toVar hd then !LitVar.polarity hd else τ (LitVar.toVar hd')) = LitVar.polarity hd'
hr : ¬τ (LitVar.toVar hd') = LitVar.polarity hd'
⊢ ∃ l₁ ∈ hd :: tl, ∃ l₂ ∈ hd :: tl, l₁ = -l₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mpr
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
⊢ (∃ l₁ ∈ C, ∃ l₂ ∈ C, l₁ = -l₂) → toPropFun C = ⊤
Tactic:
rintro ⟨_,hl1,l,hl2,rfl⟩
Proof state after:
case mpr.intro.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
⊢ toPropFun C = ⊤
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mpr.intro.intro.intro.intro
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
⊢ toPropFun C = ⊤
Tactic:
ext τ
Proof state after:
case mpr.intro.intro.intro.intro.a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
τ : PropAssignment ν
⊢ τ ⊨ toPropFun C ↔ τ ⊨ ⊤
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mpr.intro.intro.intro.intro.a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
τ : PropAssignment ν
⊢ τ ⊨ toPropFun C ↔ τ ⊨ ⊤
Tactic:
simp [satisfies_iff]
Proof state after:
case mpr.intro.intro.intro.intro.a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
τ : PropAssignment ν
⊢ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.tautology_iff
Proof state before:
case mpr.intro.intro.intro.intro.a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
τ : PropAssignment ν
⊢ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Tactic:
by_cases τ ⊨ LitVar.toPropFun l <;> aesop
Proof state after:
no goals
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
⊢ toPropFun (or c1 c2) = toPropFun c1 ⊔ toPropFun c2
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (or c1 c2) ↔ τ ⊨ toPropFun c1 ⊔ toPropFun c2
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (or c1 c2) ↔ τ ⊨ toPropFun c1 ⊔ toPropFun c2
Tactic:
simp [or, satisfies_iff]
Proof state after:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) ↔
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) ↔
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
apply Iff.intro
Proof state after:
case a.mp
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) →
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

case a.mpr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ ((∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l) →
    ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mp
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) →
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
rintro ⟨l,h1,h2⟩
Proof state after:
case a.mp.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1 ∨ l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l