feat: add BitVec.toInt_[pos|neg]_iff_toNat_[large|small]

opencompl · Aug 18, 2024 · b756ee6 · b756ee6
1 parent 38288ae
commit b756ee6
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -303,6 +303,14 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 @[simp] theorem ofInt_natCast (w n : Nat) :
   BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
 
+theorem toInt_neg_iff_toNat_large {w : Nat} {x : BitVec w} :
+    BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
+  simp [toInt_eq_toNat_cond]; omega
+
+theorem toInt_pos_iff_toNat_small {w : Nat} {x : BitVec w} :
+    0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
+  simp [toInt_eq_toNat_cond]; omega
+
 /-! ### zeroExtend and truncate -/
 
 theorem truncate_eq_zeroExtend {v : Nat} {x : BitVec w} :