Theorem: LeanSAT.Cnf.semVars_toPropFun (LeanSAT/Data/Cnf.lean)

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

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

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

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

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

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

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

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

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

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

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

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