From 93bcc03c5df0247deb02ddb336c811ad0a664ffd Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 27 Aug 2023 08:28:28 +0000 Subject: [PATCH] chore: rename `Nat.shiftl'` to `Nat.shiftLeft'` (#6788) This makes it match the unprimed `Nat.shiftLeft`. Follows on from #6356 which removed `Nat.shiftl`. --- Mathlib/Data/Int/Bitwise.lean | 14 +++++------ Mathlib/Data/Nat/Bits.lean | 2 +- Mathlib/Data/Nat/Size.lean | 39 +++++++++++++++--------------- Mathlib/Init/Data/Int/Bitwise.lean | 4 +-- Mathlib/Init/Data/Nat/Bitwise.lean | 30 +++++++++++------------ 5 files changed, 45 insertions(+), 44 deletions(-) diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index 58d9297e80e82..e11d7165673b4 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -385,7 +385,7 @@ theorem shiftr_coe_nat (m n : ℕ) : shiftr m n = m >>> n := by cases n <;> rfl #align int.shiftr_coe_nat Int.shiftr_coe_nat @[simp] -theorem shiftl_negSucc (m n : ℕ) : shiftl -[m+1] n = -[Nat.shiftl' true m n+1] := +theorem shiftl_negSucc (m n : ℕ) : shiftl -[m+1] n = -[Nat.shiftLeft' true m n+1] := rfl #align int.shiftl_neg_succ Int.shiftl_negSucc @@ -407,9 +407,9 @@ attribute [local simp] Int.zero_div theorem shiftl_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), shiftl m (n + k) = shiftl (shiftl m n) k | (m : ℕ), n, (k : ℕ) => congr_arg ofNat (by simp [Nat.pow_add, mul_assoc]) - | -[m+1], n, (k : ℕ) => congr_arg negSucc (Nat.shiftl'_add _ _ _ _) + | -[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.shiftl' false m n) >>> k) + subNatNat_elim n k.succ (fun n k i => shiftl (↑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 => @@ -417,12 +417,12 @@ theorem shiftl_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), shiftl m (n + k) = shift ← Nat.shiftLeft_sub, shiftl] | -[m+1], n, -[k+1] => subNatNat_elim n k.succ - (fun n k i => shiftl -[m+1] i = -[(Nat.shiftl' true m n) >>> k+1]) + (fun n k i => shiftl -[m+1] i = -[(Nat.shiftLeft' true m n) >>> k+1]) (fun i n => congr_arg negSucc <| by - rw [← Nat.shiftl'_sub, add_tsub_cancel_left]; apply Nat.le_add_right) + 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.shiftl'_sub, tsub_self] + congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub, tsub_self] <;> rfl #align int.shiftl_add Int.shiftl_add @@ -432,7 +432,7 @@ theorem shiftl_sub (m : ℤ) (n : ℕ) (k : ℤ) : shiftl m (n - k) = shiftr (sh theorem shiftl_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), shiftl m n = m * ↑(2 ^ n) | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp) - | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftl'_tt_eq_mul_pow _ _) + | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _) #align int.shiftl_eq_mul_pow Int.shiftl_eq_mul_pow theorem shiftr_eq_div_pow : ∀ (m : ℤ) (n : ℕ), shiftr m n = m / ↑(2 ^ n) diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean index 8d78efb3a6770..3fcccc90f5462 100644 --- a/Mathlib/Data/Nat/Bits.lean +++ b/Mathlib/Data/Nat/Bits.lean @@ -17,7 +17,7 @@ which allows us to more easily work with operations which do depend on the number of leading zeros in the binary representation of `n`. For example, we can more easily work with `Nat.bits` and `Nat.size`. -See also: `Nat.bitwise`, `Nat.pow` (for various lemmas about `size` and `shiftl`/`shiftr`), +See also: `Nat.bitwise`, `Nat.pow` (for various lemmas about `size` and `shiftLeft`/`shiftRight`), and `Nat.digits`. -/ diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean index 17c8483a37746..93c8a60ad3505 100644 --- a/Mathlib/Data/Nat/Size.lean +++ b/Mathlib/Data/Nat/Size.lean @@ -12,7 +12,7 @@ import Mathlib.Data.Nat.Bits namespace Nat -/-! ### `shiftl` and `shiftr` -/ +/-! ### `shiftLeft` and `shiftRight` -/ section set_option linter.deprecated false @@ -20,14 +20,14 @@ set_option linter.deprecated false theorem shiftLeft_eq_mul_pow (m) : ∀ n, m <<< n = m * 2 ^ n := shiftLeft_eq _ #align nat.shiftl_eq_mul_pow Nat.shiftLeft_eq_mul_pow -theorem shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' true m n + 1 = (m + 1) * 2 ^ n - | 0 => by simp [shiftl', pow_zero, Nat.one_mul] +theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1) * 2 ^ n + | 0 => by simp [shiftLeft', pow_zero, Nat.one_mul] | k + 1 => by - change bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2) + change bit1 (shiftLeft' true m k) + 1 = (m + 1) * (2 ^ k * 2) rw [bit1_val] - change 2 * (shiftl' true m k + 1) = _ - rw [shiftl'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2] -#align nat.shiftl'_tt_eq_mul_pow Nat.shiftl'_tt_eq_mul_pow + change 2 * (shiftLeft' true m k + 1) = _ + rw [shiftLeft'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2] +#align nat.shiftl'_tt_eq_mul_pow Nat.shiftLeft'_tt_eq_mul_pow end @@ -43,14 +43,14 @@ theorem shiftRight_eq_div_pow (m) : ∀ n, m >>> n = m / 2 ^ n simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ] #align nat.shiftr_eq_div_pow Nat.shiftRight_eq_div_pow -theorem shiftl'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftl' b m n ≠ 0 := by - induction n <;> simp [bit_ne_zero, shiftl', *] -#align nat.shiftl'_ne_zero_left Nat.shiftl'_ne_zero_left +theorem shiftLeft'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftLeft' b m n ≠ 0 := by + induction n <;> simp [bit_ne_zero, shiftLeft', *] +#align nat.shiftl'_ne_zero_left Nat.shiftLeft'_ne_zero_left -theorem shiftl'_tt_ne_zero (m) : ∀ {n}, (n ≠ 0) → shiftl' true m n ≠ 0 +theorem shiftLeft'_tt_ne_zero (m) : ∀ {n}, (n ≠ 0) → shiftLeft' true m n ≠ 0 | 0, h => absurd rfl h | succ _, _ => Nat.bit1_ne_zero _ -#align nat.shiftl'_tt_ne_zero Nat.shiftl'_tt_ne_zero +#align nat.shiftl'_tt_ne_zero Nat.shiftLeft'_tt_ne_zero /-! ### `size` -/ @@ -90,27 +90,28 @@ theorem size_one : size 1 = 1 := end @[simp] -theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) : size (shiftl' b m n) = size m + n := by - induction' n with n IH <;> simp [shiftl'] at h ⊢ +theorem size_shiftLeft' {b m n} (h : shiftLeft' b m n ≠ 0) : + size (shiftLeft' b m n) = size m + n := by + induction' n with n IH <;> simp [shiftLeft'] at h ⊢ rw [size_bit h, Nat.add_succ] - by_cases s0 : shiftl' b m n = 0 <;> [skip; rw [IH s0]] + by_cases s0 : shiftLeft' b m n = 0 <;> [skip; rw [IH s0]] rw [s0] at h ⊢ cases b; · exact absurd rfl h - have : shiftl' true m n + 1 = 1 := congr_arg (· + 1) s0 - rw [shiftl'_tt_eq_mul_pow] at this + have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0 + rw [shiftLeft'_tt_eq_mul_pow] at this obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩) simp only [zero_add, one_mul] at this obtain rfl : n = 0 := Nat.eq_zero_of_le_zero (le_of_not_gt fun hn => ne_of_gt (pow_lt_pow_of_lt_right (by decide) hn) this) rfl -#align nat.size_shiftl' Nat.size_shiftl' +#align nat.size_shiftl' Nat.size_shiftLeft' -- TODO: decide whether `Nat.shiftLeft_eq` (which rewrites the LHS into a power) should be a simp -- lemma; it was not in mathlib3. Until then, tell the simpNF linter to ignore the issue. @[simp, nolint simpNF] theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n := - by simp only [size_shiftl' (shiftl'_ne_zero_left _ h _), ← shiftl'_false] + by simp only [size_shiftLeft' (shiftLeft'_ne_zero_left _ h _), ← shiftLeft'_false] #align nat.size_shiftl Nat.size_shiftLeft theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by diff --git a/Mathlib/Init/Data/Int/Bitwise.lean b/Mathlib/Init/Data/Int/Bitwise.lean index cb1d2b4c1d698..6eceaea4b4f74 100644 --- a/Mathlib/Init/Data/Int/Bitwise.lean +++ b/Mathlib/Init/Data/Int/Bitwise.lean @@ -104,9 +104,9 @@ def lxor' : ℤ → ℤ → ℤ /-- `shiftl m n` produces an integer whose binary representation is obtained by left-shifting the binary representation of `m` by `n` places -/ def shiftl : ℤ → ℤ → ℤ - | (m : ℕ), (n : ℕ) => Nat.shiftl' false m n + | (m : ℕ), (n : ℕ) => Nat.shiftLeft' false m n | (m : ℕ), -[n +1] => m >>> (Nat.succ n) - | -[m +1], (n : ℕ) => -[Nat.shiftl' true m n +1] + | -[m +1], (n : ℕ) => -[Nat.shiftLeft' true m n +1] | -[m +1], -[n +1] => -[m >>> (Nat.succ n) +1] #align int.shiftl Int.shiftl diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean index be537af7def5d..51a17ab3be68d 100644 --- a/Mathlib/Init/Data/Nat/Bitwise.lean +++ b/Mathlib/Init/Data/Nat/Bitwise.lean @@ -180,21 +180,21 @@ theorem bit_zero : bit false 0 = 0 := rfl #align nat.bit_zero Nat.bit_zero -/--`shiftl' b m n` performs a left shift of `m` `n` times +/--`shiftLeft' b m n` performs a left shift of `m` `n` times and adds the bit `b` as the least significant bit each time. Returns the corresponding natural number-/ -def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ +def shiftLeft' (b : Bool) (m : ℕ) : ℕ → ℕ | 0 => m - | n + 1 => bit b (shiftl' b m n) -#align nat.shiftl' Nat.shiftl' + | n + 1 => bit b (shiftLeft' b m n) +#align nat.shiftl' Nat.shiftLeft' @[simp] -theorem shiftl'_false : ∀ n, shiftl' false m n = m <<< n +theorem shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n | 0 => rfl | n + 1 => by have : 2 * (m * 2^n) = 2^(n+1)*m := by rw [Nat.mul_comm, Nat.mul_assoc, ← pow_succ]; simp - simp [shiftl', bit_val, shiftl'_false, this] + simp [shiftLeft', bit_val, shiftLeft'_false, this] /-- Std4 takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/ @[simp] @@ -318,28 +318,28 @@ theorem div2_bit (b n) : div2 (bit b n) = n := by <;> exact by decide #align nat.div2_bit Nat.div2_bit -theorem shiftl'_add (b m n) : ∀ k, shiftl' b m (n + k) = shiftl' b (shiftl' b m n) k +theorem shiftLeft'_add (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k | 0 => rfl - | k + 1 => congr_arg (bit b) (shiftl'_add b m n k) -#align nat.shiftl'_add Nat.shiftl'_add + | k + 1 => congr_arg (bit b) (shiftLeft'_add b m n k) +#align nat.shiftl'_add Nat.shiftLeft'_add theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k := by - intro k; simp only [← shiftl'_false, shiftl'_add] + intro k; simp only [← shiftLeft'_false, shiftLeft'_add] theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k | 0 => rfl | k + 1 => by simp [add_succ, shiftRight_add] -theorem shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = (shiftl' b m n) >>> k +theorem shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (shiftLeft' b m n) >>> k | n, 0, _ => rfl | n + 1, k + 1, h => by - rw [succ_sub_succ_eq_sub, shiftl', Nat.add_comm, shiftRight_add] - simp only [shiftl'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero] + rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add] + simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero] simp [← div2_val, div2_bit] -#align nat.shiftl'_sub Nat.shiftl'_sub +#align nat.shiftl'_sub Nat.shiftLeft'_sub theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k := - fun _ _ _ hk => by simp only [← shiftl'_false, shiftl'_sub false _ hk] + fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk] @[simp] theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=