feat: theorems about Nat/Int/Rat needed for dyadics

src/Init/Data/Int/Bitwise/Basic.lean

@@ -50,4 +50,21 @@ protected def shiftRight : Int → Nat → Int
 
 instance : HShiftRight Int Nat Int := ⟨.shiftRight⟩
 
+/--
+Bitwise left shift, usually accessed via the `<<<` operator.
+
+Examples:
+ * `1 <<< 2 = 4`
+ * `1 <<< 3 = 8`
+ * `0 <<< 3 = 0`
+ * `0xf1 <<< 4 = 0xf10`
+ * `(-1) <<< 3 = -8`
+-/
+@[expose]
+protected def shiftLeft : Int → Nat → Int
+  | Int.ofNat n, s => Int.ofNat (n <<< s)
+  | Int.negSucc n, s => Int.negSucc (((n + 1) <<< s) - 1)
+
+instance : HShiftLeft Int Nat Int := ⟨.shiftLeft⟩
+
 end Int

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -37,11 +37,11 @@ theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
   · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
     rfl
 
-@[simp]
+@[simp, grind =]
 theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
   simp [Int.shiftRight_eq_div_pow]
 
-@[simp]
+@[simp, grind =]
 theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
@@ -88,4 +88,32 @@ theorem shiftRight_le_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : (n >>> s)
     have rl : n / 2 ^ s ≤ 0 := Int.ediv_nonpos_of_nonpos_of_neg (by omega) (by norm_cast at *; omega)
     norm_cast at *
 
+@[simp, grind =]
+theorem shiftLeft_zero (n : Int) : n <<< 0 = n := by
+  change Int.shiftLeft _ _ = _
+  match n with
+  | Int.ofNat n
+  | Int.negSucc n => simp [Int.shiftLeft]
+
+theorem shiftLeft_succ (m : Int) (n : Nat) : m <<< (n + 1) = (m <<< n) * 2 := by
+  change Int.shiftLeft _ _ = Int.shiftLeft _ _ * 2
+  match m with
+  | (m : Nat) =>
+    dsimp [Int.shiftLeft]
+    rw [Nat.shiftLeft_succ, Nat.mul_comm, natCast_mul, ofNat_two]
+  | Int.negSucc m =>
+    dsimp [Int.shiftLeft]
+    rw [Nat.shiftLeft_succ, Nat.mul_comm, Int.negSucc_eq]
+    have := Nat.le_shiftLeft (a := m + 1) (b := n)
+    omega
+
+theorem shiftLeft_eq (a : Int) (b : Nat) : a <<< b = a * 2 ^ b := by
+  induction b with
+  | zero => simp
+  | succ b ih =>
+    rw [shiftLeft_succ, ih, Int.pow_succ, Int.mul_assoc]
+
+theorem shiftLeft_eq' (a : Int) (b : Nat) : a <<< b = a * (2 ^ b : Nat) := by
+  simp [shiftLeft_eq]
+
 end Int

src/Init/Data/Int/Pow.lean

@@ -21,6 +21,11 @@ protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
+protected theorem pow_add (a : Int) (m n : Nat) : a ^ (m + n) = a ^ m * a ^ n := by
+  induction n with
+  | zero => rw [Nat.add_zero, Int.pow_zero, Int.mul_one]
+  | succ _ ih => rw [Nat.add_succ, Int.pow_succ, Int.pow_succ, ih, Int.mul_assoc]
+
 protected theorem zero_pow {n : Nat} (h : n ≠ 0) : (0 : Int) ^ n = 0 := by
   match n, h with
   | n + 1, _ => simp [Int.pow_succ]

src/Init/Data/Nat/Lemmas.lean

@@ -1331,6 +1331,25 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
 theorem log2_lt (h : n ≠ 0) : n.log2 < k ↔ n < 2 ^ k := by
   rw [← Nat.not_le, ← Nat.not_le, le_log2 h]
 
+theorem log2_eq_iff (h : n ≠ 0) : n.log2 = k ↔ 2 ^ k ≤ n ∧ n < 2 ^ (k + 1) := by
+  constructor
+  · intro w
+    exact ⟨(le_log2 h).mp (Nat.le_of_eq w.symm), (log2_lt h).mp (by subst w; apply lt_succ_self)⟩
+  · intro w
+    apply Nat.le_antisymm
+    · apply Nat.le_of_lt_add_one
+      exact (log2_lt h).mpr w.2
+    · exact (le_log2 h).mpr w.1
+
+theorem log2_two_mul (h : n ≠ 0) : (2 * n).log2 = n.log2 + 1 := by
+  obtain ⟨h₁, h₂⟩ := (log2_eq_iff h).mp rfl
+  rw [log2_eq_iff (Nat.mul_ne_zero (by decide) h)]
+  constructor
+  · rw [Nat.pow_succ, Nat.mul_comm]
+    exact mul_le_mul_left 2 h₁
+  · rw [Nat.pow_succ, Nat.mul_comm]
+    rwa [Nat.mul_lt_mul_right (by decide)]
+
 @[simp]
 theorem log2_two_pow : (2 ^ n).log2 = n := by
   apply Nat.eq_of_le_of_lt_succ <;> simp [le_log2, log2_lt, NeZero.ne, Nat.pow_lt_pow_iff_right]

src/Init/Data/Rat/Lemmas.lean

@@ -209,6 +209,9 @@ theorem add_def (a b : Rat) :
 theorem add_def' (a b : Rat) : a + b = mkRat (a.num * b.den + b.num * a.den) (a.den * b.den) := by
   rw [add_def, normalize_eq_mkRat]
 
+theorem add_zero (a : Rat) : a + 0 = a := by simp [add_def', mkRat_self]
+theorem zero_add (a : Rat) : 0 + a = a := by simp [add_def', mkRat_self]
+
 theorem normalize_add_normalize (n₁ n₂) {d₁ d₂} (z₁ z₂) :
     normalize n₁ d₁ z₁ + normalize n₂ d₂ z₂ =
     normalize (n₁ * d₂ + n₂ * d₁) (d₁ * d₂) (Nat.mul_ne_zero z₁ z₂) := by