English
A variant of binaryRec allowing a different elimination step; parallels binaryRec.
Русский
Вариант binaryRec с другим шагом устранения; аналогично бинарной рекурсии.
LaTeX
$$$\text{binaryRec}'\;\text{motive}\;\text{zero}\;\text{bit}\;n \in \text{motive}(n)$$$
Lean4
/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
the bit being appended is `true` -/
@[elab_as_elim, specialize]
def binaryRec' {motive : Nat → Sort u} (zero : motive 0)
(bit : ∀ b n, (n = 0 → b = true) → motive n → motive (bit b n)) : ∀ n, motive n :=
binaryRec zero fun b n ih =>
if h : n = 0 → b = true then bit b n h ih
else
have : n.bit b = 0 := by
rw [bit_eq_zero_iff]
cases n <;> cases b <;> simp at h ⊢
congrArg motive this ▸ zero
