internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
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
Tactic:
cases h1
Proof state after:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
refine Or.inl ⟨l,?_⟩
Proof state after:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ l ∈ c1 ∧ τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ l ∈ c1 ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
refine Or.inr ⟨l,?_⟩
Proof state after:
case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ l ∈ c2 ∧ τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ l ∈ c2 ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
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
Tactic:
rintro (⟨l,h1,h2⟩|⟨l,h1,h2⟩)
Proof state after:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l

case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
refine ⟨l,?_⟩
Proof state after:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
refine ⟨l,?_⟩
Proof state after:
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Theorem: LeanSAT.Clause.toPropFun_or
Proof state before:
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Clause.toPropFun_map
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
⊢ toPropFun (map L' f c) = PropFun.map f (toPropFun c)
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
τ : PropAssignment ν'
⊢ τ ⊨ toPropFun (map L' f c) ↔ τ ⊨ PropFun.map f (toPropFun c)
Theorem: LeanSAT.Clause.toPropFun_map
Proof state before:
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
τ : PropAssignment ν'
⊢ τ ⊨ toPropFun (map L' f c) ↔ τ ⊨ PropFun.map f (toPropFun c)
Tactic:
simp [map, satisfies_iff]
Proof state after:
no goals
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : Cnf L
⊢ v ∈ PropFun.semVars (toPropFun F) → ∃ C ∈ F, ∃ l ∈ C, LitVar.toVar l = v
Tactic:
rcases F with ⟨F⟩
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : List (Clause L)
⊢ v ∈ PropFun.semVars (toPropFun { data := F }) → ∃ C ∈ { data := F }, ∃ l ∈ C, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : List (Clause L)
⊢ v ∈ PropFun.semVars (toPropFun { data := F }) → ∃ C ∈ { data := F }, ∃ l ∈ C, LitVar.toVar l = v
Tactic:
simp [toPropFun, Array.mem_def, PropFun.all]
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : List (Clause L)
⊢ v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun F)) →
    ∃ C ∈ F, ∃ l ∈ C.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : List (Clause L)
⊢ v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun F)) →
    ∃ C ∈ F, ∃ l ∈ C.data, LitVar.toVar l = v
Tactic:
induction F <;> simp
Proof state after:
case mk.cons
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, ∃ l ∈ C.data, LitVar.toVar l = v
⊢ v ∈ PropFun.semVars (Clause.toPropFun head✝ ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    (∃ l ∈ head✝.data, LitVar.toVar l = v) ∨ ∃ a ∈ tail✝, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
⊢ v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
intro hv
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
have := PropFun.semVars_conj _ _ hv
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this :
  v ∈
    PropFun.semVars (Clause.toPropFun hd) ∪
      PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this :
  v ∈
    PropFun.semVars (Clause.toPropFun hd) ∪
      PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
simp at this
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this :
  v ∈ PropFun.semVars (Clause.toPropFun hd) ∨
    v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this :
  v ∈ PropFun.semVars (Clause.toPropFun hd) ∨
    v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
rcases this with (h|h)
Proof state after:
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v

case inr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
have := Clause.mem_semVars_toPropFun _ _ h
Proof state after:
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
this : ∃ l ∈ hd, LitVar.toVar l = v
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
this : ∃ l ∈ hd, LitVar.toVar l = v
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
simp [Array.mem_def] at this
Proof state after:
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
this : ∃ l ∈ hd.data, LitVar.toVar l = v
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
this : ∃ l ∈ hd.data, LitVar.toVar l = v
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case inr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
have := ih h
Proof state after:
case inr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this : ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Theorem: LeanSAT.Cnf.semVars_toPropFun
Proof state before:
case inr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this : ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
Tactic:
simp_all [Array.mem_def]
Proof state after:
no goals
Theorem: LeanSAT.Cnf.mem_semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
F : Cnf L
⊢ x ∈ PropFun.semVars (toPropFun F) → ∃ C ∈ F, x ∈ PropFun.semVars (Clause.toPropFun C)
Tactic:
intro h
Proof state after:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
F : Cnf L
h : x ∈ PropFun.semVars (toPropFun F)
⊢ ∃ C ∈ F, x ∈ PropFun.semVars (Clause.toPropFun C)
Theorem: LeanSAT.Cnf.mem_semVars_toPropFun
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
F : Cnf L
h : x ∈ PropFun.semVars (toPropFun F)
⊢ ∃ C ∈ F, x ∈ PropFun.semVars (Clause.toPropFun C)
Tactic:
rcases F with ⟨data⟩
Proof state after:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ { data := data }, x ∈ PropFun.semVars (Clause.toPropFun C)
Theorem: LeanSAT.Cnf.mem_semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ { data := data }, x ∈ PropFun.semVars (Clause.toPropFun C)
Tactic:
simp [Array.mem_def]
Proof state after:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ data, x ∈ PropFun.semVars (Clause.toPropFun C)
Theorem: LeanSAT.Cnf.mem_semVars_toPropFun
Proof state before:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ data, x ∈ PropFun.semVars (Clause.toPropFun C)
Tactic:
induction data <;> simp_all [toPropFun, PropFun.all]
Proof state after:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h : x ∈ PropFun.semVars (Clause.toPropFun head✝ ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)
Theorem: LeanSAT.Cnf.mem_semVars_toPropFun
Proof state before:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h : x ∈ PropFun.semVars (Clause.toPropFun head✝ ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)
Tactic:
replace h := PropFun.semVars_conj _ _ h
Proof state after:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h :
  x ∈
    PropFun.semVars (Clause.toPropFun head✝) ∪
      PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)
Theorem: LeanSAT.Cnf.mem_semVars_toPropFun
Proof state before:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h :
  x ∈
    PropFun.semVars (Clause.toPropFun head✝) ∪
      PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Cnf.satisfies_iff
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ toPropFun φ ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C
Tactic:
rw [toPropFun]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ all ↑(List.map Clause.toPropFun φ.data) ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C
Theorem: LeanSAT.Cnf.satisfies_iff
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ all ↑(List.map Clause.toPropFun φ.data) ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C
Tactic:
rcases φ with ⟨φ⟩
Proof state after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : List (Clause L)
⊢ τ ⊨ all ↑(List.map Clause.toPropFun { data := φ }.data) ↔ ∀ C ∈ { data := φ }, τ ⊨ Clause.toPropFun C
Theorem: LeanSAT.Cnf.satisfies_iff
Proof state before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : List (Clause L)
⊢ τ ⊨ all ↑(List.map Clause.toPropFun { data := φ }.data) ↔ ∀ C ∈ { data := φ }, τ ⊨ Clause.toPropFun C
Tactic:
induction φ <;> simp_all [Array.mem_def]
Proof state after:
no goals
Theorem: LeanSAT.Cnf.toPropFun_addClause
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
⊢ toPropFun (addClause C f) = toPropFun f ⊓ Clause.toPropFun C
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (addClause C f) ↔ τ ⊨ toPropFun f ⊓ Clause.toPropFun C
Theorem: LeanSAT.Cnf.toPropFun_addClause
Proof state before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (addClause C f) ↔ τ ⊨ toPropFun f ⊓ Clause.toPropFun C
Tactic:
simp [satisfies_iff, Array.mem_def, addClause]
Proof state after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
τ : PropAssignment ν
⊢ (∀ (C_1 : Clause L), C_1 ∈ f.data ∨ C_1 = C → τ ⊨ Clause.toPropFun C_1) ↔
    (∀ C ∈ f.data, τ ⊨ Clause.toPropFun C) ∧ τ ⊨ Clause.toPropFun C