English
Strong recursion principle on even and odd numbers: for all P, if from all smaller indices before 2n we can derive P(2n) and from all smaller indices before 2n+1 we can derive P(2n+1), then P(n) holds for all n.
Русский
Сильный принцип рекурсии по чётным и нечётным: если из утверждений о всех меньших индексах следует P(2n) и P(2n+1), тогда P(n) для всех n.
LaTeX
$$$$ \forall P:\\mathbb{N} \\to \\mathrm{Sort},\\ (\\forall n,\\ (\\forall k < 2n, P(k)) \\Rightarrow P(2n)) \\wedge \\forall n,\\ (\\forall k < 2n+1, P(k)) \\Rightarrow P(2n+1) \\Rightarrow \\forall n, P(n). $$$$
Lean4
/-- 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 : ℕ`. -/
@[elab_as_elim]
noncomputable def evenOddStrongRec {P : ℕ → Sort*} (h_even : ∀ n : ℕ, (∀ k < 2 * n, P k) → P (2 * n))
(h_odd : ∀ n : ℕ, (∀ k < 2 * n + 1, P k) → P (2 * n + 1)) (n : ℕ) : P n :=
n.strongRecOn fun m ih =>
m.even_or_odd'.choose_spec.by_cases (fun h => h.symm ▸ h_even m.even_or_odd'.choose <| h ▸ ih)
(fun h => h.symm ▸ h_odd m.even_or_odd'.choose <| h ▸ ih)
