A recursion principle based on even and odd numbers. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def nat.even_odd_rec {P : ℕ → Sort u_1} (h0 : P 0) (h_even : Π (n : ℕ), P n → P (2 * n)) (h_odd : Π (n : ℕ), P n → P (2 * n + 1)) (n : ℕ) :

P n

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.binary_rec, to avoid having to switch to dealing with bit0 and bit1.

Equations

nat.even_odd_rec h0 h_even h_odd n = nat.binary_rec h0 (λ (b : bool) (i : ℕ) (hi : P i), b.cases_on (_.mpr (_.mp (h_even i hi))) (_.mpr (_.mp (h_odd i hi)))) n

source

@[simp]

theorem nat.even_odd_rec_zero (P : ℕ → Sort u_1) (h0 : P 0) (h_even : Π (i : ℕ), P i → P (2 * i)) (h_odd : Π (i : ℕ), P i → P (2 * i + 1)) :

nat.even_odd_rec h0 h_even h_odd 0 = h0

source

@[simp]

theorem nat.even_odd_rec_even (n : ℕ) (P : ℕ → Sort u_1) (h0 : P 0) (h_even : Π (i : ℕ), P i → P (2 * i)) (h_odd : Π (i : ℕ), P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :

nat.even_odd_rec h0 h_even h_odd (2 * n) = h_even n (nat.even_odd_rec h0 h_even h_odd n)

source

@[simp]

theorem nat.even_odd_rec_odd (n : ℕ) (P : ℕ → Sort u_1) (h0 : P 0) (h_even : Π (i : ℕ), P i → P (2 * i)) (h_odd : Π (i : ℕ), P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :

nat.even_odd_rec h0 h_even h_odd (2 * n + 1) = h_odd n (nat.even_odd_rec h0 h_even h_odd n)