diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 186ff1f6ba54..55645f1de34e 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -833,9 +833,12 @@ theorem Int.mod_lt (a : Int) (b: Nat) (h : a < 0) (h2 : -a < b): a % b = b - ((- have rr : ¬ (2 * x.toNat < 2 ^ n) := by omega simp [rr] norm_cast - have ee : ((((x.toNat:Nat):Int) - (((2 ^ n):Nat):Int)))< 0 := sorry - rw [Int.mod_lt ee sorry] - have nn : -(↑x.toNat - (((2 ^ n:Nat)):Int)) % (((2 ^ i):Nat):Int) = -(↑x.toNat - ((2 ^ n):Int)) := sorry + have ee : ((((x.toNat:Nat):Int) - (((2 ^ n):Nat):Int)))< 0 := by omega + rw [Int.mod_lt ee] + have nn : -(↑x.toNat - (((2 ^ n:Nat)):Int)) % (((2 ^ i):Nat):Int) = -(↑x.toNat - ((2 ^ n):Int)) := by + norm_cast + + sorry rw [nn] norm_cast rw [Int.neg_sub] @@ -844,9 +847,16 @@ theorem Int.mod_lt (a : Int) (b: Nat) (h : a < 0) (h2 : -a < b): a % b = b - ((- norm_cast have y : x.toNat + (2 ^ i - 1) - (2 ^ n - 1) = x.toNat + (2 ^ i) - (2 ^ n) := by omega rw [y] - have yy : ((((2 ^ i):Nat):Int) + (↑x.toNat - 2 ^ n)).toNat = 2 ^ i + x.toNat - 2 ^ n := by omega + have yy : ((((2 ^ i):Nat):Int) + (↑x.toNat - 2 ^ n)).toNat = 2 ^ i + x.toNat - 2 ^ n := by + norm_cast + omega rw [yy] omega + norm_cast + have uu : ↑x.toNat - ↑(2 ^ n) < 2 ^n := by omega + norm_cast + have ii := Nat.pow_lt_pow_of_lt (a := 2) (by omega) xx + omega · simp at rr simp [rr] have tt := BitVec.toNat_lt_of_msb_false rr