Fix unfolding logic of bv_simplify

stdpp_unstable/bitvector_tactics.v

@@ -482,14 +482,22 @@ Tactic Notation "bv_simplify" :=
   with length of lists of bytes. *)
   reduce_closed_N;
   autorewrite with bv_simplify;
-  first [apply bv_eq_wrap | apply bv_neq_wrap | idtac];
+  lazymatch goal with
+  | |- _ =@{bv _} _ => apply bv_eq_wrap
+  | |- not (_ =@{bv _} _) => apply bv_neq_wrap
+  | _ => idtac
+  end;
   bv_unfold;
   autorewrite with bv_unfolded_simplify.
 
 Tactic Notation "bv_simplify" ident(H) :=
   unfold_lets_in_context;
   autorewrite with bv_simplify in H;
-  first [ apply bv_eq in H | apply bv_neq in H | idtac ];
+  lazymatch (type of H) with
+  | _ =@{bv _} _ => apply bv_eq in H
+  | not (_ =@{bv _} _) => apply bv_neq in H
+  | _ => idtac
+  end;
   tactic bv_unfold in H;
   autorewrite with bv_unfolded_simplify in H.
 Tactic Notation "bv_simplify" "select" open_constr(pat) :=

tests/bitvector_tactics.ref

@@ -64,3 +64,25 @@ goal 2 is:
        (bv_wrap (16 * 2) (bv_unsigned v ≫ Z.of_N (16 * 2)) ≪ Z.of_N (16 * 2))
        (Z.lor (bv_unsigned b ≪ Z.of_N (16 * 1))
           (bv_wrap (16 * 1) (bv_unsigned v))))
+1 goal
+  
+  b : bv 16
+  ============================
+  bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b)
+1 goal
+  
+  b : bv 16
+  ============================
+  bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned b + 1)
+1 goal
+  
+  b : bv 16
+  H : bv_unsigned b = bv_unsigned b
+  ============================
+  True
+1 goal
+  
+  b : bv 16
+  H : bv_unsigned b ≠ bv_wrap 16 (bv_unsigned b + 1)
+  ============================
+  True

tests/bitvector_tactics.v

@@ -73,3 +73,13 @@ Goal ∀ b : bv 16, ∀ v : bv 64,
 Proof.
   intros. bv_simplify. Show. bitblast.
 Qed.
+
+(** Regression test for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/411 *)
+Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b).
+Proof. intros. bv_simplify. Show. Restart. intros. bv_solve. Qed.
+Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned (b + BV 16 1)).
+Proof. intros. bv_simplify. Show. Restart. intros. bv_solve. Qed.
+Goal ∀ b : bv 16, bv_unsigned b = bv_unsigned b → True.
+Proof. intros ? H. bv_simplify H. Show. Abort.
+Goal ∀ b : bv 16, bv_unsigned b ≠ bv_unsigned (b + BV 16 1) → True.
+Proof. intros ? H. bv_simplify H. Show. Abort.