Theorem: LeanSAT.Clause.tautology_iff (LeanSAT/Data/Cnf.lean)

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
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 = ⊤

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
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₂

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⟩
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₂

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]
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₂

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
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₂

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
State after:
no goals

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 ?_
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₂

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
State after:
no goals

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
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₂

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
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₂

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
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₂

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⟩
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₂

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))
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₂

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
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₂

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⟩
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₂

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
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₂

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
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₂

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
State after:
no goals

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⟩
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 = ⊤

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 τ
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 ↔ τ ⊨ ⊤

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]
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

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
State after:
no goals