chore(Algebra/Group/Defs): use Nat.binaryRec

Mathlib/Algebra/Group/Defs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 import Mathlib.Data.Int.Notation
+import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Algebra.Group.ZeroOne
 import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.Lemma
@@ -583,40 +584,16 @@ needed. These problems do not come up in practice, so most of the time we will n
 the `npow` field when defining multiplicative objects.
 -/
 
-/--
-Scalar multiplication by repeated self-addition,
-the additive version of exponentation by repeated squaring.
--/
--- Ideally this would be generated by `@[to_additive]` from `npowBinRec`.
-def nsmulBinRec {M : Type*} [Zero M] [Add M] (k : ℕ) (m : M) : M :=
-  go k 0 m
-where
-  /-- Auxiliary tail-recursive implementation for `nsmulBinRec`-/
-  go : ℕ → M → M → M
-  | 0, y, _ => y
-  | (k + 1), y, x =>
-    let k' := (k + 1) >>> 1
-    if k &&& 1 = 1 then
-      go k' y (x + x)
-    else
-      go k' (y + x) (x + x)
-
 /-- Exponentiation by repeated squaring. -/
-@[to_additive existing]
-def npowBinRec {M : Type*} [One M] [Mul M] (k : ℕ) (m : M) : M :=
-  go k 1 m
+@[to_additive "Scalar multiplication by repeated self-addition,
+the additive version of exponentation by repeated squaring."]
+def npowBinRec {M : Type*} [One M] [Mul M] (k : ℕ) : M → M :=
+  npowBinRec.go k 1
 where
-  /-- Auxiliary tail-recursive implementation for `npowBinRec`-/
-  go : ℕ → M → M → M
-  | 0, y, _ => y
-  | (k + 1), y, x =>
-    let k' := (k + 1) >>> 1
-    if k &&& 1 = 1 then
-      go k' y (x * x)
-    else
-      go k' (y * x) (x * x)
-
-attribute [to_additive existing] npowBinRec.go
+  /-- Auxiliary tail-recursive implementation for `npowBinRec`. -/
+  @[to_additive nsmulBinRec.go "Auxiliary tail-recursive implementation for `nsmulBinRec`."]
+  go (k : ℕ) : M → M → M :=
+    k.binaryRec (fun y _ ↦ y) fun bn _n fn y x ↦ fn (cond bn (y * x) y) (x * x)
 
 /--
 A variant of `npowRec` which is a semigroup homomorphisms from `ℕ₊` to `M`.
@@ -637,9 +614,10 @@ def nsmulRec' {M : Type*} [Zero M] [Add M] : ℕ → M → M
 attribute [to_additive existing] npowRec'
 
 @[to_additive]
-theorem npowRec'_succ {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
-    npowRec' (k + 2) m = npowRec' (k + 1) m * m := by
-  rfl
+theorem npowRec'_succ {M : Type*} [Semigroup M] [One M] {k : ℕ} (_ : k ≠ 0) (m : M) :
+    npowRec' (k + 1) m = npowRec' k m * m :=
+  match k with
+  | _ + 1 => rfl
 
 @[to_additive]
 theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
@@ -652,12 +630,11 @@ theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
     | k + 2 => simp [npowRec', ← mul_assoc, ← ih]
 
 @[to_additive]
-theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
-    m * npowRec' (k + 1) m = npowRec' (k + 1) m * m := by
+theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :
+    m * npowRec' k m = npowRec' k m * m := by
   induction k using Nat.strongRecOn with
   | ind k' ih =>
     match k' with
-    | 0 => rfl
     | 1 => simp [npowRec', mul_assoc]
     | k + 2 => simp [npowRec', ← mul_assoc, ih]
 
@@ -669,41 +646,25 @@ theorem npowRec_eq {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
     match k' with
     | 0 => rfl
     | k + 1 =>
-      rw [npowRec, npowRec'_succ, ← mul_assoc]
+      rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
       congr
       simp [ih]
 
 @[to_additive]
 theorem npowBinRec.go_spec {M : Type*} [Semigroup M] [One M] (k : ℕ) (m n : M) :
     npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n := by
-  induction k using Nat.strongRecOn generalizing m n with
-  | ind k' ih =>
-    cases k' with
-    | zero => simp [go, npowRec']
-    | succ k' =>
-      rw [go]
-      split <;> rename_i w <;> rw [(by omega : (k' + 1 + 1) >>> 1 = k' >>> 1 + 1)]
-      · rw [ih]
-        · congr 1
-          rw [← npowRec'_two_mul]
-          congr 1
-          rw [Nat.shiftRight_eq_div_pow, Nat.pow_one, Nat.mul_add, Nat.mul_div_cancel']
-          simp only [Nat.and_one_is_mod] at w
-          omega
-        · omega
-      · rw [ih]
-        · rw [mul_assoc]
-          rw [← npowRec'_two_mul]
-          congr 1
-          conv =>
-            rhs
-            rw [npowRec']
-          rw [← npowRec'_mul_comm]
-          congr 2
-          · rw [Nat.shiftRight_eq_div_pow, Nat.pow_one]
-            simp only [Nat.and_one_is_mod] at w
-            omega
-        · omega
+  unfold go
+  generalize hk : k + 1 = k'
+  replace hk : k' ≠ 0 := by omega
+  induction k' using Nat.binaryRecFromOne generalizing n m with
+  | z₀ => simp at hk
+  | z₁ => simp [npowRec']
+  | f b k' k'0 ih =>
+    rw [Nat.binaryRec_eq rfl, ih _ _ k'0]
+    cases b <;> simp only [Nat.bit, cond_false, cond_true, ← Nat.two_mul, npowRec'_two_mul]
+    rw [npowRec'_succ (by omega), npowRec'_two_mul, ← npowRec'_two_mul,
+      ← npowRec'_mul_comm (by omega), mul_assoc]
+
 /--
 An abbreviation for `npowRec` with an additional typeclass assumption on associativity
 so that we can use `@[csimp]` to replace it with an implementation by repeated squaring
@@ -727,20 +688,12 @@ as an automatic parameter."]
 abbrev npowBinRecAuto {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M :=
   npowBinRec k m
 
-@[csimp]
-theorem nsmulRec_eq_nsmulBinRec : @nsmulRecAuto = @nsmulBinRecAuto := by
-  funext M _ _ k m
-  rw [nsmulBinRecAuto, nsmulRecAuto, nsmulBinRec]
-  match k with
-  | 0 => rw [nsmulRec, nsmulBinRec.go]
-  | k + 1 => rw [nsmulBinRec.go_spec, nsmulRec_eq]
-
-@[csimp]
+@[to_additive (attr := csimp)]
 theorem npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto := by
   funext M _ _ k m
   rw [npowBinRecAuto, npowRecAuto, npowBinRec]
   match k with
-  | 0 => rw [npowRec, npowBinRec.go]
+  | 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
   | k + 1 => rw [npowBinRec.go_spec, npowRec_eq]
 
 /-- An `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`. -/