# Binary representation of integers using inductive types #

Note: Unlike in Coq, where this representation is preferred because of the reliance on kernel reduction, in Lean this representation is discouraged in favor of the "Peano" natural numbers Nat, and the purpose of this collection of theorems is to show the equivalence of the different approaches.

inductive PosNum :

The type of positive binary numbers.

13 = 1101(base 2) = bit1 (bit0 (bit1 one))

Instances For
Equations
instance instOnePosNum :
Equations
Equations
inductive Num :

The type of nonnegative binary numbers, using PosNum.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))

Instances For
Equations
instance instZeroNum :
Equations
instance instOneNum :
Equations
instance instInhabitedNum :
Equations
inductive ZNum :

Representation of integers using trichotomy around zero.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one))) -13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one)))

• zero: ZNum
• pos:
• neg:
Instances For
Equations
instance instZeroZNum :
Equations
instance instOneZNum :
Equations
Equations
def PosNum.bit (b : Bool) :

bit b n appends the bit b to the end of n, where bit tt x = x1 and bit ff x = x0.

Equations
Instances For

The successor of a PosNum.

Equations
Instances For

Returns a boolean for whether the PosNum is one.

Equations
Instances For

Addition of two PosNums.

Equations
Instances For
Equations

The predecessor of a PosNum as a Num.

Equations
Instances For

The predecessor of a PosNum as a PosNum. This means that pred 1 = 1.

Equations
Instances For

The number of bits of a PosNum, as a PosNum.

Equations
• PosNum.one.size = 1
• n.bit0.size = n.size.succ
• n.bit1.size = n.size.succ
Instances For

The number of bits of a PosNum, as a Nat.

Equations
• PosNum.one.natSize = 1
• n.bit0.natSize = n.natSize.succ
• n.bit1.natSize = n.natSize.succ
Instances For
def PosNum.mul (a : PosNum) :

Multiplication of two PosNums.

Equations
• a.mul PosNum.one = a
• a.mul n.bit0 = (a.mul n).bit0
• a.mul n.bit1 = (a.mul n).bit0 + a
Instances For
instance PosNum.instMul :
Equations

ofNatSucc n is the PosNum corresponding to n + 1.

Equations
Instances For

ofNat n is the PosNum corresponding to n, except for ofNat 0 = 1.

Equations
Instances For
Equations

Ordering of PosNums.

Equations
Instances For
instance PosNum.instLT :
Equations
instance PosNum.instLE :
Equations
instance PosNum.decidableLT :
DecidableRel fun (x1 x2 : PosNum) => x1 < x2
Equations
• x✝.decidableLT x = id inferInstance
instance PosNum.decidableLE :
DecidableRel fun (x1 x2 : PosNum) => x1 x2
Equations
• x✝.decidableLE x = id inferInstance
@[deprecated]
def castPosNum {α : Type u_1} [One α] [Add α] :
PosNumα

castPosNum casts a PosNum into any type which has 1 and +.

Equations
• n.bit0 = n + n
• n.bit1 = n + n + 1
Instances For
@[deprecated]
def castNum {α : Type u_1} [One α] [Add α] [Zero α] :
Numα

castNum casts a Num into any type which has 0, 1 and +.

Equations
Instances For
@[deprecated, instance 900]
instance posNumCoe {α : Type u_1} [One α] [Add α] :
Equations
• posNumCoe = { coe := castPosNum }
@[deprecated, instance 900]
instance numNatCoe {α : Type u_1} [One α] [Add α] [Zero α] :
Equations
• numNatCoe = { coe := castNum }
instance instReprPosNum :
Equations
instance instReprNum :
Equations
def Num.succ' :

The successor of a Num as a PosNum.

Equations
Instances For
def Num.succ (n : Num) :

The successor of a Num as a Num.

Equations
Instances For

Addition of two Nums.

Equations
Instances For
Equations
def Num.bit0 :

bit0 n appends a 0 to the end of n, where bit0 n = n0.

Equations
Instances For
def Num.bit1 :

bit1 n appends a 1 to the end of n, where bit1 n = n1.

Equations
Instances For
def Num.bit (b : Bool) :

bit b n appends the bit b to the end of n, where bit tt x = x1 and bit ff x = x0.

Equations
Instances For
def Num.size :

The number of bits required to represent a Num, as a Num. size 0 is defined to be 0.

Equations
Instances For

The number of bits required to represent a Num, as a Nat. size 0 is defined to be 0.

Equations
Instances For
def Num.mul :

Multiplication of two Nums.

Equations
Instances For
instance Num.instMul :
Equations
def Num.cmp :

Ordering of Nums.

Equations
Instances For
instance Num.instLT :
Equations
instance Num.instLE :
Equations
instance Num.decidableLT :
DecidableRel fun (x1 x2 : Num) => x1 < x2
Equations
• x✝.decidableLT x = id inferInstance
instance Num.decidableLE :
DecidableRel fun (x1 x2 : Num) => x1 x2
Equations
• x✝.decidableLE x = id inferInstance

Converts a Num to a ZNum.

Equations
Instances For

Converts x : Num to -x : ZNum.

Equations
Instances For
def Num.ofNat' :
Num

Converts a Nat to a Num.

Equations
Instances For
def ZNum.zNeg :

The negation of a ZNum.

Equations
Instances For
instance ZNum.instNeg :
Equations
def ZNum.abs :

The absolute value of a ZNum as a Num.

Equations
Instances For
def ZNum.succ :

The successor of a ZNum.

Equations
Instances For
def ZNum.pred :

The predecessor of a ZNum.

Equations
Instances For
def ZNum.bit0 :

bit0 n appends a 0 to the end of n, where bit0 n = n0.

Equations
Instances For
def ZNum.bit1 :

bit1 x appends a 1 to the end of x, mapping x to 2 * x + 1.

Equations
Instances For

bitm1 x appends a 1 to the end of x, mapping x to 2 * x - 1.

Equations
Instances For

Converts an Int to a ZNum.

Equations
Instances For

Subtraction of two PosNums, producing a ZNum.

Equations
• x.sub' PosNum.one = x.pred'.toZNum
• PosNum.one.sub' x = x.pred'.toZNumNeg
• a.bit0.sub' b.bit0 = (a.sub' b).bit0
• a.bit0.sub' b.bit1 = (a.sub' b).bitm1
• a.bit1.sub' b.bit0 = (a.sub' b).bit1
• a.bit1.sub' b.bit1 = (a.sub' b).bit0
Instances For

Converts a ZNum to Option PosNum, where it is some if the ZNum was positive and none otherwise.

Equations
Instances For

Converts a ZNum to a PosNum, mapping all out of range values to 1.

Equations
Instances For
def PosNum.sub (a : PosNum) (b : PosNum) :

Subtraction of PosNums, where if a < b, then a - b = 1.

Equations
• a.sub b = match a.sub' b with | => p | x => 1
Instances For
instance PosNum.instSub :
Equations
def Num.ppred :

The predecessor of a Num as an Option Num, where ppred 0 = none

Equations
Instances For
def Num.pred :

The predecessor of a Num as a Num, where pred 0 = 0.

Equations
Instances For
def Num.div2 :

Divides a Num by 2

Equations
Instances For

Converts a ZNum to an Option Num, where ofZNum' p = none if p < 0.

Equations
Instances For

Converts a ZNum to an Option Num, where ofZNum p = 0 if p < 0.

Equations
Instances For
def Num.sub' :

Subtraction of two Nums, producing a ZNum.

Equations
Instances For
def Num.psub (a : Num) (b : Num) :

Subtraction of two Nums, producing an Option Num.

Equations
Instances For
def Num.sub (a : Num) (b : Num) :

Subtraction of two Nums, where if a < b, a - b = 0.

Equations
Instances For
instance Num.instSub :
Equations

Addition of ZNums.

Equations
Instances For
Equations
def ZNum.mul :

Multiplication of ZNums.

Equations
Instances For
instance ZNum.instMul :
Equations
def ZNum.cmp :

Ordering on ZNums.

Equations
Instances For
instance ZNum.instLT :
Equations
instance ZNum.instLE :
Equations
instance ZNum.decidableLT :
DecidableRel fun (x1 x2 : ZNum) => x1 < x2
Equations
• x✝.decidableLT x = id inferInstance
instance ZNum.decidableLE :
DecidableRel fun (x1 x2 : ZNum) => x1 x2
Equations
• x✝.decidableLE x = id inferInstance
def PosNum.divModAux (d : PosNum) (q : Num) (r : Num) :

Auxiliary definition for PosNum.divMod.

Equations
Instances For
def PosNum.divMod (d : PosNum) :

divMod x y = (y / x, y % x).

Equations
• d.divMod n.bit0 = match d.divMod n with | (q, r₁) => d.divModAux q r₁.bit0
• d.divMod n.bit1 = match d.divMod n with | (q, r₁) => d.divModAux q r₁.bit1
• d.divMod PosNum.one = d.divModAux 0 1
Instances For
def PosNum.div' (n : PosNum) (d : PosNum) :

Division of PosNum,

Equations
• n.div' d = (d.divMod n).1
Instances For
def PosNum.mod' (n : PosNum) (d : PosNum) :

Modulus of PosNums.

Equations
• n.mod' d = (d.divMod n).2
Instances For
def Num.div :

Division of Nums, where x / 0 = 0.

Equations
Instances For
def Num.mod :

Modulus of Nums.

Equations
Instances For
instance Num.instDiv :
Equations
instance Num.instMod :
Equations
def Num.gcdAux :

Auxiliary definition for Num.gcd.

Equations
Instances For
def Num.gcd (a : Num) (b : Num) :

Greatest Common Divisor (GCD) of two Nums.

Equations
Instances For
def ZNum.div :

Division of ZNum, where x / 0 = 0.

Equations
Instances For
def ZNum.mod :

Modulus of ZNums.

Equations
Instances For
instance ZNum.instDiv :
Equations
instance ZNum.instMod :
Equations
def ZNum.gcd (a : ZNum) (b : ZNum) :

Greatest Common Divisor (GCD) of two ZNums.

Equations
• a.gcd b = a.abs.gcd b.abs
Instances For
@[deprecated]
def castZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
ZNumα

castZNum casts a ZNum into any type which has 0, 1, + and neg

Equations
Instances For
@[deprecated, instance 900]
instance znumCoe {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
Equations
• znumCoe = { coe := castZNum }
instance instReprZNum :
Equations