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

instance instDecidableEqPosNum : DecidableEq PosNum

Equations

• instDecidableEqPosNum = decEqPosNum✝

instance instOnePosNum : One PosNum

Equations

• instOnePosNum = { one := PosNum.one }

instance instInhabitedPosNum : Inhabited PosNum

Equations

• instInhabitedPosNum = { default := 1 }

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

instance instDecidableEqNum : DecidableEq Num

Equations

• instDecidableEqNum = decEqNum✝

instance instZeroNum : Zero Num

Equations

• instZeroNum = { zero := Num.zero }

instance instOneNum : One Num

Equations

• instOneNum = { one := Num.pos 1 }

instance instInhabitedNum : Inhabited Num

Equations

• instInhabitedNum = { default := 0 }

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

instance instDecidableEqZNum : DecidableEq ZNum

Equations

• instDecidableEqZNum = decEqZNum✝

instance instZeroZNum : Zero ZNum

Equations

• instZeroZNum = { zero := ZNum.zero }

instance instOneZNum : One ZNum

Equations

• instOneZNum = { one := ZNum.pos 1 }

instance instInhabitedZNum : Inhabited ZNum

Equations

• instInhabitedZNum = { default := 0 }

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.

Equations

• PosNum.bit b = bif b then PosNum.bit1 else PosNum.bit0

def PosNum.succ : PosNum → PosNum

The successor of a PosNum.

Equations

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

def PosNum.isOne : PosNum → Bool

Returns a boolean for whether the PosNum is one.

Equations

• PosNum.one.isOne = true
• x✝.isOne = false

def PosNum.add : PosNum → PosNum → PosNum

Addition of two PosNums.

Equations

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

instance PosNum.instAdd : Add PosNum

Equations

• PosNum.instAdd = { add := PosNum.add }

def PosNum.pred' : PosNum → Num

The predecessor of a PosNum as a Num.

Equations

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

def PosNum.pred (a : PosNum) : PosNum

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

Equations

• a.pred = Num.casesOn a.pred' 1 id

def PosNum.size : PosNum → PosNum

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

def PosNum.natSize : PosNum → ℕ

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

def PosNum.mul (a : PosNum) : PosNum → 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

instance PosNum.instMul : Mul PosNum

Equations

• PosNum.instMul = { mul := PosNum.mul }

def PosNum.ofNatSucc : ℕ → PosNum

ofNatSucc n is the PosNum corresponding to n + 1.

Equations

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

def PosNum.ofNat (n : ℕ) : PosNum

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

Equations

• PosNum.ofNat n = PosNum.ofNatSucc n.pred

@[instance 100]

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

Equations

• PosNum.instOfNatHAddNatOfNat = { ofNat := PosNum.ofNat (n + 1) }

def PosNum.cmp : PosNum → PosNum → Ordering

Ordering of PosNums.

Equations

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

instance PosNum.instLT : LT PosNum

Equations

• PosNum.instLT = { lt := fun (a b : PosNum) => a.cmp b = Ordering.lt }

instance PosNum.instLE : LE PosNum

Equations

• PosNum.instLE = { le := fun (a b : PosNum) => ¬b < a }

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

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

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

Equations

• ↑PosNum.one = 1
• ↑n.bit0 = ↑n + ↑n
• ↑n.bit1 = ↑n + ↑n + 1

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

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

Equations

• ↑Num.zero = 0
• ↑(Num.pos p) = ↑p

@[instance 900]

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

Equations

• posNumCoe = { coe := castPosNum }

@[instance 900]

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

Equations

• numNatCoe = { coe := castNum }

instance instReprPosNum : Repr PosNum

Equations

• instReprPosNum = { reprPrec := fun (n : PosNum) (x : ℕ) => repr ↑n }

instance instReprNum : Repr Num

Equations

• instReprNum = { reprPrec := fun (n : Num) (x : ℕ) => repr ↑n }

def Num.succ' : Num → PosNum

The successor of a Num as a PosNum.

Equations

• Num.zero.succ' = 1
• (Num.pos p).succ' = p.succ

def Num.succ (n : Num) : Num

The successor of a Num as a Num.

Equations

• n.succ = Num.pos n.succ'

def Num.add : Num → Num → Num

Addition of two Nums.

Equations

• Num.zero.add x✝ = x✝
• x✝.add Num.zero = x✝
• (Num.pos a).add (Num.pos b) = Num.pos (a + b)

instance Num.instAdd : Add Num

Equations

• Num.instAdd = { add := Num.add }

def Num.bit0 : Num → Num

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

Equations

• Num.zero.bit0 = 0
• (Num.pos p).bit0 = Num.pos p.bit0

def Num.bit1 : Num → Num

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

Equations

• Num.zero.bit1 = 1
• (Num.pos p).bit1 = Num.pos p.bit1

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.

Equations

• Num.bit b = bif b then Num.bit1 else Num.bit0

def Num.size : Num → Num

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

Equations

• Num.zero.size = 0
• (Num.pos p).size = Num.pos p.size

def Num.natSize : Num → ℕ

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

Equations

• Num.zero.natSize = 0
• (Num.pos p).natSize = p.natSize

def Num.mul : Num → Num → Num

Multiplication of two Nums.

Equations

• Num.zero.mul x✝ = 0
• x✝.mul Num.zero = 0
• (Num.pos a).mul (Num.pos b) = Num.pos (a * b)

instance Num.instMul : Mul Num

Equations

• Num.instMul = { mul := Num.mul }

def Num.cmp : Num → Num → Ordering

Ordering of Nums.

Equations

• Num.zero.cmp Num.zero = Ordering.eq
• x✝.cmp Num.zero = Ordering.gt
• Num.zero.cmp x = Ordering.lt
• (Num.pos a).cmp (Num.pos b) = a.cmp b

instance Num.instLT : LT Num

Equations

• Num.instLT = { lt := fun (a b : Num) => a.cmp b = Ordering.lt }

instance Num.instLE : LE Num

Equations

• Num.instLE = { le := fun (a b : Num) => ¬b < a }

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

def Num.toZNum : Num → ZNum

Converts a Num to a ZNum.

Equations

• Num.zero.toZNum = 0
• (Num.pos p).toZNum = ZNum.pos p

def Num.toZNumNeg : Num → ZNum

Converts x : Num to -x : ZNum.

Equations

• Num.zero.toZNumNeg = 0
• (Num.pos p).toZNumNeg = ZNum.neg p

def Num.ofNat' : ℕ → Num

Converts a Nat to a Num.

Equations

• Num.ofNat' n = Nat.binaryRec 0 (fun (b : Bool) (x : ℕ) => bif b then Num.bit1 else Num.bit0) n

def ZNum.zNeg : ZNum → ZNum

The negation of a ZNum.

Equations

• ZNum.zero.zNeg = 0
• (ZNum.pos a).zNeg = ZNum.neg a
• (ZNum.neg a).zNeg = ZNum.pos a

instance ZNum.instNeg : Neg ZNum

Equations

• ZNum.instNeg = { neg := ZNum.zNeg }

def ZNum.abs : ZNum → Num

The absolute value of a ZNum as a Num.

Equations

• ZNum.zero.abs = 0
• (ZNum.pos a).abs = Num.pos a
• (ZNum.neg a).abs = Num.pos a

def ZNum.succ : ZNum → ZNum

The successor of a ZNum.

Equations

• ZNum.zero.succ = 1
• (ZNum.pos a).succ = ZNum.pos a.succ
• (ZNum.neg a).succ = a.pred'.toZNumNeg

def ZNum.pred : ZNum → ZNum

The predecessor of a ZNum.

Equations

• ZNum.zero.pred = ZNum.neg 1
• (ZNum.pos a).pred = a.pred'.toZNum
• (ZNum.neg a).pred = ZNum.neg a.succ

def ZNum.bit0 : ZNum → ZNum

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

Equations

• ZNum.zero.bit0 = 0
• (ZNum.pos a).bit0 = ZNum.pos a.bit0
• (ZNum.neg a).bit0 = ZNum.neg a.bit0

def ZNum.bit1 : ZNum → ZNum

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

Equations

• ZNum.zero.bit1 = 1
• (ZNum.pos a).bit1 = ZNum.pos a.bit1
• (ZNum.neg a).bit1 = ZNum.neg (Num.casesOn a.pred' 1 PosNum.bit1)

def ZNum.bitm1 : ZNum → ZNum

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

Equations

• ZNum.zero.bitm1 = ZNum.neg 1
• (ZNum.pos a).bitm1 = ZNum.pos (Num.casesOn a.pred' 1 PosNum.bit1)
• (ZNum.neg a).bitm1 = ZNum.neg a.bit1

def ZNum.ofInt' : ℤ → ZNum

Converts an Int to a ZNum.

Equations

• ZNum.ofInt' (Int.ofNat n) = (Num.ofNat' n).toZNum
• ZNum.ofInt' (Int.negSucc n) = (Num.ofNat' (n + 1)).toZNumNeg

def PosNum.sub' : PosNum → PosNum → ZNum

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

def PosNum.ofZNum' : ZNum → Option PosNum

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

Equations

• PosNum.ofZNum' (ZNum.pos p) = some p
• PosNum.ofZNum' x✝ = none

def PosNum.ofZNum : ZNum → PosNum

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

Equations

• PosNum.ofZNum (ZNum.pos p) = p
• PosNum.ofZNum x✝ = 1

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

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

Equations

• a.sub b = match a.sub' b with | ZNum.pos p => p | x => 1

instance PosNum.instSub : Sub PosNum

Equations

• PosNum.instSub = { sub := PosNum.sub }

def Num.ppred : Num → Option Num

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

Equations

• Num.zero.ppred = none
• (Num.pos p).ppred = some p.pred'

def Num.pred : Num → Num

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

Equations

• Num.zero.pred = 0
• (Num.pos p).pred = p.pred'

def Num.div2 : Num → Num

Divides a Num by 2

Equations

• Num.zero.div2 = 0
• (Num.pos PosNum.one).div2 = 0
• (Num.pos p.bit0).div2 = Num.pos p
• (Num.pos p.bit1).div2 = Num.pos p

def Num.ofZNum' : ZNum → Option Num

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

Equations

• Num.ofZNum' ZNum.zero = some 0
• Num.ofZNum' (ZNum.pos a) = some (Num.pos a)
• Num.ofZNum' (ZNum.neg a) = none

def Num.ofZNum : ZNum → Num

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

Equations

• Num.ofZNum (ZNum.pos p) = Num.pos p
• Num.ofZNum x✝ = 0

def Num.sub' : Num → Num → ZNum

Subtraction of two Nums, producing a ZNum.

Equations

• Num.zero.sub' Num.zero = 0
• (Num.pos a).sub' Num.zero = ZNum.pos a
• Num.zero.sub' (Num.pos b) = ZNum.neg b
• (Num.pos a).sub' (Num.pos b) = a.sub' b

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

Subtraction of two Nums, producing an Option Num.

Equations

• a.psub b = Num.ofZNum' (a.sub' b)

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

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

Equations

• a.sub b = Num.ofZNum (a.sub' b)

instance Num.instSub : Sub Num

Equations

• Num.instSub = { sub := Num.sub }

def ZNum.add : ZNum → ZNum → ZNum

Addition of ZNums.

Equations

• ZNum.zero.add x✝ = x✝
• x✝.add ZNum.zero = x✝
• (ZNum.pos a).add (ZNum.pos b) = ZNum.pos (a + b)
• (ZNum.pos a).add (ZNum.neg b) = a.sub' b
• (ZNum.neg a).add (ZNum.pos b) = b.sub' a
• (ZNum.neg a).add (ZNum.neg b) = ZNum.neg (a + b)

instance ZNum.instAdd : Add ZNum

Equations

• ZNum.instAdd = { add := ZNum.add }

def ZNum.mul : ZNum → ZNum → ZNum

Multiplication of ZNums.

Equations

• ZNum.zero.mul x✝ = 0
• x✝.mul ZNum.zero = 0
• (ZNum.pos a).mul (ZNum.pos b) = ZNum.pos (a * b)
• (ZNum.pos a).mul (ZNum.neg b) = ZNum.neg (a * b)
• (ZNum.neg a).mul (ZNum.pos b) = ZNum.neg (a * b)
• (ZNum.neg a).mul (ZNum.neg b) = ZNum.pos (a * b)

instance ZNum.instMul : Mul ZNum

Equations

• ZNum.instMul = { mul := ZNum.mul }

def ZNum.cmp : ZNum → ZNum → Ordering

Ordering on ZNums.

Equations

• ZNum.zero.cmp ZNum.zero = Ordering.eq
• (ZNum.pos a).cmp (ZNum.pos b) = a.cmp b
• (ZNum.neg a).cmp (ZNum.neg b) = b.cmp a
• (ZNum.pos a).cmp x✝ = Ordering.gt
• (ZNum.neg a).cmp x✝ = Ordering.lt
• x.cmp (ZNum.pos a) = Ordering.lt
• x.cmp (ZNum.neg a) = Ordering.gt

instance ZNum.instLT : LT ZNum

Equations

• ZNum.instLT = { lt := fun (a b : ZNum) => a.cmp b = Ordering.lt }

instance ZNum.instLE : LE ZNum

Equations

• ZNum.instLE = { le := fun (a b : ZNum) => ¬b < a }

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 r : Num) : Num × Num

Auxiliary definition for PosNum.divMod.

Equations

• d.divModAux q r = match Num.ofZNum' (r.sub' (Num.pos d)) with | some r' => (q.bit1, r') | none => (q.bit0, r)

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

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

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

Division of PosNum,

Equations

• n.div' d = (d.divMod n).fst

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

Modulus of PosNums.

Equations

• n.mod' d = (d.divMod n).snd

def Num.div : Num → Num → Num

Division of Nums, where x / 0 = 0.

Equations

• Num.zero.div x✝ = 0
• x✝.div Num.zero = 0
• (Num.pos a).div (Num.pos b) = a.div' b

def Num.mod : Num → Num → Num

Modulus of Nums.

Equations

• Num.zero.mod x✝ = 0
• x✝.mod Num.zero = x✝
• (Num.pos a).mod (Num.pos b) = a.mod' b

instance Num.instDiv : Div Num

Equations

• Num.instDiv = { div := Num.div }

instance Num.instMod : Mod Num

Equations

• Num.instMod = { mod := Num.mod }

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

Auxiliary definition for Num.gcd.

Equations

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

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

Greatest Common Divisor (GCD) of two Nums.

Equations

• a.gcd b = if a ≤ b then Num.gcdAux (a.natSize + b.natSize) a b else Num.gcdAux (b.natSize + a.natSize) b a

def ZNum.div : ZNum → ZNum → ZNum

Division of ZNum, where x / 0 = 0.

Equations

• ZNum.zero.div x✝ = 0
• x✝.div ZNum.zero = 0
• (ZNum.pos a).div (ZNum.pos b) = (a.div' b).toZNum
• (ZNum.pos a).div (ZNum.neg b) = (a.div' b).toZNumNeg
• (ZNum.neg a).div (ZNum.pos b) = ZNum.neg (a.pred' / Num.pos b).succ'
• (ZNum.neg a).div (ZNum.neg b) = ZNum.pos (a.pred' / Num.pos b).succ'

def ZNum.mod : ZNum → ZNum → ZNum

Modulus of ZNums.

Equations

• ZNum.zero.mod x✝ = 0
• (ZNum.pos n).mod x✝ = (Num.pos n % x✝.abs).toZNum
• (ZNum.neg n).mod x✝ = x✝.abs.sub' (n.pred' % x✝.abs).succ

instance ZNum.instDiv : Div ZNum

Equations

• ZNum.instDiv = { div := ZNum.div }

instance ZNum.instMod : Mod ZNum

Equations

• ZNum.instMod = { mod := ZNum.mod }

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

Greatest Common Divisor (GCD) of two ZNums.

Equations

• a.gcd b = a.abs.gcd b.abs

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

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

Equations

• ↑ZNum.zero = 0
• ↑(ZNum.pos a) = ↑a
• ↑(ZNum.neg a) = -↑a

@[instance 900]

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

Equations

• znumCoe = { coe := castZNum }

instance instReprZNum : Repr ZNum

Equations

• instReprZNum = { reprPrec := fun (n : ZNum) (x : ℕ) => repr ↑n }