English
A recursion principle for bit representations of natural numbers: any motive can be defined from 0 and the step given by bit b n.
Русский
Принцип рекурсии по двоичному представлению: любую мотиальную зависимость можно определить от 0 и шага через bit b n.
LaTeX
$$$\text{binaryRec}\;\text{motive}\;\text{zero}\;\text{bit}\;n \in \text{motive}(n)$$$
Lean4
/-- A recursion principle for `bit` representations of natural numbers.
For a predicate `motive : Nat → Sort u`, if instances can be
constructed for natural numbers of the form `bit b n`,
they can be constructed for all natural numbers. -/
@[elab_as_elim, specialize]
def binaryRec {motive : Nat → Sort u} (zero : motive 0) (bit : ∀ b n, motive n → motive (bit b n)) (n : Nat) :
motive n :=
if n0 : n = 0 then congrArg motive n0 ▸ zero
else
let x := bit (1 &&& n != 0) (n >>> 1) (binaryRec zero bit (n >>> 1))
congrArg motive n.bit_testBit_zero_shiftRight_one ▸ x
decreasing_by exact bitwise_rec_lemma n0
