diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 8f05d13f93cd..f1f5e2db3fba 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -308,8 +308,7 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : @[simp] theorem toNat_mod_cancel' {x : BitVec n} : (x.toNat : Int) % (((2 ^ n) : Nat) : Int) = x.toNat := by - sorry -- FIXME #6278 - -- rw_mod_cast [toNat_mod_cancel] + rw_mod_cast [toNat_mod_cancel] @[simp] theorem sub_toNat_mod_cancel {x : BitVec w} (h : ¬ x = 0#w) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat := by @@ -787,10 +786,9 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h @[simp] theorem toInt_or (x y : BitVec w) : BitVec.toInt (x ||| y) = Int.bmod (BitVec.toNat x ||| BitVec.toNat y) (2^w) := by - sorry -- FIXME #6278 - -- rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt - -- (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))] - -- omega + rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt + (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))] + omega @[simp] theorem toFin_or (x y : BitVec v) : BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by @@ -861,10 +859,9 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where @[simp] theorem toInt_and (x y : BitVec w) : BitVec.toInt (x &&& y) = Int.bmod (BitVec.toNat x &&& BitVec.toNat y) (2^w) := by - sorry -- FIXME #6278 - -- rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt - -- (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))] - -- omega + rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt + (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))] + omega @[simp] theorem toFin_and (x y : BitVec v) : BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by @@ -935,10 +932,9 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher @[simp] theorem toInt_xor (x y : BitVec w) : BitVec.toInt (x ^^^ y) = Int.bmod (BitVec.toNat x ^^^ BitVec.toNat y) (2^w) := by - sorry -- FIXME #6278 - -- rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt - -- (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))] - -- omega + rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt + (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))] + omega @[simp] theorem toFin_xor (x y : BitVec v) : BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by @@ -1019,11 +1015,10 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl @[simp] theorem toInt_not {x : BitVec w} : (~~~x).toInt = Int.bmod (2^w - 1 - x.toNat) (2^w) := by - sorry -- FIXME #6278 - -- rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def] - -- simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega] - -- rw_mod_cast [Nat.mod_eq_of_lt (by omega)] - -- omega + rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def] + simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega] + rw_mod_cast [Nat.mod_eq_of_lt (by omega)] + omega @[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} : BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by @@ -1587,18 +1582,17 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms apply BitVec.eq_of_toNat_eq simp only [signExtend, BitVec.toInt_eq_msb_cond, toNat_ofInt, toNat_not, toNat_setWidth, hmsb, ↓reduceIte] - sorry -- FIXME #6278 - -- norm_cast - -- rw [Int.ofNat_sub_ofNat_of_lt, Int.negSucc_emod] - -- simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one] - -- rw [Int.subNatNat_of_le] - -- · rw [Int.toNat_ofNat, Nat.add_comm, Nat.sub_add_eq] - -- · apply Nat.le_trans - -- · apply Nat.succ_le_of_lt - -- apply Nat.mod_lt - -- apply Nat.two_pow_pos - -- · apply Nat.le_refl - -- · omega + norm_cast + rw [Int.ofNat_sub_ofNat_of_lt, Int.negSucc_emod] + simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one] + rw [Int.subNatNat_of_le] + · rw [Int.toNat_ofNat, Nat.add_comm, Nat.sub_add_eq] + · apply Nat.le_trans + · apply Nat.succ_le_of_lt + apply Nat.mod_lt + apply Nat.two_pow_pos + · apply Nat.le_refl + · omega theorem getLsbD_signExtend (x : BitVec w) {v i : Nat} : (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by @@ -1676,11 +1670,10 @@ theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v): simp [getElem_signExtend, Nat.le_sub_one_of_lt hv] have H : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right (by omega) (by omega) simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul] - sorry -- FIXME #6278 - -- by_cases h : x.msb - -- <;> norm_cast - -- <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)] - -- omega + by_cases h : x.msb + <;> norm_cast + <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)] + omega /- If the current width `w` is larger than the extended width `v`, diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index ecff751c14ae..d2741d67f05b 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -24,12 +24,11 @@ theorem shiftRight_add (i : Int) (m n : Nat) : theorem shiftRight_eq_div_pow (m : Int) (n : Nat) : m >>> n = m / ((2 ^ n) : Nat) := by - sorry -- FIXME #6278 - -- simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow] - -- split - -- · simp - -- · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))] - -- rfl + simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow] + split + · simp + · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))] + rfl @[simp] theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean index d617999ca1b5..233849788b86 100644 --- a/src/Init/Data/Int/Pow.lean +++ b/src/Init/Data/Int/Pow.lean @@ -52,9 +52,8 @@ protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) : @[simp] protected theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) : (2 : Int) ^ (w - 1) - (2 : Int) ^ w = - (2 : Int) ^ (w - 1) := by - sorry -- FIXME #6278 - -- norm_cast - -- rw [← Nat.two_pow_pred_add_two_pow_pred h] - -- simp [h] + norm_cast + rw [← Nat.two_pow_pred_add_two_pow_pred h] + simp [h] end Int