final

leanprover · Feb 3, 2025 · 8d1069b · 8d1069b
1 parent 4517a83
commit 8d1069b
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 7 deletions.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -165,8 +165,7 @@ builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (_ : Bit
     let_expr BEq.beq α inst outerLhs rhs := e | return .continue
     let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue
     let_expr Complement.complement _ _ lhs := outerLhs | return .continue
-    let newRhs := ~~~rhsVal
-    let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst lhs (toExpr newRhs)
+    let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst lhs (toExpr (~~~rhsVal))
     let proof :=
       mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm)
         (toExpr w)
@@ -179,8 +178,7 @@ builtin_simproc [bv_normalize] bv_equal_const_not' ((_ : BitVec _) == ~~~(_ : Bi
     let_expr BEq.beq α inst lhs outerRhs := e | return .continue
     let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue
     let_expr Complement.complement _ _ rhs := outerRhs | return .continue
-    let newLhs := ~~~lhsVal
-    let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst (toExpr newLhs) rhs
+    let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst rhs (toExpr (~~~lhsVal))
     let proof :=
       mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm')
         (toExpr w)

diff --git a/src/Std/Tactic/BVDecide/Normalize/Equal.lean b/src/Std/Tactic/BVDecide/Normalize/Equal.lean
@@ -190,9 +190,10 @@ theorem BitVec.not_eq_comm (a b : BitVec w) : (~~~a == b) = (a == ~~~b) := by
   simp [_root_.BitVec.not_eq_comm]
 
 -- used for bv_equal_const_not simproc
-theorem BitVec.not_eq_comm' (a b : BitVec w) : (a == ~~~b) = (~~~a == b) := by
-  rw [Bool.eq_iff_iff]
+theorem BitVec.not_eq_comm' (a b : BitVec w) : (a == ~~~b) = (b == ~~~a) := by
+  rw [Bool.eq_iff_iff, beq_iff_eq, Eq.comm]
   simp [_root_.BitVec.not_eq_comm]
 
+
 end Frontend.Normalize
 end Std.Tactic.BVDecide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
@@ -233,7 +233,7 @@ example (d : Bool) (a b c : BitVec w) :
 example (a : BitVec 32) : (~~~a = 0#32) ↔ (a = -1) := by
   bv_normalize
 
-example (a : BitVec 32) : (0#32 = ~~~a) ↔ (-1 = a) := by
+example (a : BitVec 32) : (0#32 = ~~~a) ↔ (a = -1) := by
   bv_normalize
 
 -- reducing or to and while still applying or specific rewrites