English
A bit-based induction principle: if a motive is closed under the bit-construction, then it holds for all n.
Русский
Индукционный принцип по битам: если свойство сохраняется при конструировании битов, то оно верно для всех n.
LaTeX
$$$\forall motive,\; \forall n, \text{bitCasesOn}(n) \Rightarrow \text{motive}(n)$$$
Lean4
/-- 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 any given natural number. -/
@[inline]
def bitCasesOn {motive : Nat → Sort u} (n) (bit : ∀ b n, motive (bit b n)) : motive n :=
-- `1 &&& n != 0` is faster than `n.testBit 0`. This may change when we have faster `testBit`.
let x :=
bit (1 &&& n != 0)
(n >>> 1)
-- `congrArg motive _ ▸ x` is defeq to `x` in non-dependent case
congrArg motive n.bit_testBit_zero_shiftRight_one ▸ x
