English
Let C be a family of types, z ∈ C0 and f : ∀ b n, C n → C (bit b n). For n ≠ 0, binaryRec z f n equals f (bodd n) (div2 n) (binaryRec z f (div2 n)).
Русский
Пусть C — семейство типов, z ∈ C0 и f : ∀ b n, C n → C (bit b n). Для n ≠ 0 выполняется binaryRec z f n = f (bodd n) (div2 n) (binaryRec z f (div2 n)).
LaTeX
$$$$ \\text{Для любой }\ C:\ Nat \\to \\mathrm{Sort}*,\\ z \\in C(0),\\ f:\\forall b\\,n, C(n) \\to C(\\mathrm{bit}\\, b\\, n),\\ n \\neq 0:\\ binaryRec\\ z\\ f\\ n = f(\\mathrm{bodd}\\, n)(\\mathrm{div2}\\, n)(binaryRec\\ z\\ f\\ (\\mathrm{div2}\\ n)) $$$$
Lean4
theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → C (bit b n)) {n} (h : n ≠ 0) :
binaryRec z f n = bit_bodd_div2 n ▸ f (bodd n) (div2 n) (binaryRec z f (div2 n)) := by
cases n using bitCasesOn with
| bit b n =>
rw [binaryRec_eq _ _ (by right; simpa [bit_eq_zero_iff] using h)]
generalize_proofs h; revert h
rw [bodd_bit, div2_bit]
simp
