A recursion principle based on even and odd numbers. #
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
@[simp]
theorem
Nat.evenOddRec_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.evenOddRec h0 h_even h_odd (2 * n) = h_even n (Nat.evenOddRec h0 h_even h_odd n)
noncomputable def
Nat.evenOddStrongRec
{P : ℕ → Sort u_1}
(n : ℕ)
(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))
:
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.