perf: improve bv_decide performance with large literals (#6453)

This PR improves bv_decide's performance in the presence of large
literals.

The core change of this PR is the reformulation of the reflection code
for literals to:
```diff
 def eval (assign : Assignment) : BVExpr w → BitVec w
   | .var idx =>
-    let ⟨bv⟩ := assign.get idx
-    bv.truncate w
+    let packedBv := assign.get idx
+    /-
+    This formulation improves performance, as in a well formed expression the condition always holds
+    so there is no need for the more involved `BitVec.truncate` logic.
+    -/
+    if h : packedBv.w = w then
+      h ▸ packedBv.bv
+    else
+      packedBv.bv.truncate w
```
The remainder is merely further simplifications that make the terms
smaller and easier to deal with in general. This change is motivated by
applying the following diff to the kernel:
```diff
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b0e6844dca..f13bb96bd4 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -518,6 +518,7 @@ optional<constant_info> type_checker::is_delta(expr const & e) const {
 optional<expr> type_checker::unfold_definition_core(expr const & e) {
     if (is_constant(e)) {
         if (auto d = is_delta(e)) {
+//            std::cout << "Working on unfolding: " << d->get_name() << std::endl;
             if (length(const_levels(e)) == d->get_num_lparams()) {
                 if (m_diag) {
                     m_diag->record_unfold(d->get_name());
```
and observing that in the test case from #6043 we see a long series of
```
Working on unfolding: Bool.decEq
Working on unfolding: Bool.decEq.match_1
Working on unfolding: Bool.casesOn
Working on unfolding: Nat.ble
Working on unfolding: Nat.brecOn
Working on unfolding: Nat.beq.match_1
Working on unfolding: Nat.casesOn
Working on unfolding: Nat.casesOn
Working on unfolding: Nat.beq.match_1
Working on unfolding: Nat.casesOn
Working on unfolding: Nat.casesOn
```
the chain begins with `BitVec.truncate`, works through a few
abstractions and then continues like above forever, so I avoid the call
to truncate like this. It is not quite clear to me why removing `ofBool`
helps so much here, maybe some other kernel heuristic kicks in to rescue
us.

Either way this diff is a general improvement for reflection of `BitVec`
constants as we should never have to run `BitVec.truncate` again!

Fixes: #6043

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -82,7 +82,7 @@ instance : ToExpr Gate where
     | .and => mkConst ``Gate.and
     | .xor => mkConst ``Gate.xor
     | .beq => mkConst ``Gate.beq
-    | .imp => mkConst ``Gate.imp
+    | .or => mkConst ``Gate.or
   toTypeExpr := mkConst ``Gate
 
 instance : ToExpr BVPred where

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -91,7 +91,7 @@ where
     | .and => ``Std.Tactic.BVDecide.Reflect.Bool.and_congr
     | .xor => ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr
     | .beq => ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr
-    | .imp => ``Std.Tactic.BVDecide.Reflect.Bool.imp_congr
+    | .or => ``Std.Tactic.BVDecide.Reflect.Bool.or_congr
 
 /--
 Construct the reified version of `Bool.not subExpr`.
@@ -136,7 +136,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
         lhsEvalExpr lhsProof?
         rhsEvalExpr rhsProof? | return none
     return mkApp9
-      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
+      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.cond_congr)
       discrExpr lhsExpr rhsExpr
       discrEvalExpr lhsEvalExpr rhsEvalExpr
       discrProof lhsProof rhsProof

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean

@@ -22,67 +22,70 @@ This function adds the two lemmas:
 - `discrExpr = false → atomExpr = rhsExpr`
 It assumes that `discrExpr`, `lhsExpr` and `rhsExpr` are the expressions corresponding to `discr`,
 `lhs` and `rhs`. Furthermore it assumes that `atomExpr` is of the form
-`if discrExpr = true then lhsExpr else rhsExpr`.
+`bif discrExpr then lhsExpr else rhsExpr`.
 -/
-def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+def addCondLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
     (discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
-  let some trueLemma ← mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some trueLemma ← mkCondTrueLemma discr atom lhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma trueLemma
-  let some falseLemma ← mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  let some falseLemma ← mkCondFalseLemma discr atom rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
   LemmaM.addLemma falseLemma
 where
-  mkIfTrueLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
-      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
-    mkIfLemma true discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
+  mkCondTrueLemma (discr : ReifiedBVLogical) (atom lhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
+    let resExpr := lhsExpr
+    let resValExpr := lhs
+    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
 
-  mkIfFalseLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
-      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
-    mkIfLemma false discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
 
-  mkIfLemma (discrVal : Bool) (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
-      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
-    let resExpr := if discrVal then lhsExpr else rhsExpr
-    let resValExpr := if discrVal then lhs else rhs
-    let lemmaName :=
-      if discrVal then
-        ``Std.Tactic.BVDecide.Reflect.BitVec.if_true
-      else
-        ``Std.Tactic.BVDecide.Reflect.BitVec.if_false
-    let discrValExpr := toExpr discrVal
-    let discrVal ← ReifiedBVLogical.mkBoolConst discrVal
-
-    let eqDiscrExpr ← mkAppM ``BEq.beq #[discrExpr, discrValExpr]
-    let eqDiscr ← ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
+    let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
+    let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr
 
     let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
-    let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
+    let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
       let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
 
-      let trueExpr := mkConst ``Bool.true
-      let eqDiscrTrueExpr ← mkEq eqDiscrExpr trueExpr
-      let eqBVExprTrueExpr ← mkEq eqBVExpr trueExpr
-      let impExpr ← mkArrow eqDiscrTrueExpr eqBVExprTrueExpr
-      -- construct a `Decidable` instance for the implication using forall_prop_decidable
-      let decEqDiscrTrue := mkApp2 (mkConst ``instDecidableEqBool) eqDiscrExpr trueExpr
-      let decEqBVExprTrue := mkApp2 (mkConst ``instDecidableEqBool) eqBVExpr trueExpr
-      let impDecidable := mkApp4 (mkConst ``forall_prop_decidable)
-        eqDiscrTrueExpr
-        (.lam .anonymous eqDiscrTrueExpr eqBVExprTrueExpr .default)
-        decEqDiscrTrue
-        (.lam .anonymous eqDiscrTrueExpr decEqBVExprTrue .default)
-
-      let decideImpExpr := mkApp2 (mkConst ``Decidable.decide) impExpr impDecidable
+      -- !discr || (atom == rhs)
+      let impExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
+
+      return mkApp4
+        (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
+        impExpr
+        evalExpr
+        congrProof
+        lemmaProof
+    return some ⟨imp.bvExpr, proof, imp.expr⟩
+
+  mkCondFalseLemma (discr : ReifiedBVLogical) (atom rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
+    let resExpr := rhsExpr
+    let resValExpr := rhs
+    let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false
+
+    let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
+    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
+    let eqBV ← ReifiedBVLogical.ofPred eqBVPred
+
+    let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or
+
+    let proof := do
+      let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
+      let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
+      let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr rhs.width) discrExpr lhsExpr rhsExpr
+
+      -- discr || (atom == rhs)
+      let impExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr
 
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
-        decideImpExpr
+        impExpr
         evalExpr
         congrProof
         lemmaProof

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -220,15 +220,12 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | ite _ discrExpr _ lhsExpr rhsExpr =>
-      let_expr Eq α discrExpr val := discrExpr | return none
-      let_expr Bool := α | return none
-      let_expr Bool.true := val | return none
+    | cond _ discrExpr lhsExpr rhsExpr =>
       let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
       let some discr ← ReifiedBVLogical.of discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
-      addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
+      addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
       return some atom
     | _ => return none
 
@@ -392,10 +389,7 @@ where
       | Bool => gateReflection lhsExpr rhsExpr .beq
       | BitVec _ => goPred t
       | _ => return none
-    | ite _ discrExpr _ lhsExpr rhsExpr =>
-      let_expr Eq α discrExpr val := discrExpr | return none
-      let_expr Bool := α | return none
-      let_expr Bool.true := val | return none
+    | cond _ discrExpr lhsExpr rhsExpr =>
       let some discr ← goOrAtom discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -127,8 +127,6 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
       else
         return .continue
 
-attribute [builtin_bv_normalize_proc↓] reduceIte
-
 /-- Return a number `k` such that `2^k = n`. -/
 private def Nat.log2Exact (n : Nat) : Option Nat := do
   guard <| n ≠ 0

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -293,8 +293,15 @@ The semantics for `BVExpr`.
 -/
 def eval (assign : Assignment) : BVExpr w → BitVec w
   | .var idx =>
-    let ⟨bv⟩ := assign.get idx
-    bv.truncate w
+    let packedBv := assign.get idx
+    /-
+    This formulation improves performance, as in a well formed expression the condition always holds
+    so there is no need for the more involved `BitVec.truncate` logic.
+    -/
+    if h : packedBv.w = w then
+      h ▸ packedBv.bv
+    else
+      packedBv.bv.truncate w
   | .const val => val
   | .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
   | .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
@@ -308,8 +315,13 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
   | .arithShiftRight lhs rhs => BitVec.sshiftRight' (eval assign lhs) (eval assign rhs)
 
 @[simp]
-theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate _ := by
-  rfl
+theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate w := by
+  rw [eval]
+  split
+  · next h =>
+    subst h
+    simp
+  · rfl
 
 @[simp]
 theorem eval_const : eval assign (.const val) = val := by rfl
@@ -454,7 +466,7 @@ def eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool :=
 @[simp] theorem eval_not : eval assign (.not x) = !eval assign x := rfl
 @[simp] theorem eval_gate : eval assign (.gate g x y) = g.eval (eval assign x) (eval assign y) := rfl
 @[simp] theorem eval_ite :
-  eval assign (.ite d l r) = if (eval assign d) then (eval assign l) else (eval assign r) := rfl
+  eval assign (.ite d l r) = bif (eval assign d) then (eval assign l) else (eval assign r) := rfl
 
 def Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) : Prop := eval assign x = true
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -18,21 +18,21 @@ inductive Gate
   | and
   | xor
   | beq
-  | imp
+  | or
 
 namespace Gate
 
 def toString : Gate → String
   | and => "&&"
   | xor => "^^"
   | beq => "=="
-  | imp => "->"
+  | or => "||"
 
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | xor => (· ^^ ·)
   | beq => (· == ·)
-  | imp => (· → ·)
+  | or => (· || ·)
 
 end Gate
 
@@ -59,13 +59,13 @@ def eval (a : α → Bool) : BoolExpr α → Bool
   | .const b => b
   | .not x => !eval a x
   | .gate g x y => g.eval (eval a x) (eval a y)
-  | .ite d l r => if d.eval a then l.eval a else r.eval a
+  | .ite d l r => bif d.eval a then l.eval a else r.eval a
 
 @[simp] theorem eval_literal : eval a (.literal l) = a l := rfl
 @[simp] theorem eval_const : eval a (.const b) = b := rfl
 @[simp] theorem eval_not : eval a (.not x) = !eval a x := rfl
 @[simp] theorem eval_gate : eval a (.gate g x y) = g.eval (eval a x) (eval a y) := rfl
-@[simp] theorem eval_ite : eval a (.ite d l r) = if d.eval a then l.eval a else r.eval a := rfl
+@[simp] theorem eval_ite : eval a (.ite d l r) = bif d.eval a then l.eval a else r.eval a := rfl
 
 def Sat (a : α → Bool) (x : BoolExpr α) : Prop := eval a x = true
 def Unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean

@@ -75,9 +75,9 @@ where
         let ret := aig.mkBEqCached input
         have := LawfulOperator.le_size (f := mkBEqCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
-      | .imp =>
-        let ret := aig.mkImpCached input
-        have := LawfulOperator.le_size (f := mkImpCached) aig input
+      | .or =>
+        let ret := aig.mkOrCached input
+        have := LawfulOperator.le_size (f := mkOrCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
 
 namespace ofBoolExprCached
@@ -127,9 +127,9 @@ theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
     | beq =>
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached), rih, lih]
-    | imp =>
+    | or =>
       simp only [go]
-      rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
+      rw [AIG.LawfulOperator.decl_eq (f := mkOrCached), rih, lih]
 
 theorem go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -118,7 +118,6 @@ theorem BitVec.srem_umod (x y : BitVec w) :
   rw [BitVec.srem_eq]
   cases x.msb <;> cases y.msb <;> simp
 
-attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 attribute [bv_normalize] BitVec.twoPow_eq
 

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -41,7 +41,14 @@ attribute [bv_normalize] Bool.not_not
 attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
 attribute [bv_normalize] eq_self
-attribute [bv_normalize] ite_self
+attribute [bv_normalize] Bool.cond_self
+attribute [bv_normalize] cond_false
+attribute [bv_normalize] cond_true
+attribute [bv_normalize] Bool.cond_not
+
+@[bv_normalize]
+theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b then x else y) := by
+  rw [cond_eq_if]
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide

src/Std/Tactic/BVDecide/Normalize/Prop.lean

@@ -13,8 +13,6 @@ This module contains the `Prop` simplifying part of the `bv_normalize` simp set.
 namespace Std.Tactic.BVDecide
 namespace Frontend.Normalize
 
-attribute [bv_normalize] ite_true
-attribute [bv_normalize] ite_false
 attribute [bv_normalize] dite_true
 attribute [bv_normalize] dite_false
 attribute [bv_normalize] and_true

src/Std/Tactic/BVDecide/Reflect.lean

@@ -123,12 +123,12 @@ theorem umod_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (lhs' % rhs') = (lhs % rhs) := by
   simp[*]
 
-theorem if_true (discr : Bool) (lhs rhs : BitVec w) :
-    decide ((discr == true) = true → ((if discr = true then lhs else rhs) == lhs) = true) = true := by
+theorem cond_true (discr : Bool) (lhs rhs : BitVec w) :
+    (!discr || ((bif discr then lhs else rhs) == lhs)) = true := by
   cases discr <;> simp
 
-theorem if_false (discr : Bool) (lhs rhs : BitVec w) :
-    decide ((discr == false) = true → ((if discr = true then lhs else rhs) == rhs) = true) = true := by
+theorem cond_false (discr : Bool) (lhs rhs : BitVec w) :
+    (discr || ((bif discr then lhs else rhs) == rhs)) = true := by
   cases discr <;> simp
 
 end BitVec
@@ -150,13 +150,13 @@ theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (lhs' == rhs') = (lhs == rhs) := by
   simp[*]
 
-theorem imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
+theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
+    (lhs' || rhs') = (lhs || rhs) := by
   simp[*]
 
-theorem ite_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
+theorem cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
     (h3 : rhs' = rhs) :
-    (if discr' = true then lhs' else rhs') = (if discr = true then lhs else rhs) := by
+    (bif discr' = true then lhs' else rhs') = (bif discr = true then lhs else rhs) := by
   simp[*]
 
 theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by

tests/lean/run/6043.lean

@@ -0,0 +1,6 @@
+import Std.Tactic.BVDecide
+
+theorem extracted_1 (x : BitVec 32) :
+  BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
+    BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by
+  bv_decide

tests/lean/run/bv_decide_rewriter.lean

@@ -85,6 +85,7 @@ example : (BitVec.twoPow 16 2) = 4#16 := by bv_normalize
 example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize
 example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize
 example {x y : Bool} (h1 : x && y) : x || y := by bv_normalize
+example (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by bv_normalize
 
 section
 

tests/lean/run/bv_substructure.lean

@@ -23,17 +23,8 @@ theorem substructure_unit_3' (x y : BitVec 8) : Bool.xor (x = y) (y ≠ x) := by
 theorem substructure_unit_4 (a b : Bool) : (a && b) = (b && a) := by
   bv_decide
 
-theorem substructure_unit_5 (a : Bool) (b c : BitVec 32) (h1 : b < c ↔ a) (h2 : a = true) : b < c := by
+theorem substructure_unit_5 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
   bv_decide
 
-theorem substructure_unit_6 (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by
-  bv_decide
-
-theorem substructure_unit_7 (a b c: Bool) : (bif a then b else c) = (bif !a then c else b) := by
-  bv_decide
-
-theorem substructure_unit_8 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
-  bv_decide
-
-theorem substructure_unit_9 (x y : BitVec 32) (h : x.getLsbD 0 = false) : (if x.getLsbD 0 then x else y) = y := by
+theorem substructure_unit_6 (x y : BitVec 32) (h : x.getLsbD 0 = false) : (if x.getLsbD 0 then x else y) = y := by
   bv_decide