From 965d186bd846e38c923b47a25463bd7c7044ecdd Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 14 May 2024 06:55:23 +0100 Subject: [PATCH 1/3] feat: add BitVec.and_add_xor_eq_or This solves one AliveStatement --- SSA/Projects/InstCombine/ForLean.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 41a662e47..771bbd255 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -810,6 +810,23 @@ lemma toInt_zero_iff (w : Nat) (x : BitVec w) : BitVec.toInt x = 0 ↔ x = 0 := lemma toInt_nonzero_iff (w : Nat) (x : BitVec w) : BitVec.toInt x ≠ 0 ↔ x ≠ 0 := by simp [toInt_ne] +@[simp] +theorem and_add_xor_eq_or {a b : BitVec w} : (b &&& a) + (b ^^^ a) = b ||| a := by + ext i + rw [getLsb_add (by omega), getLsb_and, getLsb_xor, getLsb_or] + have hj : carry (↑i) (b &&& a) (b ^^^ a) false = false := by + induction i.val + case zero => + simp [carry, Nat.mod_one] + case succ v v_h => + simp only [carry_succ, v_h, Bool.atLeastTwo_false_right, getLsb_and, + getLsb_xor, Bool.and_eq_false_imp, Bool.and_eq_true, bne_eq_false_iff_eq, + and_imp] + intros x x' + rw [x, x'] + simp only [Bool.bne_assoc] + by_cases h_a : a.getLsb ↑i <;> simp [h_a, hj] + end BitVec -- Given (a, b) that are less than a modulus m, to show (a + b) % m < k, it suffices to consider two cases. From 34ff84d1c44de310759fc9c579b081a03fab7faa Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 15 May 2024 05:14:44 +0100 Subject: [PATCH 2/3] Update SSA/Projects/InstCombine/ForLean.lean Co-authored-by: Alex Keizer --- SSA/Projects/InstCombine/ForLean.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 771bbd255..17900f46b 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -825,7 +825,7 @@ theorem and_add_xor_eq_or {a b : BitVec w} : (b &&& a) + (b ^^^ a) = b ||| a := intros x x' rw [x, x'] simp only [Bool.bne_assoc] - by_cases h_a : a.getLsb ↑i <;> simp [h_a, hj] + cases a.getLsb ↑i <;> simp [hj] end BitVec From f35dab00cedcc3d0e6d2f9bc927c9cf5ebb9dfc5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 15 May 2024 05:30:31 +0100 Subject: [PATCH 3/3] chore: extract lemma --- SSA/Projects/InstCombine/ForLean.lean | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 17900f46b..5600621f8 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -811,21 +811,22 @@ lemma toInt_nonzero_iff (w : Nat) (x : BitVec w) : BitVec.toInt x ≠ 0 ↔ x simp [toInt_ne] @[simp] -theorem and_add_xor_eq_or {a b : BitVec w} : (b &&& a) + (b ^^^ a) = b ||| a := by +lemma carry_and_xor_false : carry i (a &&& b) (a ^^^ b) false = false := by + induction i + case zero => + simp [carry, Nat.mod_one] + case succ v v_h => + simp only [carry_succ, v_h, Bool.atLeastTwo_false_right, getLsb_and, + getLsb_xor, Bool.and_eq_false_imp, Bool.and_eq_true, bne_eq_false_iff_eq, + and_imp] + intros; simp [*] + +@[simp] +theorem and_add_xor_eq_or {a b : BitVec w} : (a &&& b) + (a ^^^ b) = a ||| b := by ext i rw [getLsb_add (by omega), getLsb_and, getLsb_xor, getLsb_or] - have hj : carry (↑i) (b &&& a) (b ^^^ a) false = false := by - induction i.val - case zero => - simp [carry, Nat.mod_one] - case succ v v_h => - simp only [carry_succ, v_h, Bool.atLeastTwo_false_right, getLsb_and, - getLsb_xor, Bool.and_eq_false_imp, Bool.and_eq_true, bne_eq_false_iff_eq, - and_imp] - intros x x' - rw [x, x'] simp only [Bool.bne_assoc] - cases a.getLsb ↑i <;> simp [hj] + cases a.getLsb ↑i <;> simp [carry_and_xor_false] end BitVec