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

The type of positive binary numbers.

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

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

def instDecidableEqPosNum.decEq (x✝ x✝¹ : PosNum) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instDecidableEqPosNum : DecidableEq PosNum

@[implicit_reducible]

instance instOnePosNum : One PosNum

@[implicit_reducible]

instance instInhabitedPosNum : Inhabited PosNum

inductive Num : Type

The type of nonnegative binary numbers, using PosNum.

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

• zero : Num
• pos : PosNum → Num

def instDecidableEqNum.decEq (x✝ x✝¹ : Num) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instDecidableEqNum : DecidableEq Num

@[implicit_reducible]

instance instZeroNum : Zero Num

@[implicit_reducible]

instance instOneNum : One Num

@[implicit_reducible]

instance instInhabitedNum : Inhabited Num

inductive ZNum : Type

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

@[implicit_reducible]

instance instDecidableEqZNum : DecidableEq ZNum

def instDecidableEqZNum.decEq (x✝ x✝¹ : ZNum) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instZeroZNum : Zero ZNum

@[implicit_reducible]

instance instOneZNum : One ZNum

@[implicit_reducible]

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.

def PosNum.isOne : PosNum → Bool

Returns a Boolean for whether the PosNum is one.

def PosNum.add : PosNum → PosNum → PosNum

Addition of two PosNums.

@[implicit_reducible]

instance PosNum.instAdd : Add PosNum

def PosNum.pred' : PosNum → Num

The predecessor of a PosNum as a Num.

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.

def PosNum.natSize : PosNum → ℕ

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

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

Multiplication of two PosNums.

@[implicit_reducible]

instance PosNum.instMul : Mul PosNum

def PosNum.ofNatSucc : ℕ → PosNum

ofNatSucc n is the PosNum corresponding to n + 1.

def PosNum.ofNat (n : ℕ) : PosNum

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

@[implicit_reducible, instance 100]

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

def PosNum.cmp : PosNum → PosNum → Ordering

Ordering of PosNums.

@[implicit_reducible]

instance PosNum.instLT : LT PosNum

@[implicit_reducible]

instance PosNum.instLE : LE PosNum

@[implicit_reducible]

instance PosNum.decidableLT : DecidableLT PosNum

@[implicit_reducible]

instance PosNum.decidableLE : DecidableLE PosNum

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

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

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

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

@[implicit_reducible, instance 900]

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

@[implicit_reducible, instance 900]

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

@[implicit_reducible]

instance instReprPosNum : Repr PosNum

@[implicit_reducible]

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.

@[implicit_reducible]

instance Num.instAdd : 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.

@[implicit_reducible]

instance Num.instMul : Mul Num

def Num.cmp : Num → Num → Ordering

Ordering of Nums.

@[implicit_reducible]

instance Num.instLT : LT Num

@[implicit_reducible]

instance Num.instLE : LE Num

@[implicit_reducible]

instance Num.decidableLT : DecidableLT Num

@[implicit_reducible]

instance Num.decidableLE : DecidableLE Num

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.

@[implicit_reducible]

instance ZNum.instNeg : 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.

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 b : PosNum) : PosNum

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

@[implicit_reducible]

instance PosNum.instSub : 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 b : Num) : Option Num

Subtraction of two Nums, producing an Option Num.

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

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

@[implicit_reducible]

instance Num.instSub : Sub Num

def ZNum.add : ZNum → ZNum → ZNum

Addition of ZNums.

@[implicit_reducible]

instance ZNum.instAdd : Add ZNum

def ZNum.mul : ZNum → ZNum → ZNum

Multiplication of ZNums.

@[implicit_reducible]

instance ZNum.instMul : Mul ZNum

def ZNum.cmp : ZNum → ZNum → Ordering

Ordering on ZNums.

@[implicit_reducible]

instance ZNum.instLT : LT ZNum

@[implicit_reducible]

instance ZNum.instLE : LE ZNum

@[implicit_reducible]

instance ZNum.decidableLT : DecidableLT ZNum

@[implicit_reducible]

instance ZNum.decidableLE : DecidableLE ZNum

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

Auxiliary definition for PosNum.divMod.

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

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

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

Division of PosNum

def PosNum.mod' (n 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.

@[implicit_reducible]

instance Num.instDiv : Div Num

@[implicit_reducible]

instance Num.instMod : Mod Num

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

Auxiliary definition for Num.gcd.

def Num.gcd (a 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.

@[implicit_reducible]

instance ZNum.instDiv : Div ZNum

@[implicit_reducible]

instance ZNum.instMod : Mod ZNum

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

Greatest Common Divisor (GCD) of two ZNums.

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

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

@[implicit_reducible, instance 900]

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

@[implicit_reducible]

instance instReprZNum : Repr ZNum