even_odd_rec as a wrapper for binary_rec?

Stream: general

[Stuart Presnell]

Would it be reasonable to PR something like the following? This would allow recursion over even/odd numbers without having to deal with implementation details like bit0 and bit1.

def even_odd_rec (n : ℕ) (P : ℕ → Sort*) (h0 : P 0)
  (h_even : ∀ i, P i → P (2 * i))
  (h_odd : ∀ i, P i → P (2 * i + 1)) : P n :=
begin
  refine @binary_rec P h0 (λ b i hi, _) n,
  cases b,
  { simpa [bit0_val i] using h_even i hi },
  { simpa [bit1_val i] using h_odd i hi },
end

[Eric Wieser]

I feel like the bit0 and bit1 version might still be more useful

[Eric Wieser]

Since we have lots of lemmas about those

[Eric Wieser]

But I can see that the one in terms of nat.bit could be annoying to use

[Stuart Presnell]

The bit0 and bit1 version would still be there for anyone who wants them, of course.

[Stuart Presnell]

It just seems wrong and inconvenient to have to drop out of the familiar world of natural numbers and into the world of bits, when we could just as easily provide the same functionality within ℕ.

[Stuart Presnell]

#15457