Additional properties of binary recursion on Nat
#
This file documents additional properties of binary recursion,
which allows us to more easily work with operations which do depend
on the number of leading zeros in the binary representation of n
.
For example, we can more easily work with Nat.bits
and Nat.size
.
See also: Nat.bitwise
, Nat.pow
(for various lemmas about size
and shiftLeft
/shiftRight
),
and Nat.digits
.
shiftLeft' b m n
performs a left shift of m
n
times
and adds the bit b
as the least significant bit each time.
Returns the corresponding natural number
Equations
- Nat.shiftLeft' b m 0 = m
- Nat.shiftLeft' b m n.succ = Nat.bit b (Nat.shiftLeft' b m n)
Instances For
Lean takes the unprimed name for Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n
.
A recursion principle for bit
representations of natural numbers.
For a predicate C : Nat → Sort*
, if instances can be
constructed for natural numbers of the form bit b n
,
they can be constructed for all natural numbers.
Equations
- Nat.binaryRec z f n = if n0 : n = 0 then ⋯.mpr z else let n' := n.div2; let_fun _x := ⋯; ⋯.mpr (f n.bodd n' (Nat.binaryRec z f n'))
Instances For
bitwise ops
boddDiv2_eq
and bodd
#
bit0
and bit1
#
The same as binaryRec_eq
,
but that one unfortunately requires f
to be the identity when appending false
to 0
.
Here, we allow you to explicitly say that that case is not happening,
i.e. supplying n = 0 → b = true
.
The same as binaryRec
, but the induction step can assume that if n=0
,
the bit being appended is true
Equations
- Nat.binaryRec' z f = Nat.binaryRec z fun (b : Bool) (n : ℕ) (ih : C n) => if h : n = 0 → b = true then f b n h ih else ⋯.mpr z
Instances For
The same as binaryRec
, but special casing both 0 and 1 as base cases
Equations
- Nat.binaryRecFromOne z₀ z₁ f n = Nat.binaryRec' z₀ (fun (b : Bool) (n : ℕ) (h : n = 0 → b = true) (ih : C n) => if h' : n = 0 then ⋯.mpr (⋯.mpr z₁) else f b n h' ih) n