From 83d7426bfc4e802df64c373031a369a895b54bfa Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 10 Sep 2023 18:23:14 +0000 Subject: [PATCH] refactor(Data/Int/Bitwise): use `<<<` and `>>>` notation (#6789) The lemma names have changed to use `shiftLeft` and `shiftRight` to match the new `Nat` names. --- Mathlib/Data/Int/Bitwise.lean | 83 ++++++++++++++++-------------- Mathlib/Init/Data/Int/Bitwise.lean | 15 +++--- 2 files changed, 51 insertions(+), 47 deletions(-) diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index e11d7165673b4..b0c5ee7116ecf 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -365,96 +365,99 @@ theorem testBit_lnot : ∀ n k, testBit (lnot n) k = not (testBit n k) #align int.test_bit_lnot Int.testBit_lnot @[simp] -theorem shiftl_neg (m n : ℤ) : shiftl m (-n) = shiftr m n := +theorem shiftLeft_neg (m n : ℤ) : m <<< (-n) = m >>> n := rfl -#align int.shiftl_neg Int.shiftl_neg +#align int.shiftl_neg Int.shiftLeft_neg @[simp] -theorem shiftr_neg (m n : ℤ) : shiftr m (-n) = shiftl m n := by rw [← shiftl_neg, neg_neg] -#align int.shiftr_neg Int.shiftr_neg +theorem shiftRight_neg (m n : ℤ) : m >>> (-n) = m <<< n := by rw [← shiftLeft_neg, neg_neg] +#align int.shiftr_neg Int.shiftRight_neg -- Porting note: what's the correct new name? @[simp] -theorem shiftl_coe_nat (m n : ℕ) : shiftl m n = m <<< n := - by simp [shiftl] -#align int.shiftl_coe_nat Int.shiftl_coe_nat +theorem shiftLeft_coe_nat (m n : ℕ) : (m : ℤ) <<< (n : ℤ) = ↑(m <<< n) := + by simp [instShiftLeftInt, HShiftLeft.hShiftLeft] +#align int.shiftl_coe_nat Int.shiftLeft_coe_nat -- Porting note: what's the correct new name? @[simp] -theorem shiftr_coe_nat (m n : ℕ) : shiftr m n = m >>> n := by cases n <;> rfl -#align int.shiftr_coe_nat Int.shiftr_coe_nat +theorem shiftRight_coe_nat (m n : ℕ) : (m : ℤ) >>> (n : ℤ) = m >>> n := by cases n <;> rfl +#align int.shiftr_coe_nat Int.shiftRight_coe_nat @[simp] -theorem shiftl_negSucc (m n : ℕ) : shiftl -[m+1] n = -[Nat.shiftLeft' true m n+1] := +theorem shiftLeft_negSucc (m n : ℕ) : -[m+1] <<< (n : ℤ) = -[Nat.shiftLeft' true m n+1] := rfl -#align int.shiftl_neg_succ Int.shiftl_negSucc +#align int.shiftl_neg_succ Int.shiftLeft_negSucc @[simp] -theorem shiftr_negSucc (m n : ℕ) : shiftr -[m+1] n = -[m >>> n+1] := by cases n <;> rfl -#align int.shiftr_neg_succ Int.shiftr_negSucc +theorem shiftRight_negSucc (m n : ℕ) : -[m+1] >>> (n : ℤ) = -[m >>> n+1] := by cases n <;> rfl +#align int.shiftr_neg_succ Int.shiftRight_negSucc -theorem shiftr_add : ∀ (m : ℤ) (n k : ℕ), shiftr m (n + k) = shiftr (shiftr m n) k +theorem shiftRight_add : ∀ (m : ℤ) (n k : ℕ), m >>> (n + k : ℤ) = (m >>> (n : ℤ)) >>> (k : ℤ) | (m : ℕ), n, k => by - rw [shiftr_coe_nat, shiftr_coe_nat, ← Int.ofNat_add, shiftr_coe_nat, Nat.shiftRight_add] + rw [shiftRight_coe_nat, shiftRight_coe_nat, ← Int.ofNat_add, shiftRight_coe_nat, + Nat.shiftRight_add] | -[m+1], n, k => by - rw [shiftr_negSucc, shiftr_negSucc, ← Int.ofNat_add, shiftr_negSucc, Nat.shiftRight_add] -#align int.shiftr_add Int.shiftr_add + rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.ofNat_add, shiftRight_negSucc, + Nat.shiftRight_add] +#align int.shiftr_add Int.shiftRight_add /-! ### bitwise ops -/ attribute [local simp] Int.zero_div -theorem shiftl_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), shiftl m (n + k) = shiftl (shiftl m n) k +theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<< (n : ℤ)) <<< k | (m : ℕ), n, (k : ℕ) => congr_arg ofNat (by simp [Nat.pow_add, mul_assoc]) | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftLeft'_add _ _ _ _) | (m : ℕ), n, -[k+1] => - subNatNat_elim n k.succ (fun n k i => shiftl (↑m) i = (Nat.shiftLeft' false m n) >>> k) + subNatNat_elim n k.succ (fun n k i => (↑m) <<< i = (Nat.shiftLeft' false m n) >>> k) (fun (i n : ℕ) => by dsimp; simp [- Nat.shiftLeft_eq, ← Nat.shiftLeft_sub _ , add_tsub_cancel_left]) - fun i n => - by dsimp; simp [- Nat.shiftLeft_eq, Nat.shiftLeft_zero, Nat.shiftRight_add, - ← Nat.shiftLeft_sub, shiftl] + fun i n => by + dsimp + simp [- Nat.shiftLeft_eq, Nat.shiftLeft_zero, Nat.shiftRight_add, ← Nat.shiftLeft_sub] + rfl | -[m+1], n, -[k+1] => subNatNat_elim n k.succ - (fun n k i => shiftl -[m+1] i = -[(Nat.shiftLeft' true m n) >>> k+1]) + (fun n k i => -[m+1] <<< i = -[(Nat.shiftLeft' true m n) >>> k+1]) (fun i n => congr_arg negSucc <| by rw [← Nat.shiftLeft'_sub, add_tsub_cancel_left]; apply Nat.le_add_right) fun i n => congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub, tsub_self] <;> rfl -#align int.shiftl_add Int.shiftl_add +#align int.shiftl_add Int.shiftLeft_add -theorem shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (shiftl m n) k := - shiftl_add _ _ _ -#align int.shiftl_sub Int.shiftl_sub +theorem shiftLeft_sub (m : ℤ) (n : ℕ) (k : ℤ) : m <<< (n - k) = (m <<< (n : ℤ)) >>> k := + shiftLeft_add _ _ _ +#align int.shiftl_sub Int.shiftLeft_sub -theorem shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * ↑(2 ^ n) +theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * ↑(2 ^ n) | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp) | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _) -#align int.shiftl_eq_mul_pow Int.shiftl_eq_mul_pow +#align int.shiftl_eq_mul_pow Int.shiftLeft_eq_mul_pow -theorem shiftr_eq_div_pow : ∀ (m : ℤ) (n : ℕ), shiftr m n = m / ↑(2 ^ n) - | (m : ℕ), n => by rw [shiftr_coe_nat, Nat.shiftRight_eq_div_pow _ _]; simp +theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / ↑(2 ^ n) + | (m : ℕ), n => by rw [shiftRight_coe_nat, Nat.shiftRight_eq_div_pow _ _]; simp | -[m+1], n => by - rw [shiftr_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; rfl + rw [shiftRight_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; rfl exact ofNat_lt_ofNat_of_lt (pow_pos (by decide) _) -#align int.shiftr_eq_div_pow Int.shiftr_eq_div_pow +#align int.shiftr_eq_div_pow Int.shiftRight_eq_div_pow -theorem one_shiftl (n : ℕ) : shiftl 1 n = (2 ^ n : ℕ) := +theorem one_shiftLeft (n : ℕ) : 1 <<< (n : ℤ) = (2 ^ n : ℕ) := congr_arg ((↑) : ℕ → ℤ) (by simp) -#align int.one_shiftl Int.one_shiftl +#align int.one_shiftl Int.one_shiftLeft @[simp] -theorem zero_shiftl : ∀ n : ℤ, shiftl 0 n = 0 +theorem zero_shiftLeft : ∀ n : ℤ, 0 <<< n = 0 | (n : ℕ) => congr_arg ((↑) : ℕ → ℤ) (by simp) | -[_+1] => congr_arg ((↑) : ℕ → ℤ) (by simp) -#align int.zero_shiftl Int.zero_shiftl +#align int.zero_shiftl Int.zero_shiftLeft @[simp] -theorem zero_shiftr (n) : shiftr 0 n = 0 := - zero_shiftl _ -#align int.zero_shiftr Int.zero_shiftr +theorem zero_shiftRight (n : ℤ) : 0 >>> n = 0 := + zero_shiftLeft _ +#align int.zero_shiftr Int.zero_shiftRight end Int diff --git a/Mathlib/Init/Data/Int/Bitwise.lean b/Mathlib/Init/Data/Int/Bitwise.lean index 6eceaea4b4f74..8c91008bfdcb5 100644 --- a/Mathlib/Init/Data/Int/Bitwise.lean +++ b/Mathlib/Init/Data/Int/Bitwise.lean @@ -101,19 +101,20 @@ def lxor' : ℤ → ℤ → ℤ | -[m +1], -[n +1] => Nat.lxor' m n #align int.lxor Int.lxor' -/-- `shiftl m n` produces an integer whose binary representation +/-- `m <<< n` produces an integer whose binary representation is obtained by left-shifting the binary representation of `m` by `n` places -/ -def shiftl : ℤ → ℤ → ℤ +instance : ShiftLeft ℤ where + shiftLeft | (m : ℕ), (n : ℕ) => Nat.shiftLeft' false m n | (m : ℕ), -[n +1] => m >>> (Nat.succ n) | -[m +1], (n : ℕ) => -[Nat.shiftLeft' true m n +1] | -[m +1], -[n +1] => -[m >>> (Nat.succ n) +1] -#align int.shiftl Int.shiftl +#align int.shiftl ShiftLeft.shiftLeft -/-- `shiftr m n` produces an integer whose binary representation +/-- `m >>> n` produces an integer whose binary representation is obtained by right-shifting the binary representation of `m` by `n` places -/ -def shiftr (m n : ℤ) : ℤ := - shiftl m (-n) -#align int.shiftr Int.shiftr +instance : ShiftRight ℤ where + shiftRight m n := m <<< (-n) +#align int.shiftr ShiftRight.shiftRight end Int