Theorem: BoolExprNat.eval_toBoolExpr (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
x : BoolExprNat
f : List Bool
⊢ BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
Tactic:
induction x with
| literal a => rfl
| const b => rfl
| not x ih => simp [eval, ih, toBoolExpr]
| gate g x y ihx ihy => simp [eval, ihx, ihy, toBoolExpr]
State after:
no goals

State before:
case literal
f : List Bool
a : Nat
⊢ BoolExpr.eval (fun x => f.getD x false) (literal a).toBoolExpr = eval f (literal a)
Tactic:
rfl
State after:
no goals

State before:
case const
f : List Bool
b : Bool
⊢ BoolExpr.eval (fun x => f.getD x false) (const b).toBoolExpr = eval f (const b)
Tactic:
rfl
State after:
no goals

State before:
case not
f : List Bool
x : BoolExprNat
ih : BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
⊢ BoolExpr.eval (fun x => f.getD x false) x.not.toBoolExpr = eval f x.not
Tactic:
simp [eval, ih, toBoolExpr]
State after:
no goals

State before:
case gate
f : List Bool
g : Gate
x y : BoolExprNat
ihx : BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
ihy : BoolExpr.eval (fun x => f.getD x false) y.toBoolExpr = eval f y
⊢ BoolExpr.eval (fun x => f.getD x false) (gate g x y).toBoolExpr = eval f (gate g x y)
Tactic:
simp [eval, ihx, ihy, toBoolExpr]
State after:
no goals