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

State before:
α : Type
f g : α → Bool
x : CNF α
w : ∀ (i : α), mem i x → f i = g i
⊢ eval f x = eval g x
Tactic:
induction x
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✝ : Clause α
tail✝ : List (Clause α)
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
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ eval f (c :: x) = eval g (c :: x)
Tactic:
simp only [eval_succ]
State after:
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ (Clause.eval f c && eval f x) = (Clause.eval g c && eval g x)

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

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

State before:
case a
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
i : α
h : mem i x
⊢ mem i (c :: x)
Tactic:
simp [h]
State after:
no goals