chore: redefine Nat.div2 Nat.bodd

Mathlib/Computability/Primrec.lean

@@ -798,7 +798,7 @@ instance sum : Primcodable (α ⊕ β) :=
                 to₂ <| nat_double.comp (Primrec.encode.comp snd)))).of_eq
         fun n =>
         show _ = encode (decodeSum n) by
-          simp only [decodeSum, Nat.boddDiv2_eq]
+          simp only [decodeSum]
           cases Nat.bodd n <;> simp [decodeSum]
           · cases @decode α _ n.div2 <;> rfl
           · cases @decode β _ n.div2 <;> rfl⟩

Mathlib/Data/Int/Bitwise.lean

@@ -197,9 +197,7 @@ theorem bodd_bit (b n) : bodd (bit b n) = b := by
 theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
   | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
   | -[n+1] => by
-    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero
-    cases b <;>
-      rfl
+    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero, Bool.not_not]
 
 @[simp]
 theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m

Mathlib/Data/Nat/Bits.lean

@@ -3,12 +3,11 @@ Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Praneeth Kolichala
 -/
-import Mathlib.Data.Nat.Basic
-import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.List.Defs
+import Mathlib.Data.Nat.BinaryRec
+import Mathlib.Data.Nat.Init
+import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.Convert
-import Mathlib.Tactic.GeneralizeProofs
-import Mathlib.Tactic.Says
 
 /-!
 # Additional properties of binary recursion on `Nat`
@@ -34,6 +33,7 @@ variable {m n : ℕ}
 
 /-- `boddDiv2 n` returns a 2-tuple of type `(Bool, Nat)` where the `Bool` value indicates whether
 `n` is odd or not and the `Nat` value returns `⌊n/2⌋` -/
+@[deprecated "use `Nat.bodd` and `Nat.div2` instead" (since := "2024-06-09")]
 def boddDiv2 : ℕ → Bool × ℕ
   | 0 => (false, 0)
   | succ n =>
@@ -42,10 +42,12 @@ def boddDiv2 : ℕ → Bool × ℕ
     | (true, m) => (false, succ m)
 
 /-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2` -/
-def div2 (n : ℕ) : ℕ := (boddDiv2 n).2
+def div2 (n : ℕ) : ℕ := n >>> 1
+
+theorem div2_val (n) : div2 n = n / 2 := rfl
 
 /-- `bodd n` returns `true` if `n` is odd -/
-def bodd (n : ℕ) : Bool := (boddDiv2 n).1
+def bodd (n : ℕ) : Bool := 1 &&& n != 0
 
 @[simp] lemma bodd_zero : bodd 0 = false := rfl
 
@@ -55,9 +57,8 @@ lemma bodd_two : bodd 2 = false := rfl
 
 @[simp]
 lemma bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
-  simp only [bodd, boddDiv2]
-  let ⟨b,m⟩ := boddDiv2 n
-  cases b <;> rfl
+  simp only [bodd, succ_eq_add_one, one_and_eq_mod_two]
+  cases mod_two_eq_zero_or_one n with | _ h => simp [h, add_mod]
 
 @[simp]
 lemma bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by
@@ -73,19 +74,13 @@ lemma bodd_mul (m n : ℕ) : bodd (m * n) = (bodd m && bodd n) := by
     simp only [mul_succ, bodd_add, IH, bodd_succ]
     cases bodd m <;> cases bodd n <;> rfl
 
-lemma mod_two_of_bodd (n : ℕ) : n % 2 = (bodd n).toNat := by
-  have := congr_arg bodd (mod_add_div n 2)
-  simp? [not] at this says
-    simp only [bodd_add, bodd_mul, bodd_succ, not, bodd_zero, Bool.false_and, Bool.bne_false]
-      at this
-  have _ : ∀ b, and false b = false := by
-    intro b
-    cases b <;> rfl
-  have _ : ∀ b, bxor b false = b := by
-    intro b
-    cases b <;> rfl
-  rw [← this]
-  rcases mod_two_eq_zero_or_one n with h | h <;> rw [h] <;> rfl
+@[simp]
+lemma bodd_bit (b n) : bodd (bit b n) = b := by
+  cases b <;> simp [bodd]
+
+lemma mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
+  cases n using bitCasesOn with
+  | h b n => cases b <;> simp
 
 @[simp] lemma div2_zero : div2 0 = 0 := rfl
 
@@ -95,24 +90,18 @@ lemma div2_two : div2 2 = 1 := rfl
 
 @[simp]
 lemma div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n) := by
-  simp only [bodd, boddDiv2, div2]
-  rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp
+  cases n using bitCasesOn with
+  | h b n => cases b <;> simp [bit_val, div2_val, Nat.succ_div, Nat.dvd_mul_right]
+
+@[simp]
+lemma div2_bit (b n) : div2 (bit b n) = n := by
+  rw [div2_val, bit_div_two]
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
 
-lemma bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
-  | 0 => rfl
-  | succ n => by
-    simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]
-    refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))
-    cases bodd n
-    · simp
-    · simp; omega
-
-lemma div2_val (n) : div2 n = n / 2 := by
-  refine Nat.eq_of_mul_eq_mul_left (by decide)
-    (Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))
-  rw [mod_two_of_bodd, bodd_add_div2]
+lemma bodd_add_div2 (n : ℕ) : cond (bodd n) 1 0 + 2 * div2 n = n := by
+  cases n using bitCasesOn with
+  | h b n => simpa using (bit_val b n).symm
 
 lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
   (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
@@ -139,12 +128,10 @@ lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
 @[simp] lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl
 @[simp] lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl
 
-lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
-  rw [div2_val]
-  apply (div_lt_iff_lt_mul <| succ_pos 1).2
-  have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
-    (lt_of_le_of_ne n.zero_le h.symm)
-  rwa [Nat.mul_one] at this
+lemma div2_lt_self (h : n ≠ 0) : div2 n < n :=
+  div_lt_self (Nat.pos_iff_ne_zero.mpr h) Nat.one_lt_two
+
+@[deprecated (since := "2024-10-22")] alias binaryRec_decreasing := div2_lt_self
 
 /-- `size n` : Returns the size of a natural number in
 bits i.e. the length of its binary representation -/
@@ -164,17 +151,6 @@ def ldiff : ℕ → ℕ → ℕ :=
 
 /-! bitwise ops -/
 
-lemma bodd_bit (b n) : bodd (bit b n) = b := by
-  rw [bit_val]
-  simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false,
-    Bool.not_true, Bool.and_false, Bool.xor_false]
-  cases b <;> cases bodd n <;> rfl
-
-lemma div2_bit (b n) : div2 (bit b n) = n := by
-  rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
-  <;> cases b
-  <;> decide
-
 lemma 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) (shiftLeft'_add b m n k)
@@ -205,8 +181,14 @@ lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
 /-! ### `boddDiv2_eq` and `bodd` -/
 
 
-@[simp]
-theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := rfl
+set_option linter.deprecated false in
+@[deprecated "`Nat.boddDiv2` has been deprecated" (since := "2024-10-22")]
+theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [boddDiv2, ih]
+    cases hn : n.bodd <;> simp [hn]
 
 @[simp]
 theorem div2_bit0 (n) : div2 (2 * n) = n :=

Mathlib/Data/Nat/Bitwise.lean

@@ -59,21 +59,16 @@ lemma bitwise_zero : bitwise f 0 0 = 0 := by
   simp only [bitwise_zero_right, ite_self]
 
 lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
-    bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2)) := by
+    bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f n.div2 m.div2) := by
   conv_lhs => unfold bitwise
   have mod_two_iff_bod x : (x % 2 = 1 : Bool) = bodd x := by
     simp only [mod_two_of_bodd, cond]; cases bodd x <;> rfl
-  simp only [hn, hm, mod_two_iff_bod, ite_false, bit, two_mul, Bool.cond_eq_ite]
+  simp [hn, hm, mod_two_iff_bod, bit, div2_val, Nat.shiftLeft_succ, two_mul]
 
 theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n}
     (h : n ≠ 0) :
-    binaryRec z f n = bit_decomp n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n)) := by
-  cases n using bitCasesOn with
-  | h b n =>
-    rw [binaryRec_eq _ _ (by right; simpa [bit_eq_zero_iff] using h)]
-    generalize_proofs h; revert h
-    rw [bodd_bit, div2_bit]
-    simp
+    binaryRec z f n = n.bit_decomp ▸ f n.bodd n.div2 (binaryRec z f n.div2) := by
+  rw [binaryRec, dif_neg h, eqRec_eq_cast, eqRec_eq_cast]; rfl
 
 @[simp]
 lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) :
@@ -163,8 +158,8 @@ lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
     | z => simp only [bitwise_zero_right, binaryRec_zero, Bool.cond_eq_ite]
     | f yb y hyb =>
       rw [← bit_ne_zero_iff] at hyb
-      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, ← div2_val,
-        div2_bit, eq_rec_constant, ih]
+      simp_rw [binaryRec_of_ne_zero _ _ hyb, bitwise_of_ne_zero hxb hyb, bodd_bit, div2_bit,
+        eq_rec_constant, ih]
 
 theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n = 0 := by
   induction n using Nat.binaryRec with | z => rfl | f b n hn => ?_
@@ -239,12 +234,12 @@ theorem bitwise_swap {f : Bool → Bool → Bool} :
     bitwise (Function.swap f) = Function.swap (bitwise f) := by
   funext m n
   simp only [Function.swap]
-  induction m using Nat.strongRecOn generalizing n with | ind m ih => ?_
-  rcases m with - | m
-  <;> rcases n with - | n
-  <;> try rw [bitwise_zero_left, bitwise_zero_right]
-  · specialize ih ((m+1) / 2) (div_lt_self' ..)
-    simp [bitwise_of_ne_zero, ih]
+  induction m using Nat.binaryRec' generalizing n with
+  | z => simp
+  | f bm m hm ihm =>
+    induction n using Nat.binaryRec' with
+    | z => simp
+    | f bn n hn => rw [bitwise_bit' _ _ _ _ hm hn, bitwise_bit' _ _ _ _ hn hm, ihm]
 
 /-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
     is also commutative. -/

Mathlib/Data/Nat/Size.lean

@@ -3,8 +3,9 @@ Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.Group.Nat.Defs
+import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Bits
 
 /-! Lemmas about `size`. -/

Mathlib/Logic/Denumerable.lean

@@ -121,9 +121,8 @@ instance option : Denumerable (Option α) :=
 instance sum : Denumerable (α ⊕ β) :=
   ⟨fun n => by
     suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
-    simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some',
-      Option.mem_def, Sum.exists]
-    cases bodd n <;> simp [decodeSum, bit, encodeSum, Nat.two_mul]⟩
+    simp only [decodeSum, decode_eq_ofNat, Option.map_some', Option.mem_def, Sum.exists]
+    cases bodd n <;> simp [bit_val, encodeSum]⟩
 
 section Sigma
 

Mathlib/Logic/Encodable/Basic.lean

@@ -228,9 +228,9 @@ def encodeSum : α ⊕ β → ℕ
 
 /-- Explicit decoding function for the sum of two encodable types. -/
 def decodeSum (n : ℕ) : Option (α ⊕ β) :=
-  match boddDiv2 n with
-  | (false, m) => (decode m : Option α).map Sum.inl
-  | (_, m) => (decode m : Option β).map Sum.inr
+  match bodd n, div2 n with
+  | false, m => (decode m : Option α).map Sum.inl
+  | _, m => (decode m : Option β).map Sum.inr
 
 /-- If `α` and `β` are encodable, then so is their sum. -/
 instance _root_.Sum.encodable : Encodable (α ⊕ β) :=
@@ -278,7 +278,7 @@ theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none := by
     rw [Nat.le_div_iff_mul_le]
     exacts [h, by decide]
   obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)
-  simp only [decodeSum, boddDiv2_eq, div2_val]; cases bodd n <;> simp [e]
+  simp only [decodeSum, div2_val]; cases bodd n <;> simp [e]
 
 noncomputable instance _root_.Prop.encodable : Encodable Prop :=
   ofEquiv Bool Equiv.propEquivBool

Mathlib/Logic/Equiv/Nat.lean

@@ -26,9 +26,9 @@ variable {α : Type*}
 @[simps]
 def boolProdNatEquivNat : Bool × ℕ ≃ ℕ where
   toFun := uncurry bit
-  invFun := boddDiv2
-  left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair, boddDiv2_eq]
-  right_inv n := by simp only [bit_decomp, boddDiv2_eq, uncurry_apply_pair]
+  invFun n := ⟨n.bodd, n.div2⟩
+  left_inv := fun ⟨b, n⟩ => by simp only [bodd_bit, div2_bit, uncurry_apply_pair]
+  right_inv n := by simp only [bit_decomp, uncurry_apply_pair]
 
 /-- An equivalence between `ℕ ⊕ ℕ` and `ℕ`, by mapping `(Sum.inl x)` to `2 * x` and `(Sum.inr x)` to
 `2 * x + 1`.