feat: de-mathlib Nat.binaryRec

Std/Data/Nat/Basic.lean

@@ -130,11 +130,98 @@ where
       guess
 termination_by iter guess => guess
 
+/-- `bodd n` returns `true` if `n` is odd-/
+def bodd (n : Nat) : Bool :=
+  (1 &&& n) != 0 -- `1 &&& n` is faster than `n &&& 1` for big `n`. This may change in the future.
+
+/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
+def div2 (n : Nat) : Nat :=
+  n >>> 1
+
+/-- `bit b` appends the digit `b` to the binary representation of
+  its natural number input. -/
+def bit (b : Bool) (n : Nat) : Nat :=
+  cond b (n + n + 1) (n + n)
+
 /-!
 ### testBit
 We define an operation for testing individual bits in the binary representation
 of a number.
 -/
 
-/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
-def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
+/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
+def testBit (m n : Nat) : Bool :=
+  bodd (m >>> n)
+
+theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
+  cases b <;> rw [Nat.mul_comm]
+  · exact congrArg (· + n) n.zero_add.symm
+  · exact congrArg (· + n + 1) n.zero_add.symm
+
+theorem div2_val (n) : div2 n = n / 2 := rfl
+
+theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
+  match n % 2, @Nat.mod_lt n 2 (by decide) with
+  | 0, _ => .inl rfl
+  | 1, _ => .inr rfl
+
+theorem mod_two_of_bodd (n : Nat) : n % 2 = cond (bodd n) 1 0 := by
+  dsimp [bodd, (· &&& ·), AndOp.and, land]
+  unfold bitwise
+  match Nat.decEq n 0 with
+  | isTrue n0 => subst n0; decide
+  | isFalse n0 =>
+    simp only [ite_false, decide_True, Bool.true_and, decide_eq_true_eq, n0,
+      show 1 / 2 = 0 by decide]
+    cases mod_two_eq_zero_or_one n with | _ h => simp [h]; rfl
+
+theorem div2_add_bodd (n : Nat) : 2 * div2 n + cond (bodd n) 1 0 = n := by
+  rw [← mod_two_of_bodd, div2_val, Nat.div_add_mod]
+
+theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
+  (bit_val _ _).trans (div2_add_bodd _)
+
+theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
+  cases n <;> cases b <;> simp [bit, Nat.succ_add]
+
+/-- For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for any given natural number. -/
+@[inline]
+def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
+
+theorem binaryRec_decreasing (h : n ≠ 0) : div2 n < n :=
+  div_lt_self (n.zero_lt_of_ne_zero h) (by decide)
+
+/-- A recursion principle for `bit` representations of natural numbers.
+  For a predicate `C : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[elab_as_elim, specialize]
+def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) (n : Nat) : C n :=
+  if n0 : n = 0 then congrArg C n0 ▸ z -- `congrArg C _` is `rfl` in non-dependent case
+  else congrArg C n.bit_decomp ▸ f n.bodd n.div2 (binaryRec z f n.div2)
+  decreasing_by exact binaryRec_decreasing n0
+
+/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`-/
+@[elab_as_elim, specialize]
+def binaryRec' {C : Nat → Sort u} (z : C 0)
+    (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec z fun b n ih =>
+    if h : n = 0 → b = true then f b n h ih
+    else by
+      have : bit b n = 0 := by
+        rw [bit_eq_zero_iff]
+        cases n <;> cases b <;> simp at h <;> simp [h]
+      exact this ▸ z
+
+/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
+@[elab_as_elim, specialize]
+def binaryRecFromOne {C : Nat → Sort u} (z₀ : C 0) (z₁ : C 1)
+    (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) : ∀ n, C n :=
+  binaryRec' z₀ fun b n h ih =>
+    if h' : n = 0 then by
+      rw [h', h h']
+      exact z₁
+    else f b n h' ih

Std/Data/Nat/Bitwise.lean

@@ -19,6 +19,9 @@ namespace Nat
 @[local simp]
 private theorem one_div_two : 1/2 = 0 := by trivial
 
+private theorem decide_mod_two_eq_one {x : Nat} : decide (x % 2 = 1) = (x % 2 != 0) := by
+  cases mod_two_eq_zero_or_one x with | _ h => simp (config := {decide := true}) [h]
+
 private theorem two_pow_succ_sub_one_div : (2 ^ (n+1) - 1) / 2 = 2^n - 1 := by
   apply fun x => (Nat.sub_eq_of_eq_add x).symm
   apply Eq.trans _
@@ -34,101 +37,65 @@ private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 :=
 
 /-! ### Preliminaries -/
 
-/--
-An induction principal that works on divison by two.
--/
-noncomputable def div2Induction {motive : Nat → Sort u}
-    (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
-  induction n using Nat.strongInductionOn with
-  | ind n hyp =>
-    apply ind
-    intro n_pos
-    if n_eq : n = 0 then
-      simp [n_eq] at n_pos
-    else
-      apply hyp
-      exact Nat.div_lt_self n_pos (Nat.le_refl _)
-
 @[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
   unfold bitwise
   simp
 
-@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
+@[simp] theorem one_and_is_mod (x : Nat) : 1 &&& x = x % 2 := by
   if xz : x = 0 then
     simp [xz, zero_and]
   else
-    have andz := and_zero (x/2)
-    simp only [HAnd.hAnd, AndOp.and, land] at andz
     simp only [HAnd.hAnd, AndOp.and, land]
     unfold bitwise
-    cases mod_two_eq_zero_or_one x with | _ p =>
-      simp [xz, p, andz, one_div_two, mod_eq_of_lt]
+    cases mod_two_eq_zero_or_one x with | _ p => simp [xz, p]
 
 /-! ### testBit -/
 
 @[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
-  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
+  simp only [testBit, zero_shiftRight, bodd, and_zero, bne_self_eq_false]
 
-theorem testBit_zero_is_mod2 (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
-  cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
+theorem testBit_zero_is_bodd (x : Nat) : testBit x 0 = bodd x :=
+  rfl
 
-theorem testBit_succ_div2 (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+theorem testBit_succ_div_two (x i : Nat) : testBit x (i + 1) = testBit (x / 2) i := by
   unfold testBit
-  simp [shiftRight_succ_inside]
+  simp [shiftRight_succ_inside, div2]
 
 theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
     unfold testBit
-    cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]
+    cases mod_two_eq_zero_or_one x with | _ xz => simp [bodd, xz]
   | succ i hyp =>
-    simp [testBit_succ_div2, hyp,
+    simp [testBit_succ_div_two, hyp,
           Nat.div_div_eq_div_mul, Nat.pow_succ, Nat.mul_comm 2]
 
 theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
-  induction x using div2Induction with
-  | ind x hyp =>
-    have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
-    match mod_two_eq_zero_or_one x with
-    | Or.inl mod2_eq =>
-      rw [←div_add_mod x 2] at xnz
-      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
-      have ⟨d, dif⟩   := hyp x_pos xnz
-      apply Exists.intro (d+1)
-      simp [testBit_succ_div2, dif]
-    | Or.inr mod2_eq =>
-      apply Exists.intro 0
-      simp [testBit_zero_is_mod2, mod2_eq]
+  induction x using binaryRecFromOne with
+  | z₀ => exact absurd rfl xnz
+  | z₁ => exact ⟨0, rfl⟩
+  | f b n n0 hyp =>
+    obtain ⟨i, h⟩ := hyp n0
+    refine ⟨i + 1, ?_⟩
+    rwa [testBit_succ_div_two, bit_div_two]
 
 theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
-  induction y using Nat.div2Induction generalizing x with
-  | ind y hyp =>
-    cases Nat.eq_zero_or_pos y with
-    | inl yz =>
-      simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
-      simp only [yz] at p
-      have ⟨i,ip⟩  := ne_zero_implies_bit_true p
-      apply Exists.intro i
-      simp [ip]
-    | inr ypos =>
-      if lsb_diff : x % 2 = y % 2 then
-        rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
-        simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
-          Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
-        have ⟨i, ieq⟩  := hyp ypos p
-        apply Exists.intro (i+1)
-        simp [testBit_succ_div2]
-        exact ieq
-      else
-        apply Exists.intro 0
-        simp only [testBit_zero_is_mod2]
-        revert lsb_diff
-        cases mod_two_eq_zero_or_one x with | _ p =>
-          cases mod_two_eq_zero_or_one y with | _ q =>
-            simp [p,q]
+  induction y using binaryRec' generalizing x with
+  | z =>
+    simp only [zero_testBit, Bool.ne_false_iff]
+    exact ne_zero_implies_bit_true p
+  | f yb y h hyp =>
+    rw [← x.bit_decomp] at *
+    by_cases hb : bodd x = yb
+    · subst hb
+      obtain ⟨i, h⟩ := hyp (ne_of_apply_ne _ p)
+      refine ⟨i + 1, ?_⟩
+      rwa [testBit_succ_div_two, bit_div_two, testBit_succ_div_two, bit_div_two]
+    · refine ⟨0, ?_⟩
+      rwa [testBit_zero_is_bodd, testBit_zero_is_bodd, bodd_bit, bodd_bit]
 
 /--
 `eq_of_testBit_eq` allows proving two natural numbers are equal
@@ -142,27 +109,18 @@ theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) :
     have p := pred i
     contradiction
 
-theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
-  induction x using div2Induction generalizing n with
-  | ind x hyp =>
-    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.pow_two_pos n) p
-    have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
+theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : 2^n ≤ x) : ∃ i, n ≤ i ∧ testBit x i := by
+  induction x using binaryRec generalizing n with
+  | z => exact absurd p (Nat.not_le_of_lt n.pow_two_pos)
+  | f xb x hyp =>
     match n with
-    | zero =>
-      let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
-      exact Exists.intro j (And.intro (Nat.zero_le _) jp)
-    | succ n =>
-      have x_ge_n : x / 2 ≥ 2 ^ n := by
-          simp [le_div_iff_mul_le, ← Nat.pow_succ']
-          exact p
-      have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
-      apply Exists.intro (j+1)
-      apply And.intro
-      case left =>
-        exact (Nat.succ_le_succ jp.left)
-      case right =>
-        simp [testBit_succ_div2 _ j]
-        exact jp.right
+    | 0 =>
+      simp only [zero_le, true_and]
+      exact ne_zero_implies_bit_true (ne_of_gt (Nat.lt_of_succ_le p))
+    | n+1 =>
+      obtain ⟨i, h⟩ := hyp (mul_two_le_bit.mp p)
+      refine ⟨i + 1, ?_⟩
+      rwa [Nat.add_le_add_iff_right, testBit_succ_div_two, bit_div_two]
 
 theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
   simp only [testBit_to_div_mod] at p
@@ -229,7 +187,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -262,14 +220,14 @@ private theorem testBit_one_zero : testBit 1 0 = true := by trivial
 @[simp] theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n) := by
   induction i generalizing n with
   | zero =>
-    simp [testBit_zero_is_mod2]
+    simp [testBit_zero_is_bodd]
     match n with
     | 0 =>
       simp
     | n+1 =>
-      simp [Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
+      simp [bodd, Nat.pow_succ, Nat.mul_comm _ 2, two_mul_sub_one, Nat.pow_two_pos]
   | succ i hyp =>
-    simp [testBit_succ_div2]
+    simp [testBit_succ_div_two]
     match n with
     | 0 =>
       simp [pow_zero]
@@ -304,12 +262,12 @@ theorem testBit_bitwise
       simp only [x_zero, y_zero, ←Nat.two_mul]
       cases i with
       | zero =>
-        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, testBit_zero_is_mod2, Nat.mul_add_mod, mod_eq_of_lt]
+        cases p : f (x % 2 != 0) (y % 2 != 0) <;>
+          simp [p, testBit_zero_is_bodd, bodd, decide_mod_two_eq_one, Nat.mul_add_mod]
       | succ i =>
         have hyp_i := hyp i (Nat.le_refl (i+1))
-        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
-          simp [p, testBit_succ_div2, one_div_two, hyp_i, Nat.mul_add_div]
+        cases p : f (x % 2 != 0) (y % 2 != 0) <;>
+          simp [p, testBit_succ_div_two, decide_mod_two_eq_one, hyp_i, Nat.mul_add_div]
 
 /-! ### bitwise -/