English
The even-odd recursion principle: for any P, if P(0) holds and P(i) → P(2i) and P(i) → P(2i+1) for all i, then P(n) holds for all n.
Русский
Основной принцип рекурсии по чётным и нечётным: если P(0) верно и из P(i) следует P(2i) и P(i) следует P(2i+1) для всех i, то P(n) верно для всех n.
LaTeX
$$$$ \text{evenOddRec} : \forall P:\\mathbb{N} \\to \\mathrm{Sort}, \\ P(0) \\to (\\forall n, P(n) \\to P(2n)) \\to (\\forall n, P(n) \\to P(2n+1)) \\to \forall n, P(n). $$$$
Lean4
/-- Recursion principle on even and odd numbers: if we have `P 0`, and for all `i : ℕ` we can
extend from `P i` to both `P (2 * i)` and `P (2 * i + 1)`, then we have `P n` for all `n : ℕ`.
This is nothing more than a wrapper around `Nat.binaryRec`, to avoid having to switch to
dealing with `bit0` and `bit1`. -/
@[elab_as_elim]
def evenOddRec {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ n, P n → P (2 * n)) (h_odd : ∀ n, P n → P (2 * n + 1)) (n : ℕ) :
P n :=
binaryRec h0
(fun
| false, i, hi => (h_even i hi : P (2 * i))
| true, i, hi => (h_odd i hi : P (2 * i + 1)))
n
