From b8af0318bff0b7313c08778cc1cacf79e2d8e63c Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 25 Aug 2022 07:24:36 +0200
Subject: [PATCH] Fix unfolding logic of bv_simplify

---
 stdpp_unstable/bitvector_tactics.v | 12 ++++++++++--
 tests/bitvector_tactics.ref        | 22 ++++++++++++++++++++++
 tests/bitvector_tactics.v          | 10 ++++++++++
 3 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/stdpp_unstable/bitvector_tactics.v b/stdpp_unstable/bitvector_tactics.v
index 4efcc067..e3c2dfc0 100644
--- a/stdpp_unstable/bitvector_tactics.v
+++ b/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) :=
diff --git a/tests/bitvector_tactics.ref b/tests/bitvector_tactics.ref
index cb9e104d..49555584 100644
--- a/tests/bitvector_tactics.ref
+++ b/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
diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
index b5b2f6f5..149be4f8 100644
--- a/tests/bitvector_tactics.v
+++ b/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.
-- 
GitLab