From 7474b08de4ef39572e2b63cc144bd0bf2bc2dfb8 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 22 May 2024 16:11:11 +0100 Subject: [PATCH] remove duplicates --- src/Init/Data/BitVec/Bitblast.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 9d99e6292f2d..1ca892057551 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -198,17 +198,6 @@ theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by simp [ule_eq_not_ult, ult_eq_not_carry] -theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false ↔ 2 * x.toNat < 2^w := by - cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide] - -theorem msb_eq_true_iff_two_mul_ge (x : BitVec w) : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by - simp [show x.msb = true ↔ ¬(x.msb = false) by simp, msb_eq_false_iff_two_mul_lt] - -theorem toInt_eq (x : BitVec w) : - x.toInt = if x.msb then (x.toNat : Int) - ((2^w : Nat) : Int) else x.toNat := by - simp only [BitVec.toInt, ← msb_eq_false_iff_two_mul_lt] - cases x.msb <;> rfl - /-- If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide -/ theorem slt_eq_ult_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) : x.slt y = x.ult y := by