Theorem: CNF.Clause.eval_congr (LeanSAT/Reflect/CNF/Basic.lean)

State before:
α : Type
f g : α → Bool
c : Clause α
w : ∀ (i : α), mem i c → f i = g i
⊢ eval f c = eval g c
Tactic:
induction c
State after:
case nil
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []

case cons
α : Type
f g : α → Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
tail_ih✝ : (∀ (i : α), mem i tail✝ → f i = g i) → eval f tail✝ = eval g tail✝
w : ∀ (i : α), mem i (head✝ :: tail✝) → f i = g i
⊢ eval f (head✝ :: tail✝) = eval g (head✝ :: tail✝)

State before:
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []
Tactic:
rfl
State after:
no goals

State before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ eval f (i :: c) = eval g (i :: c)
Tactic:
simp only [eval_succ]
State after:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ (f i.fst == i.snd || eval f c) = (g i.fst == i.snd || eval g c)

State before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ (f i.fst == i.snd || eval f c) = (g i.fst == i.snd || eval g c)
Tactic:
rw [ih, w]
State after:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ mem i.fst (i :: c)

α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ ∀ (i : α), mem i c → f i = g i

State before:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ mem i.fst (i :: c)
Tactic:
rcases i with ⟨b, (_|_)⟩ <;> simp [mem]
State after:
no goals

State before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ ∀ (i : α), mem i c → f i = g i
Tactic:
intro j h
State after:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ f j = g j

State before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ f j = g j
Tactic:
apply w
State after:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ mem j (i :: c)

State before:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ mem j (i :: c)
Tactic:
rcases h with h | h
State after:
case a.inl
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ mem j (i :: c)

case a.inr
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ mem j (i :: c)

State before:
case a.inl
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ mem j (i :: c)
Tactic:
left
State after:
case a.inl.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ (j, false) ∈ i :: c

State before:
case a.inl.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ (j, false) ∈ i :: c
Tactic:
apply List.mem_cons_of_mem _ h
State after:
no goals

State before:
case a.inr
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ mem j (i :: c)
Tactic:
right
State after:
case a.inr.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ (j, true) ∈ i :: c

State before:
case a.inr.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ (j, true) ∈ i :: c
Tactic:
apply List.mem_cons_of_mem _ h
State after:
no goals