feat: Adding HackersDelight file (#457)

opencompl · Jul 12, 2024 · f78035f · f78035f
1 parent d30ad76
commit f78035f
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/Alive.lean b/SSA/Projects/InstCombine/Alive.lean
@@ -30,3 +30,5 @@ import SSA.Projects.InstCombine.LLVM.Lemmas
 import SSA.Projects.InstCombine.Test
 -- Examples for the paper
 import SSA.Projects.InstCombine.PaperExamples
+-- Proofs from Hackers Delight Book
+import SSA.Projects.InstCombine.HackersDelight
diff --git a/SSA/Projects/InstCombine/HackersDelight.lean b/SSA/Projects/InstCombine/HackersDelight.lean
@@ -0,0 +1,14 @@
+import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Bitblast
+
+namespace HackersDelight
+
+namespace Ch1
+
+theorem neg_eq_not_add_one {x : BitVec w} : - x = ~~~ x + 1 := by
+  apply BitVec.neg_eq_not_add
+
+end Ch1
+
+end HackersDelight