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

State before:
k : Nat
x : BoolExprNat
f : Fin k → Bool
⊢ eval (List.ofFn f) x = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) x.toBoolExpr
Tactic:
match x with
| literal a => simp [toBoolExpr, List.getD_ofFn]
| const b => rfl
| not x => simp [eval, toBoolExpr, eval_ofFn]
| gate g x y => simp [eval, toBoolExpr, eval_ofFn]
State after:
no goals

State before:
k : Nat
x : BoolExprNat
f : Fin k → Bool
a : Nat
⊢ eval (List.ofFn f) (literal a) = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) (literal a).toBoolExpr
Tactic:
simp [toBoolExpr, List.getD_ofFn]
State after:
no goals

State before:
k : Nat
x : BoolExprNat
f : Fin k → Bool
b : Bool
⊢ eval (List.ofFn f) (const b) = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) (const b).toBoolExpr
Tactic:
rfl
State after:
no goals

State before:
k : Nat
x✝ : BoolExprNat
f : Fin k → Bool
x : BoolExprNat
⊢ eval (List.ofFn f) x.not = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) x.not.toBoolExpr
Tactic:
simp [eval, toBoolExpr, eval_ofFn]
State after:
no goals

State before:
k : Nat
x✝ : BoolExprNat
f : Fin k → Bool
g : Gate
x y : BoolExprNat
⊢ eval (List.ofFn f) (gate g x y) =
    BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) (gate g x y).toBoolExpr
Tactic:
simp [eval, toBoolExpr, eval_ofFn]
State after:
no goals