non-trivialize tests

Author: hargoniX

Diff for: src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean

@@ -107,7 +107,7 @@ where
         -/
         let (motive, newGoalType) ←
           withLocalDeclD `z (mkConst ``Nat) fun z => do
-            let otherArgType := mkApp2 (mkConst ``Eq [1]) (toExpr numBits) (mkConst ``System.Platform.numBits)
+            let otherArgType := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) (toExpr numBits) z
             withLocalDeclD `h otherArgType fun other => do
               let argType := mkApp (mkConst ``BitVec) z
               let argTypes := relevantTerms.map (fun _ => (`x, argType))
@@ -133,7 +133,7 @@ where
         goal.assign <| mkAppN casesOn (relevantTerms ++ abstractedHyps)
         -- remove all of the hold hypotheses about USize.toBitVec to prevent false counter examples
         (newGoal, _) ← newGoal.tryClearMany' (abstractedHyps.map Expr.fvarId!)
-        -- intro both the new `BitVec 32` as well as all hypotheses about them
+        -- intro both the new `BitVec const` as well as all hypotheses about them
         (_, newGoal) ← newGoal.introN (relevantTerms.size + abstractedHyps.size)
         return newGoal
     else

Diff for: tests/lean/run/bv_uint.lean

@@ -1,7 +1,7 @@
 import Std.Tactic.BVDecide
 
 /-! UInt8 -/
-example (a b : UInt8) : a + b = b + a := by
+example (a b c : UInt8) (h1 : a < b) (h2 : b < c) : a < c := by
   bv_decide
 
 /--
@@ -16,7 +16,7 @@ example (a b : UInt8) : a + b = a := by
 
 
 /-! UInt16 -/
-example (a b : UInt16) : a + b = b + a := by
+example (a b c : UInt16) (h1 : a < b) (h2 : b < c) : a < c := by
   bv_decide
 
 /--
@@ -31,7 +31,7 @@ example (a b : UInt16) : a + b = a := by
 
 
 /-! UInt32 -/
-example (a b : UInt32) : a + b = b + a := by
+example (a b c : UInt32) (h1 : a < b) (h2 : b < c) : a < c := by
   bv_decide
 
 /--
@@ -46,7 +46,7 @@ example (a b : UInt32) : a + b = a := by
 
 
 /-! UInt64 -/
-example (a b : UInt64) : a + b = b + a := by
+example (a b c : UInt64) (h1 : a < b) (h2 : b < c) : a < c := by
   bv_decide
 
 /--
@@ -61,7 +61,7 @@ example (a b : UInt64) : a + b = a := by
 
 
 /-! USize -/
-example (a b : USize) : a + b = b + a := by
+example (a b c : USize) (h1 : a < b) (h2 : b < c) : a < c := by
   cases System.Platform.numBits_eq <;> bv_decide
 
 /--
@@ -74,9 +74,5 @@ example (a b : USize) : a + b = a := by
   bv_normalize
   sorry
 
-
-example (h : 32 = System.Platform.numBits) (a b : USize) : a + b = b + a := by
-  bv_decide
-
-example (h : System.Platform.numBits = 32) (a b : USize) : a + b = a := by
+example (h : 32 = System.Platform.numBits) (a b c : USize) (h1 : a < b) (h2 : b < c) : a < c := by
   bv_decide