Documentation

Mathlib.Data.Nat.EvenOddRec

A recursion principle based on even and odd numbers. #

source
def Nat.evenOddRec {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.binaryRec, to avoid having to switch to dealing with bit0 and bit1.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Nat.evenOddRec_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)) :
    evenOddRec h0 h_even h_odd 0 = h0
    source
    @[simp]
    theorem Nat.evenOddRec_even {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) (n : ℕ) :
    evenOddRec h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n)
    source
    @[simp]
    theorem Nat.evenOddRec_odd {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) (n : ℕ) :
    evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)
    source
    noncomputable def Nat.evenOddStrongRec {P : ℕ → Sort u_1} (h_even : (n : ℕ) → ((k : ℕ) → k < 2 * n → P k) → P (2 * n)) (h_odd : (n : ℕ) → ((k : ℕ) → k < 2 * n + 1 → P k) → P (2 * n + 1)) (n : ℕ) :
    P n

    Strong recursion principle on even and odd numbers: if for all i : ℕ we can prove P (2 * i) from P j for all j < 2 * i and we can prove P (2 * i + 1) from P j for all j < 2 * i + 1, then we have P n for all n : ℕ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For