English
complEDSRec' is a strong recursion principle for the complement sequence: given base values for 0 and 1 and even/odd propagation rules, one obtains the sequence for all n.
Русский
complEDSRec' — мощный принцип рекурсии для дополняющей последовательности: при задании базовых значений 0 и 1 и правил распространения для чётных и нечётных индексов, последовательность существует для всех n.
LaTeX
$$$\text{complEDSRec}'\;\{P:\mathbb{N}\to \text{Sort}\} \; P(0) \; P(1) \; \big(\forall m\, P(m+1) \to P(2(m+1))\big) \; \big(\forall m\, P(m+1) \to P(m+2) \to P(2(m+1)+1)\big) \to \forall n\; P(n)$$$
Lean4
/-- Strong recursion principle for the complement sequence for a normalised EDS: if we have
* `P 0`, `P 1`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P k` for all `k < 2 * (m + 3)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P k` for all `k < 2 * (m + 2) + 1`,
then we have `P n` for all `n : ℕ`. -/
@[elab_as_elim]
noncomputable def complEDSRec' {P : ℕ → Sort u} (zero : P 0) (one : P 1)
(even : ∀ m : ℕ, (∀ k < 2 * (m + 1), P k) → P (2 * (m + 1)))
(odd : ∀ m : ℕ, (∀ k < 2 * (m + 1) + 1, P k) → P (2 * (m + 1) + 1)) (n : ℕ) : P n :=
n.evenOddStrongRec (by rintro (_ | _) h; exacts [zero, even _ h]) (by rintro (_ | _) h; exacts [one, odd _ h])
