From 9fc991da3304a73512575ef50f3b99aef9bbf855 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Fri, 21 Mar 2025 08:58:18 +0000
Subject: [PATCH] feat: add BV De Morgan's (extended) theorems from Hacker's
 Delight, 2.1 (#7604)

This PR adds bitvector theorems that to push negation into other
operations, following Hacker's Delight: Ch2.1.
---
 src/Init/Data/BitVec/Bitblast.lean | 26 +++++++++++++++++++++++++-
 src/Init/Data/BitVec/Lemmas.lean   | 16 ++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 8105949ab5..884a15605a 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1350,7 +1350,31 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
-/-! ### Lemmas that use Bitblasting Infrastructure -/
+/-! ### Lemmas that use Bitblasting circuits -/
+
+theorem add_sub_comm {x y : BitVec w} : x + y - z = x - z + y := by
+  apply eq_of_toNat_eq
+  simp only [toNat_sub, toNat_add, add_mod_mod, mod_add_mod]
+  congr 1
+  omega
+
+theorem sub_add_comm {x y : BitVec w} : x - y + z = x + z - y := by
+  rw [add_sub_comm]
+
+theorem not_add_one {x : BitVec w} : ~~~ (x + 1#w) = ~~~ x - 1#w := by
+  rw [not_eq_neg_add, not_eq_neg_add, neg_add]
+
+theorem not_add_eq_not_neg {x y : BitVec w} : ~~~ (x + y) = ~~~ x - y := by
+  rw [not_eq_neg_add, not_eq_neg_add, neg_add]
+  simp only [sub_toAdd]
+  rw [BitVec.add_assoc, @BitVec.add_comm _ (-y), ← BitVec.add_assoc]
+
+theorem not_sub_one_eq_not_add_one {x : BitVec w} : ~~~ (x - 1#w) = ~~~ x + 1#w := by
+  rw [not_eq_neg_add, not_eq_neg_add, neg_sub,
+    BitVec.add_sub_cancel, BitVec.sub_add_cancel]
+
+theorem not_sub_eq_not_add {x y : BitVec w} : ~~~ (x - y) = ~~~ x + y := by
+  rw [BitVec.sub_toAdd, not_add_eq_not_neg, sub_neg]
 
 /-- The value of `(carry i x y false)` can be computed by truncating `x` and `y`
 to `len` bits where `len ≥ i`. -/
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index fecb439734..1b2a29f221 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1573,6 +1573,22 @@ theorem not_self_ne {a : BitVec w} (h : 0 < w) : ~~~a ≠ a := by
   rw [ne_comm]
   simp [h]
 
+theorem not_and {x y : BitVec w} : ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by
+  ext i
+  simp
+
+theorem not_or {x y : BitVec w} : ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by
+  ext i
+  simp
+
+theorem not_xor_left {x y : BitVec w} : ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
+  ext i
+  simp
+
+theorem not_xor_right {x y : BitVec w} : ~~~ (x ^^^ y) = x ^^^ ~~~ y := by
+  ext i
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(x.cast h) = (~~~x).cast h := by