feat: equivalence of bit-vector negation and bitblasted negation (#3920)

src/Init/Data/BitVec/Bitblast.lean

@@ -159,4 +159,29 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
 
+/-! ### Negation -/
+
+theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
+  getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
+  apply iunfoldr_getLsb (fun _ => ()) i (by simp)
+
+theorem bit_not_add_self (x : BitVec w) :
+  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x  = -1 := by
+  simp only [add_eq_adc]
+  apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
+  intro i; simp only [ BitVec.not, adcb, testBit_toNat]
+  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
+  <;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
+
+theorem bit_not_eq_not (x : BitVec w) :
+  ((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
+  simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
+
+theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
+  simp only [← add_eq_adc]
+  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
+  · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
+    simp [← sub_toAdd, BitVec.sub_add_cancel]
+  · simp [bit_not_testBit x _]
+
 end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
+Authors: Joe Hendrix, Harun Khan
 -/
 prelude
 import Init.Data.BitVec.Lemmas
@@ -48,6 +48,51 @@ private theorem iunfoldr.eq_test
     intro i
     simp_all [truncate_succ]
 
+theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+  (∀ i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
+  ∧ (iunfoldr f (state 0)).fst = state w := by
+  unfold iunfoldr
+  simp
+  apply Fin.hIterate_elim
+        (fun j (p : α × BitVec j) => (hj : j ≤ w) →
+         (∀ i : Fin j,  getLsb p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
+          ∧ p.fst = state j)
+  case hj => simp
+  case init =>
+    intro
+    apply And.intro
+    · intro i
+      have := Fin.size_pos i
+      contradiction
+    · rfl
+  case step =>
+    intro j ⟨s, v⟩ ih hj
+    apply And.intro
+    case left =>
+      intro i
+      simp only [getLsb_cons]
+      have hj2 : j.val ≤ w := by simp
+      cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
+      | inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
+                  exact (ih hj2).1 ⟨i.val, h3⟩
+      | inr h3 => simp [h3, if_pos]
+                  cases (Nat.eq_zero_or_pos j.val) with
+                  | inl hj3 => congr
+                               rw [← (ih hj2).2]
+                  | inr hj3 => congr
+                               exact (ih hj2).2
+    case right =>
+      simp
+      have hj2 : j.val ≤ w := by simp
+      rw [← ind j, ← (ih hj2).2]
+
+
+theorem iunfoldr_getLsb {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+  getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
+  exact (iunfoldr_getLsb' state ind).1 i
+
 /--
 Correctness theorem for `iunfoldr`.
 -/
@@ -58,4 +103,11 @@ theorem iunfoldr_replace
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
 
+theorem iunfoldr_replace_snd
+  {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    (iunfoldr f a).snd = value := by
+  simp [iunfoldr.eq_test state value a init step]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -2,6 +2,7 @@
 Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed,
+
 -/
 prelude
 import Init.Data.Bool
@@ -900,6 +901,15 @@ theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
+theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
+  rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
+      ← BitVec.add_assoc, ← sub_toAdd, add_sub_cancel]
+
+theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y ↔ x + y = z := by
+  apply Iff.intro <;> intro h
+  · simp [h, sub_add_cancel]
+  · simp [←h, add_sub_cancel]
+
 theorem negOne_eq_allOnes : -1#w = allOnes w := by
   apply eq_of_toNat_eq
   if g : w = 0 then