From 65637b7683641f956225973993b02bbfbf81be14 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Mon, 14 Oct 2024 03:14:11 -0500 Subject: [PATCH] feat: lemmas about BitVector arithmetic inequalities (#5646) These lemmas are peeled from `leanprover/lnsym`. Moreover, note that these lemmas only hold when we do not have overflow in their operands, and thus, we are able to treat the operands as if they were 'regular' natural numbers. --------- Co-authored-by: Tobias Grosser Co-authored-by: Kim Morrison --- src/Init/Data/BitVec/Lemmas.lean | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 59e7e4749e..f05555b3e7 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2840,6 +2840,31 @@ theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) : (x * y).toNat = x.toNat * y.toNat := by rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h] + +/-- +`x ≤ y + z` if and only if `x - z ≤ y` +when `x - z` and `y + z` do not overflow. +-/ +theorem le_add_iff_sub_le {x y z : BitVec w} + (hxz : z ≤ x) (hbz : y.toNat + z.toNat < 2^w) : + x ≤ y + z ↔ x - z ≤ y := by + simp_all only [BitVec.le_def] + rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega), + BitVec.toNat_add_of_lt (by omega)] + omega + +/-- +`x - z ≤ y - z` if and only if `x ≤ y` +when `x - z` and `y - z` do not overflow. +-/ +theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) : + (x - z ≤ y - z) ↔ x ≤ y := by + simp_all only [BitVec.le_def] + rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega), + BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)] + omega + + /-! ### Decidable quantifiers -/ theorem forall_zero_iff {P : BitVec 0 → Prop} :