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

State before:
x : BoolExprNat
f : List Bool
a : Nat
⊢ BoolExpr.eval (fun i => decide (i < (literal a).toBoolExpr.vars) && f.getD i false) (literal a).toBoolExpr =
    eval f (literal a)
Tactic:
simp [toBoolExpr]
State after:
no goals

State before:
x : BoolExprNat
f : List Bool
b : Bool
⊢ BoolExpr.eval (fun i => decide (i < (const b).toBoolExpr.vars) && f.getD i false) (const b).toBoolExpr =
    eval f (const b)
Tactic:
rfl
State after:
no goals

State before:
x✝ : BoolExprNat
f : List Bool
x : BoolExprNat
⊢ BoolExpr.eval (fun i => decide (i < x.not.toBoolExpr.vars) && f.getD i false) x.not.toBoolExpr = eval f x.not
Tactic:
simp [toBoolExpr, eval_if]
State after:
no goals

State before:
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ BoolExpr.eval (fun i => decide (i < (gate g x y).toBoolExpr.vars) && f.getD i false) (gate g x y).toBoolExpr =
    eval f (gate g x y)
Tactic:
simp [toBoolExpr]
State after:
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ g.eval (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) x.toBoolExpr)
      (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) y.toBoolExpr) =
    g.eval (eval f x) (eval f y)

State before:
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ g.eval (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) x.toBoolExpr)
      (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) y.toBoolExpr) =
    g.eval (eval f x) (eval f y)
Tactic:
rw [BoolExpr.eval_congr, eval_if f, BoolExpr.eval_congr, eval_if f]
State after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < y.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < y.toBoolExpr.vars) && f.getD i false)

case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < x.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < x.toBoolExpr.vars) && f.getD i false)

State before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < y.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < y.toBoolExpr.vars) && f.getD i false)
Tactic:
intro i h
State after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < y.toBoolExpr.vars) && f.getD i false)

State before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < y.toBoolExpr.vars) && f.getD i false)
Tactic:
simp only [h, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
State after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars

State before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < y.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars
Tactic:
omega
State after:
no goals

State before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < x.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < x.toBoolExpr.vars) && f.getD i false)
Tactic:
intro i h
State after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < x.toBoolExpr.vars) && f.getD i false)

State before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
    (decide (i < x.toBoolExpr.vars) && f.getD i false)
Tactic:
simp only [h, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
State after:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars

State before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars
Tactic:
omega
State after:
no goals