Theorem: LRAT.Formula.limplies_delete (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
⊢ limplies α f (delete f arr)
Tactic:
intro p
State after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ p ⊨ f → p ⊨ delete f arr

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ p ⊨ f → p ⊨ delete f arr
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
State after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ (∀ (x : β), x ∈ toList f → p ⊨ x) → ∀ (x : β), x ∈ toList (delete f arr) → p ⊨ x

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ (∀ (x : β), x ∈ toList f → p ⊨ x) → ∀ (x : β), x ∈ toList (delete f arr) → p ⊨ x
Tactic:
intro h c c_in_f_del
State after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
⊢ p ⊨ c

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
⊢ p ⊨ c
Tactic:
have del_f_subset := delete_subset f arr
State after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : ∀ (c : β), c ∈ toList (delete f arr) → c ∈ toList f
⊢ p ⊨ c

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : ∀ (c : β), c ∈ toList (delete f arr) → c ∈ toList f
⊢ p ⊨ c
Tactic:
specialize del_f_subset c c_in_f_del
State after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : c ∈ toList f
⊢ p ⊨ c

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : c ∈ toList f
⊢ p ⊨ c
Tactic:
exact h c del_f_subset
State after:
no goals