Theorem: BoolExpr.eval_congr (LeanSAT/Reflect/BoolExpr/Decidable.lean)

State before:
x : BoolExpr Nat
f g : Nat → Bool
w : ∀ (i : Nat), i < x.vars → f i = g i
⊢ eval f x = eval g x
Tactic:
match x with
| .literal i => dsimp [eval]; apply w; simp
| .const b => rfl
| .not x =>
  dsimp [eval]
  rw [eval_congr f g]
  exact w
| .gate h x y =>
  dsimp [eval]
  rw [eval_congr f g, eval_congr f g]
  exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_right _ _))
  exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_left _ _))
State after:
no goals

State before:
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ eval f (literal i) = eval g (literal i)
Tactic:
dsimp [eval]
State after:
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ f i = g i

State before:
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ f i = g i
Tactic:
apply w
State after:
case a
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ i < (literal i).vars

State before:
case a
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ i < (literal i).vars
Tactic:
simp
State after:
no goals

State before:
x : BoolExpr Nat
f g : Nat → Bool
b : Bool
w : ∀ (i : Nat), i < (const b).vars → f i = g i
⊢ eval f (const b) = eval g (const b)
Tactic:
rfl
State after:
no goals

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ eval f x.not = eval g x.not
Tactic:
dsimp [eval]
State after:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ (!eval f x) = !eval g x

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ (!eval f x) = !eval g x
Tactic:
rw [eval_congr f g]
State after:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Tactic:
exact w
State after:
no goals

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ eval f (gate h x y) = eval g (gate h x y)
Tactic:
dsimp [eval]
State after:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ h.eval (eval f x) (eval f y) = h.eval (eval g x) (eval g y)

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ h.eval (eval f x) (eval f y) = h.eval (eval g x) (eval g y)
Tactic:
rw [eval_congr f g, eval_congr f g]
State after:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < y.vars → f i = g i

x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < y.vars → f i = g i

x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Tactic:
exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_right _ _))
State after:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i

State before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Tactic:
exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_left _ _))
State after:
no goals