feat: de-mathlib Nat.binaryRec

[FR-vdash-bot]

Some of the definitions have been modified to be faster.

• depends on: feat: more Bool lemmas #464
• depends on: feat: more lemmas about equality #465

[FR-vdash-bot]

awaiting-review

[eric-wieser]

What's the status of this PR in respect to #366? In that PR we got:

/--
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 _)

but these don't seem directly related.

[FR-vdash-bot]

I'm not sure where these diffs are. It might just be some mess from the merge.

[FR-vdash-bot]

What's the status of this PR in respect to #366? In that PR we got:

/--
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 _)

but these don't seem directly related.

I replaced it with binaryRecs and did some golf.

[fgdorais]

Strange. Please ignore my comments then.

[FR-vdash-bot]

It seems that Std.Data.Nat.Bitwise is not there now. What should I do now? Should I create a PR for core?

[fgdorais]

Marking as duplicate while waiting for lean4#3756. Ask to remove that label if that PR doesn't get merged.

[FR-vdash-bot]

Replaced by #799.