respect new rewrites

Author: hargoniX

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

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic
 import Lean.Elab.Tactic.BVDecide.Frontend.Attr
 import Lean.Elab.Tactic.Simp
-import Lean.Meta.Tactic.Generalize
 
 /-!
 This module contains the implementation of the pre processing pass for reducing `UIntX`/`IntX` to
@@ -26,8 +24,17 @@ namespace Frontend.Normalize
 
 open Lean.Meta
 
+/--
+Contains information for the `USize` elimination pass.
+-/
 structure USizeState where
+  /--
+  Contains terms of the form `USize.toBitVec e` that we will translate to constant width `BitVec`.
+  -/
   relevantTerms : Std.HashSet Expr := {}
+  /--
+  Contains all hypotheses that contain terms from `relevantTerms`
+  -/
   relevantHyps : Std.HashSet FVarId := {}
 
 private abbrev M := StateRefT USizeState MetaM
@@ -83,9 +90,9 @@ where
   replaceUSize (goal : MVarId) : M MVarId := do
     if let some (numBits, numBitsEq) ← findNumBitsEq goal then
       goal.withContext do
-        let relevantHyps := (← get).relevantHyps.toArray
+        let relevantHyps := (← get).relevantHyps.toArray.map mkFVar
         let relevantTerms := (← get).relevantTerms.toArray
-        let (app, abstractedHyps) ← liftMkBindingM <| MetavarContext.revert (relevantHyps.map mkFVar) goal true
+        let (app, abstractedHyps) ← liftMkBindingM <| MetavarContext.revert relevantHyps goal true
         let newMVar := app.getAppFn.mvarId!
         let targetType ← newMVar.getType
         /-

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

@@ -10,7 +10,7 @@ a.toBitVec = 0xff#8
 b.toBitVec = 0xff#8
 -/
 #guard_msgs in
-example (a b : UInt8) : a + b = a := by
+example (a b : UInt8) : a + b > a := by
   bv_decide
 
 
@@ -25,7 +25,7 @@ a.toBitVec = 0xffff#16
 b.toBitVec = 0xffff#16
 -/
 #guard_msgs in
-example (a b : UInt16) : a + b = a := by
+example (a b : UInt16) : a + b > a := by
   bv_decide
 
 
@@ -40,7 +40,7 @@ a.toBitVec = 0xffffffff#32
 b.toBitVec = 0xffffffff#32
 -/
 #guard_msgs in
-example (a b : UInt32) : a + b = a := by
+example (a b : UInt32) : a + b > a := by
   bv_decide
 
 
@@ -55,7 +55,7 @@ a.toBitVec = 0xffffffffffffffff#64
 b.toBitVec = 0xffffffffffffffff#64
 -/
 #guard_msgs in
-example (a b : UInt64) : a + b = a := by
+example (a b : UInt64) : a + b > a := by
   bv_decide
 
 
@@ -70,7 +70,7 @@ warning: Detected USize in the goal but no hypothesis about System.Platform.numB
 warning: declaration uses 'sorry'
 -/
 #guard_msgs in
-example (a b : USize) : a + b = a := by
+example (a b : USize) : a + b > a := by
   bv_normalize
   sorry