From e5b7dc819bebee0e1dd05fec72b6049bc0d803e9 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Tue, 7 May 2024 23:31:19 +0100 Subject: [PATCH] feat: bitvec lemma to turn negation into bitwise not+add (#4095) Identity 2-2 (a) (Section: Addition Combined with Logical Operations) from Hacker's Delight, 2nd edition. --- src/Init/Data/BitVec/Lemmas.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 23cc6c9919..27f3632e23 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -919,6 +919,13 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by have r : (2^w - 1) < 2^w := by omega simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r] +theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by + apply eq_of_toNat_eq + simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod] + congr + have hx : x.toNat < 2^w := x.isLt + rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, ← Nat.sub_sub, Nat.sub_add_cancel (by omega)] + /-! ### mul -/ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl