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 : Type

• one: PosNum
• bit1: PosNum → PosNum
• bit0: PosNum → PosNum

The type of positive binary numbers.

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

instance instDecidableEqPosNum : DecidableEq PosNum

instance instOnePosNum : One PosNum

instance instInhabitedPosNum : Inhabited PosNum

inductive Num : Type

• zero: Num
• pos: PosNum → Num

The type of nonnegative binary numbers, using PosNum.

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

instance instDecidableEqNum : DecidableEq Num

instance instZeroNum : Zero Num

instance instOneNum : One Num

instance instInhabitedNum : Inhabited Num

inductive ZNum : Type

• zero: ZNum
• pos: PosNum → ZNum
• neg: PosNum → 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)))

instance instDecidableEqZNum : DecidableEq ZNum

instance instZeroZNum : Zero ZNum

instance instOneZNum : One ZNum

instance instInhabitedZNum : Inhabited ZNum

def PosNum.bit (b : Bool) : PosNum → PosNum

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

def PosNum.succ : PosNum → PosNum

The successor of a PosNum.

Equations

• PosNum.succ PosNum.one = PosNum.bit0 PosNum.one
• PosNum.succ (PosNum.bit1 n) = PosNum.bit0 (PosNum.succ n)
• PosNum.succ (PosNum.bit0 n) = PosNum.bit1 n

def PosNum.isOne : PosNum → Bool

Returns a boolean for whether the PosNum is one.

def PosNum.add : PosNum → PosNum → PosNum

Addition of two PosNums.

Equations

• PosNum.add PosNum.one x = PosNum.succ x
• PosNum.add x PosNum.one = PosNum.succ x
• PosNum.add (PosNum.bit0 a) (PosNum.bit0 b) = PosNum.bit0 (PosNum.add a b)
• PosNum.add (PosNum.bit1 a) (PosNum.bit1 b) = PosNum.bit0 (PosNum.succ (PosNum.add a b))
• PosNum.add (PosNum.bit0 a) (PosNum.bit1 b) = PosNum.bit1 (PosNum.add a b)
• PosNum.add (PosNum.bit1 a) (PosNum.bit0 b) = PosNum.bit1 (PosNum.add a b)

instance PosNum.instAddPosNum : Add PosNum

def PosNum.pred' : PosNum → Num

The predecessor of a PosNum as a Num.

Equations

• PosNum.pred' PosNum.one = 0
• PosNum.pred' (PosNum.bit0 n) = Num.pos (Num.casesOn (PosNum.pred' n) 1 PosNum.bit1)
• PosNum.pred' (PosNum.bit1 n) = Num.pos (PosNum.bit0 n)

def PosNum.pred (a : PosNum) : PosNum

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

def PosNum.size : PosNum → PosNum

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

Equations

• PosNum.size PosNum.one = 1
• PosNum.size (PosNum.bit0 n) = PosNum.succ (PosNum.size n)
• PosNum.size (PosNum.bit1 n) = PosNum.succ (PosNum.size n)

def PosNum.natSize : PosNum → ℕ

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

Equations

• PosNum.natSize PosNum.one = 1
• PosNum.natSize (PosNum.bit0 n) = Nat.succ (PosNum.natSize n)
• PosNum.natSize (PosNum.bit1 n) = Nat.succ (PosNum.natSize n)

def PosNum.mul (a : PosNum) : PosNum → PosNum

Multiplication of two PosNums.

Equations

• PosNum.mul a PosNum.one = a
• PosNum.mul a (PosNum.bit0 n) = PosNum.bit0 (PosNum.mul a n)
• PosNum.mul a (PosNum.bit1 n) = PosNum.bit0 (PosNum.mul a n) + a

instance PosNum.instMulPosNum : Mul PosNum

def PosNum.ofNatSucc : ℕ → PosNum

ofNatSucc n is the PosNum corresponding to n + 1.

Equations

• PosNum.ofNatSucc 0 = 1
• PosNum.ofNatSucc (Nat.succ n) = PosNum.succ (PosNum.ofNatSucc n)

def PosNum.ofNat (n : ℕ) : PosNum

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

instance PosNum.instOfNatPosNumHAddNatInstHAddInstAddNatOfNat {n : ℕ} : OfNat PosNum (n + 1)

def PosNum.cmp : PosNum → PosNum → Ordering

Ordering of PosNums.

Equations

• PosNum.cmp PosNum.one PosNum.one = Ordering.eq
• PosNum.cmp x PosNum.one = Ordering.gt
• PosNum.cmp PosNum.one x = Ordering.lt
• PosNum.cmp (PosNum.bit0 a) (PosNum.bit0 b) = PosNum.cmp a b
• PosNum.cmp (PosNum.bit0 a) (PosNum.bit1 b) = Ordering.casesOn (PosNum.cmp a b) Ordering.lt Ordering.lt Ordering.gt
• PosNum.cmp (PosNum.bit1 a) (PosNum.bit0 b) = Ordering.casesOn (PosNum.cmp a b) Ordering.lt Ordering.gt Ordering.gt
• PosNum.cmp (PosNum.bit1 a) (PosNum.bit1 b) = PosNum.cmp a b

instance PosNum.instLTPosNum : LT PosNum

instance PosNum.instLEPosNum : LE PosNum

instance PosNum.decidableLT : DecidableRel fun x x_1 => x < x_1

instance PosNum.decidableLE : DecidableRel fun x x_1 => x ≤ x_1

@[deprecated]

def castPosNum {α : Type u_1} [One α] [Add α] : PosNum → α

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

Equations

• ↑PosNum.one = 1
• ↑(PosNum.bit0 n) = bit0 ↑n
• ↑(PosNum.bit1 n) = bit1 ↑n

@[deprecated]

def castNum {α : Type u_1} [One α] [Add α] [Zero α] : Num → α

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

@[deprecated]

instance posNumCoe {α : Type u_1} [One α] [Add α] : CoeHTCT PosNum α

@[deprecated]

instance numNatCoe {α : Type u_1} [One α] [Add α] [Zero α] : CoeHTCT Num α

instance instReprPosNum : Repr PosNum

instance instReprNum : Repr Num

def Num.succ' : Num → PosNum

The successor of a Num as a PosNum.

def Num.succ (n : Num) : Num

The successor of a Num as a Num.

def Num.add : Num → Num → Num

Addition of two Nums.

instance Num.instAddNum : Add Num

def Num.bit0 : Num → Num

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

def Num.bit1 : Num → Num

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

def Num.bit (b : Bool) : Num → Num

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

def Num.size : Num → Num

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

def Num.natSize : Num → ℕ

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

def Num.mul : Num → Num → Num

Multiplication of two Nums.

instance Num.instMulNum : Mul Num

def Num.cmp : Num → Num → Ordering

Ordering of Nums.

instance Num.instLTNum : LT Num

instance Num.instLENum : LE Num

instance Num.decidableLT : DecidableRel fun x x_1 => x < x_1

instance Num.decidableLE : DecidableRel fun x x_1 => x ≤ x_1

def Num.toZNum : Num → ZNum

Converts a Num to a ZNum.

def Num.toZNumNeg : Num → ZNum

Converts x : Num to -x : ZNum.

def Num.ofNat' : ℕ → Num

Converts a Nat to a Num.

def ZNum.zNeg : ZNum → ZNum

The negation of a ZNum.

instance ZNum.instNegZNum : Neg ZNum

def ZNum.abs : ZNum → Num

The absolute value of a ZNum as a Num.

def ZNum.succ : ZNum → ZNum

The successor of a ZNum.

def ZNum.pred : ZNum → ZNum

The predecessor of a ZNum.

def ZNum.bit0 : ZNum → ZNum

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

def ZNum.bit1 : ZNum → ZNum

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

def ZNum.bitm1 : ZNum → ZNum

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

def ZNum.ofInt' : ℤ → ZNum

Converts an Int to a ZNum.

def PosNum.sub' : PosNum → PosNum → ZNum

Subtraction of two PosNums, producing a ZNum.

Equations

• PosNum.sub' x PosNum.one = Num.toZNum (PosNum.pred' x)
• PosNum.sub' PosNum.one x = Num.toZNumNeg (PosNum.pred' x)
• PosNum.sub' (PosNum.bit0 a) (PosNum.bit0 b) = ZNum.bit0 (PosNum.sub' a b)
• PosNum.sub' (PosNum.bit0 a) (PosNum.bit1 b) = ZNum.bitm1 (PosNum.sub' a b)
• PosNum.sub' (PosNum.bit1 a) (PosNum.bit0 b) = ZNum.bit1 (PosNum.sub' a b)
• PosNum.sub' (PosNum.bit1 a) (PosNum.bit1 b) = ZNum.bit0 (PosNum.sub' a b)

def PosNum.ofZNum' : ZNum → Option PosNum

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

def PosNum.ofZNum : ZNum → PosNum

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

def PosNum.sub (a : PosNum) (b : PosNum) : PosNum

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

instance PosNum.instSubPosNum : Sub PosNum

def Num.ppred : Num → Option Num

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

def Num.pred : Num → Num

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

def Num.div2 : Num → Num

Divides a Num by 2

def Num.ofZNum' : ZNum → Option Num

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

def Num.ofZNum : ZNum → Num

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

def Num.sub' : Num → Num → ZNum

Subtraction of two Nums, producing a ZNum.

def Num.psub (a : Num) (b : Num) : Option Num

Subtraction of two Nums, producing an Option Num.

def Num.sub (a : Num) (b : Num) : Num

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

instance Num.instSubNum : Sub Num

def ZNum.add : ZNum → ZNum → ZNum

Addition of ZNums.

instance ZNum.instAddZNum : Add ZNum

def ZNum.mul : ZNum → ZNum → ZNum

Multiplication of ZNums.

instance ZNum.instMulZNum : Mul ZNum

def ZNum.cmp : ZNum → ZNum → Ordering

Ordering on ZNums.

instance ZNum.instLTZNum : LT ZNum

instance ZNum.instLEZNum : LE ZNum

instance ZNum.decidableLT : DecidableRel fun x x_1 => x < x_1

instance ZNum.decidableLE : DecidableRel fun x x_1 => x ≤ x_1

def PosNum.divModAux (d : PosNum) (q : Num) (r : Num) : Num × Num

Auxiliary definition for PosNum.divMod.

def PosNum.divMod (d : PosNum) : PosNum → Num × Num

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

Equations

• PosNum.divMod d (PosNum.bit0 n) = match PosNum.divMod d n with | (q, r₁) => PosNum.divModAux d q (Num.bit0 r₁)
• PosNum.divMod d (PosNum.bit1 n) = match PosNum.divMod d n with | (q, r₁) => PosNum.divModAux d q (Num.bit1 r₁)
• PosNum.divMod d PosNum.one = PosNum.divModAux d 0 1

def PosNum.div' (n : PosNum) (d : PosNum) : Num

Division of PosNum,

def PosNum.mod' (n : PosNum) (d : PosNum) : Num

Modulus of PosNums.

def Num.div : Num → Num → Num

Division of Nums, where x / 0 = 0.

def Num.mod : Num → Num → Num

Modulus of Nums.

instance Num.instDivNum : Div Num

instance Num.instModNum : Mod Num

def Num.gcdAux : ℕ → Num → Num → Num

Auxiliary definition for Num.gcd.

Equations

• Num.gcdAux 0 x x = x
• Num.gcdAux (Nat.succ n) Num.zero x = x
• Num.gcdAux (Nat.succ n) x x = Num.gcdAux n (x % x) x

def Num.gcd (a : Num) (b : Num) : Num

Greatest Common Divisor (GCD) of two Nums.

def ZNum.div : ZNum → ZNum → ZNum

Division of ZNum, where x / 0 = 0.

def ZNum.mod : ZNum → ZNum → ZNum

Modulus of ZNums.

instance ZNum.instDivZNum : Div ZNum

instance ZNum.instModZNum : Mod ZNum

def ZNum.gcd (a : ZNum) (b : ZNum) : Num

Greatest Common Divisor (GCD) of two ZNums.

@[deprecated]

def castZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : ZNum → α

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

@[deprecated]

instance znumCoe {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : CoeHTCT ZNum α

instance instReprZNum : Repr ZNum