[Merged by Bors] - refactor(data/nat/basic): move more bit theory out

src/data/int/bitwise.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad
 -/
 import data.int.basic
 import data.nat.pow
+import data.nat.size
 
 /-!
 # Bitwise operations on integers

src/data/nat/basic.lean

@@ -718,78 +718,6 @@ by simp [nat.find_greatest, h]
 
 end find_greatest
 
-/-! ### `bodd_div2` and `bodd` -/
-
-@[simp] theorem bodd_div2_eq (n : ℕ) : bodd_div2 n = (bodd n, div2 n) :=
-by unfold bodd div2; cases bodd_div2 n; refl
-
-@[simp] lemma bodd_bit0 (n) : bodd (bit0 n) = ff := bodd_bit ff n
-@[simp] lemma bodd_bit1 (n) : bodd (bit1 n) = tt := bodd_bit tt n
-
-@[simp] lemma div2_bit0 (n) : div2 (bit0 n) = n := div2_bit ff n
-@[simp] lemma div2_bit1 (n) : div2 (bit1 n) = n := div2_bit tt n
-
-/-! ### `bit0` and `bit1` -/
-
--- There is no need to prove `bit0_eq_zero : bit0 n = 0 ↔ n = 0`
--- as this is true for any `[semiring R] [no_zero_divisors R] [char_zero R]`
-
--- However the lemmas `bit0_eq_bit0`, `bit1_eq_bit1`, `bit1_eq_one`, `one_eq_bit1`
--- need `[ring R] [no_zero_divisors R] [char_zero R]` in general,
--- so we prove `ℕ` specialized versions here.
-@[simp] lemma bit0_eq_bit0 {m n : ℕ} : bit0 m = bit0 n ↔ m = n :=
-⟨nat.bit0_inj, λ h, by subst h⟩
-
-@[simp] lemma bit1_eq_bit1 {m n : ℕ} : bit1 m = bit1 n ↔ m = n :=
-⟨nat.bit1_inj, λ h, by subst h⟩
-
-@[simp] lemma bit1_eq_one {n : ℕ} : bit1 n = 1 ↔ n = 0 :=
-⟨@nat.bit1_inj n 0, λ h, by subst h⟩
-@[simp] lemma one_eq_bit1 {n : ℕ} : 1 = bit1 n ↔ n = 0 :=
-⟨λ h, (@nat.bit1_inj 0 n h).symm, λ h, by subst h⟩
-
-theorem bit_add : ∀ (b : bool) (n m : ℕ), bit b (n + m) = bit ff n + bit b m
-| tt := bit1_add
-| ff := bit0_add
-
-theorem bit_add' : ∀ (b : bool) (n m : ℕ), bit b (n + m) = bit b n + bit ff m
-| tt := bit1_add'
-| ff := bit0_add
-
-theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0 :=
-by cases b; [exact nat.bit0_ne_zero h, exact nat.bit1_ne_zero _]
-
-lemma bit0_mod_two : bit0 n % 2 = 0 := by { rw nat.mod_two_of_bodd, simp }
-
-lemma bit1_mod_two : bit1 n % 2 = 1 := by { rw nat.mod_two_of_bodd, simp }
-
-lemma pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n :=
-by { cases n, cases h, apply succ_pos, }
-
-@[simp] lemma bit_cases_on_bit {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (b : bool) (n : ℕ) :
-  bit_cases_on (bit b n) H = H b n :=
-eq_of_heq $ (eq_rec_heq _ _).trans $ by rw [bodd_bit, div2_bit]
-
-@[simp] lemma bit_cases_on_bit0 {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) :
-  bit_cases_on (bit0 n) H = H ff n :=
-bit_cases_on_bit H ff n
-
-@[simp] lemma bit_cases_on_bit1 {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) :
-  bit_cases_on (bit1 n) H = H tt n :=
-bit_cases_on_bit H tt n
-
-lemma bit_cases_on_injective {C : ℕ → Sort u} :
-  function.injective (λ H : Π b n, C (bit b n), λ n, bit_cases_on n H) :=
-begin
-  intros H₁ H₂ h,
-  ext b n,
-  simpa only [bit_cases_on_bit] using congr_fun h (bit b n)
-end
-
-@[simp] lemma bit_cases_on_inj {C : ℕ → Sort u} (H₁ H₂ : Π b n, C (bit b n)) :
-  (λ n, bit_cases_on n H₁) = (λ n, bit_cases_on n H₂) ↔ H₁ = H₂ :=
-bit_cases_on_injective.eq_iff
-
 /-! ### decidability of predicates -/
 
 instance decidable_ball_lt (n : nat) (P : Π k < n, Prop) :

src/data/nat/bits.lean

@@ -3,9 +3,7 @@ Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Praneeth Kolichala
 -/
-import tactic.generalize_proofs
-import tactic.norm_num
-import algebra.char_zero
+import data.nat.basic
 
 /-!
 # Additional properties of binary recursion on `nat`
@@ -21,8 +19,86 @@ and `nat.digits`.
 
 namespace nat
 
+universe u
+variables {n : ℕ}
+
+/-! ### `bodd_div2` and `bodd` -/
+
+@[simp] theorem bodd_div2_eq (n : ℕ) : bodd_div2 n = (bodd n, div2 n) :=
+by unfold bodd div2; cases bodd_div2 n; refl
+
+@[simp] lemma bodd_bit0 (n) : bodd (bit0 n) = ff := bodd_bit ff n
+@[simp] lemma bodd_bit1 (n) : bodd (bit1 n) = tt := bodd_bit tt n
+
+@[simp] lemma div2_bit0 (n) : div2 (bit0 n) = n := div2_bit ff n
+@[simp] lemma div2_bit1 (n) : div2 (bit1 n) = n := div2_bit tt n
+
+/-! ### `bit0` and `bit1` -/
+
+-- There is no need to prove `bit0_eq_zero : bit0 n = 0 ↔ n = 0`
+-- as this is true for any `[semiring R] [no_zero_divisors R] [char_zero R]`
+
+-- However the lemmas `bit0_eq_bit0`, `bit1_eq_bit1`, `bit1_eq_one`, `one_eq_bit1`
+-- need `[ring R] [no_zero_divisors R] [char_zero R]` in general,
+-- so we prove `ℕ` specialized versions here.
+@[simp] lemma bit0_eq_bit0 {m n : ℕ} : bit0 m = bit0 n ↔ m = n :=
+⟨nat.bit0_inj, λ h, by subst h⟩
+
+@[simp] lemma bit1_eq_bit1 {m n : ℕ} : bit1 m = bit1 n ↔ m = n :=
+⟨nat.bit1_inj, λ h, by subst h⟩
+
+@[simp] lemma bit1_eq_one {n : ℕ} : bit1 n = 1 ↔ n = 0 :=
+⟨@nat.bit1_inj n 0, λ h, by subst h⟩
+@[simp] lemma one_eq_bit1 {n : ℕ} : 1 = bit1 n ↔ n = 0 :=
+⟨λ h, (@nat.bit1_inj 0 n h).symm, λ h, by subst h⟩
+
+theorem bit_add : ∀ (b : bool) (n m : ℕ), bit b (n + m) = bit ff n + bit b m
+| tt := bit1_add
+| ff := bit0_add
+
+theorem bit_add' : ∀ (b : bool) (n m : ℕ), bit b (n + m) = bit b n + bit ff m
+| tt := bit1_add'
+| ff := bit0_add
+
+theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bit b n ≠ 0 :=
+by cases b; [exact nat.bit0_ne_zero h, exact nat.bit1_ne_zero _]
+
+lemma bit0_mod_two : bit0 n % 2 = 0 := by { rw nat.mod_two_of_bodd, simp }
+
+lemma bit1_mod_two : bit1 n % 2 = 1 := by { rw nat.mod_two_of_bodd, simp }
+
+lemma pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n :=
+by { cases n, cases h, apply succ_pos, }
+
+@[simp] lemma bit_cases_on_bit {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (b : bool) (n : ℕ) :
+  bit_cases_on (bit b n) H = H b n :=
+eq_of_heq $ (eq_rec_heq _ _).trans $ by rw [bodd_bit, div2_bit]
+
+@[simp] lemma bit_cases_on_bit0 {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) :
+  bit_cases_on (bit0 n) H = H ff n :=
+bit_cases_on_bit H ff n
+
+@[simp] lemma bit_cases_on_bit1 {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) :
+  bit_cases_on (bit1 n) H = H tt n :=
+bit_cases_on_bit H tt n
+
+lemma bit_cases_on_injective {C : ℕ → Sort u} :
+  function.injective (λ H : Π b n, C (bit b n), λ n, bit_cases_on n H) :=
+begin
+  intros H₁ H₂ h,
+  ext b n,
+  simpa only [bit_cases_on_bit] using congr_fun h (bit b n)
+end
+
+@[simp] lemma bit_cases_on_inj {C : ℕ → Sort u} (H₁ H₂ : Π b n, C (bit b n)) :
+  (λ n, bit_cases_on n H₁) = (λ n, bit_cases_on n H₂) ↔ H₁ = H₂ :=
+bit_cases_on_injective.eq_iff
+
+protected lemma bit0_eq_zero {n : ℕ} : bit0 n = 0 ↔ n = 0 :=
+⟨nat.eq_zero_of_add_eq_zero_left, λ h, by simp [h]⟩
+
 lemma bit_eq_zero_iff {n : ℕ} {b : bool} : bit b n = 0 ↔ n = 0 ∧ b = ff :=
-by { split, { cases b; simp [nat.bit], }, rintro ⟨rfl, rfl⟩, refl, }
+by { split, { cases b; simp [nat.bit, nat.bit0_eq_zero], }, rintro ⟨rfl, rfl⟩, refl, }
 
 /-- The same as binary_rec_eq, but that one unfortunately requires `f` to be the identity when
   appending `ff` to `0`. Here, we allow you to explicitly say that that case is not happening, i.e.
@@ -70,7 +146,8 @@ bits_append_bit n tt (λ _, rfl)
 
 @[simp] lemma one_bits : nat.bits 1 = [tt] := by { convert bit1_bits 0, simp, }
 
-example : bits 3423 = [tt, tt, tt, tt, tt, ff, tt, ff, tt, ff, tt, tt] := by norm_num
+-- TODO Find somewhere this can live.
+-- example : bits 3423 = [tt, tt, tt, tt, tt, ff, tt, ff, tt, ff, tt, tt] := by norm_num
 
 lemma bodd_eq_bits_head (n : ℕ) : n.bodd = n.bits.head :=
 begin
@@ -84,12 +161,4 @@ begin
   simp [div2_bit, bits_append_bit _ _ h],
 end
 
-lemma size_eq_bits_len (n : ℕ) : n.bits.length = n.size :=
-begin
-  induction n using nat.binary_rec' with b n h ih, { simp, },
-  rw [size_bit, bits_append_bit _ _ h],
-  { simp [ih], },
-  { simpa [bit_eq_zero_iff], }
-end
-
 end nat

src/data/nat/bitwise.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
+import data.list.basic
 import data.nat.bits
 import tactic.linarith
 
@@ -39,7 +40,7 @@ namespace nat
 @[simp] lemma bit_tt : bit tt = bit1 := rfl
 
 @[simp] lemma bit_eq_zero {n : ℕ} {b : bool} : n.bit b = 0 ↔ n = 0 ∧ b = ff :=
-by { cases b; norm_num [bit0_eq_zero, nat.bit1_ne_zero] }
+by { cases b; simp [nat.bit0_eq_zero, nat.bit1_ne_zero] }
 
 lemma zero_of_test_bit_eq_ff {n : ℕ} (h : ∀ i, test_bit n i = ff) : n = 0 :=
 begin

src/data/nat/pow.lean

@@ -200,127 +200,4 @@ begin
   exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n),
 end
 
-/-! ### `shiftl` and `shiftr` -/
-
-lemma shiftl_eq_mul_pow (m) : ∀ n, shiftl m n = m * 2 ^ n
-| 0     := (nat.mul_one _).symm
-| (k+1) := show bit0 (shiftl m k) = m * (2 * 2 ^ k),
-  by rw [bit0_val, shiftl_eq_mul_pow, mul_left_comm, mul_comm 2]
-
-lemma shiftl'_tt_eq_mul_pow (m) : ∀ n, shiftl' tt m n + 1 = (m + 1) * 2 ^ n
-| 0     := by simp [shiftl, shiftl', pow_zero, nat.one_mul]
-| (k+1) :=
-begin
-  change bit1 (shiftl' tt m k) + 1 = (m + 1) * (2 * 2 ^ k),
-  rw bit1_val,
-  change 2 * (shiftl' tt m k + 1) = _,
-  rw [shiftl'_tt_eq_mul_pow, mul_left_comm, mul_comm 2],
-end
-
-lemma one_shiftl (n) : shiftl 1 n = 2 ^ n :=
-(shiftl_eq_mul_pow _ _).trans (nat.one_mul _)
-
-@[simp] lemma zero_shiftl (n) : shiftl 0 n = 0 :=
-(shiftl_eq_mul_pow _ _).trans (nat.zero_mul _)
-
-lemma shiftr_eq_div_pow (m) : ∀ n, shiftr m n = m / 2 ^ n
-| 0     := (nat.div_one _).symm
-| (k+1) := (congr_arg div2 (shiftr_eq_div_pow k)).trans $
-           by rw [div2_val, nat.div_div_eq_div_mul, mul_comm]; refl
-
-@[simp] lemma zero_shiftr (n) : shiftr 0 n = 0 :=
-(shiftr_eq_div_pow _ _).trans (nat.zero_div _)
-
-theorem shiftl'_ne_zero_left (b) {m} (h : m ≠ 0) (n) : shiftl' b m n ≠ 0 :=
-by induction n; simp [shiftl', bit_ne_zero, *]
-
-theorem shiftl'_tt_ne_zero (m) : ∀ {n} (h : n ≠ 0), shiftl' tt m n ≠ 0
-| 0        h := absurd rfl h
-| (succ n) _ := nat.bit1_ne_zero _
-
-/-! ### `size` -/
-
-@[simp] theorem size_zero : size 0 = 0 := by simp [size]
-
-@[simp] theorem size_bit {b n} (h : bit b n ≠ 0) : size (bit b n) = succ (size n) :=
-begin
-  rw size,
-  conv { to_lhs, rw [binary_rec], simp [h] },
-  rw div2_bit,
-end
-
-@[simp] theorem size_bit0 {n} (h : n ≠ 0) : size (bit0 n) = succ (size n) :=
-@size_bit ff n (nat.bit0_ne_zero h)
-
-@[simp] theorem size_bit1 (n) : size (bit1 n) = succ (size n) :=
-@size_bit tt n (nat.bit1_ne_zero n)
-
-@[simp] theorem size_one : size 1 = 1 :=
-show size (bit1 0) = 1, by rw [size_bit1, size_zero]
-
-@[simp] theorem size_shiftl' {b m n} (h : shiftl' b m n ≠ 0) :
-  size (shiftl' b m n) = size m + n :=
-begin
-  induction n with n IH; simp [shiftl'] at h ⊢,
-  rw [size_bit h, nat.add_succ],
-  by_cases s0 : shiftl' b m n = 0; [skip, rw [IH s0]],
-  rw s0 at h ⊢,
-  cases b, {exact absurd rfl h},
-  have : shiftl' tt m n + 1 = 1 := congr_arg (+1) s0,
-  rw [shiftl'_tt_eq_mul_pow] at this,
-  obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩),
-  rw one_mul at this,
-  obtain rfl : n = 0 := nat.eq_zero_of_le_zero (le_of_not_gt $ λ hn,
-    ne_of_gt (pow_lt_pow_of_lt_right dec_trivial hn) this),
-  refl
-end
-
-@[simp] theorem size_shiftl {m} (h : m ≠ 0) (n) :
-  size (shiftl m n) = size m + n :=
-size_shiftl' (shiftl'_ne_zero_left _ h _)
-
-theorem lt_size_self (n : ℕ) : n < 2^size n :=
-begin
-  rw [← one_shiftl],
-  have : ∀ {n}, n = 0 → n < shiftl 1 (size n), { simp },
-  apply binary_rec _ _ n, {apply this rfl},
-  intros b n IH,
-  by_cases bit b n = 0, {apply this h},
-  rw [size_bit h, shiftl_succ],
-  exact bit_lt_bit0 _ IH
-end
-
-theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2^n :=
-⟨λ h, lt_of_lt_of_le (lt_size_self _) (pow_le_pow_of_le_right dec_trivial h),
-begin
-  rw [← one_shiftl], revert n,
-  apply binary_rec _ _ m,
-  { intros n h, simp },
-  { intros b m IH n h,
-    by_cases e : bit b m = 0, { simp [e] },
-    rw [size_bit e],
-    cases n with n,
-    { exact e.elim (nat.eq_zero_of_le_zero (le_of_lt_succ h)) },
-    { apply succ_le_succ (IH _),
-      apply lt_imp_lt_of_le_imp_le (λ h', bit0_le_bit _ h') h } }
-end⟩
-
-theorem lt_size {m n : ℕ} : m < size n ↔ 2^m ≤ n :=
-by rw [← not_lt, decidable.iff_not_comm, not_lt, size_le]
-
-theorem size_pos {n : ℕ} : 0 < size n ↔ 0 < n :=
-by rw lt_size; refl
-
-theorem size_eq_zero {n : ℕ} : size n = 0 ↔ n = 0 :=
-by have := @size_pos n; simp [pos_iff_ne_zero] at this;
-   exact decidable.not_iff_not.1 this
-
-theorem size_pow {n : ℕ} : size (2^n) = n+1 :=
-le_antisymm
-  (size_le.2 $ pow_lt_pow_of_lt_right dec_trivial (lt_succ_self _))
-  (lt_size.2 $ le_rfl)
-
-theorem size_le_size {m n : ℕ} (h : m ≤ n) : size m ≤ size n :=
-size_le.2 $ lt_of_le_of_lt h (lt_size_self _)
-
 end nat