Documentation

Mathlib.Data.Num.Basic

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))

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

instance instDecidableEqPosNum :

DecidableEq PosNum

Equations

instDecidableEqPosNum = decEqPosNum✝

instance instOnePosNum :

Equations

instOnePosNum = { one := PosNum.one }

instance instInhabitedPosNum :

Inhabited PosNum

Equations

instInhabitedPosNum = { default := 1 }

inductive Num :

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 :

Equations

instZeroNum = { zero := Num.zero }

instance instOneNum :

Equations

instOneNum = { one := Num.pos 1 }

instance instInhabitedNum :

Equations

instInhabitedNum = { default := 0 }

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

instance instDecidableEqZNum :

DecidableEq ZNum

Equations

instDecidableEqZNum = decEqZNum✝

instance instZeroZNum :

Equations

instZeroZNum = { zero := ZNum.zero }

instance instOneZNum :

Equations

instOneZNum = { one := ZNum.pos 1 }

instance instInhabitedZNum :

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

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 :

Equations

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

def PosNum.pred' :

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

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

def PosNum.natSize :

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

Equations

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 :

Equations

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

def PosNum.ofNatSucc :

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 : ℕ) :

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 :

Equations

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

instance PosNum.instLE :

Equations

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

instance PosNum.decidableLT :

DecidableLT PosNum

Equations

x✝¹.decidableLT x✝ = id inferInstance

instance PosNum.decidableLE :

DecidableLE PosNum

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 α] :

Equations

numNatCoe = { coe := castNum }

instance instReprPosNum :

Equations

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

instance instReprNum :

Equations

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

def Num.succ' :

The successor of a Num as a PosNum.

Equations

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

def Num.succ (n : Num) :

The successor of a Num as a Num.

Equations

n.succ = Num.pos n.succ'

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 :

Equations

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

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

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

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

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 :

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

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 :

Equations

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

Num → Num → Ordering

Ordering of Nums.

Equations

instance Num.instLT :

Equations

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

instance Num.instLE :

Equations

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

instance Num.decidableLT :

DecidableLT Num

Equations

x✝¹.decidableLT x✝ = id inferInstance

instance Num.decidableLE :

DecidableLE Num

Equations

x✝¹.decidableLE x✝ = id inferInstance

def Num.toZNum :

Converts a Num to a ZNum.

Equations

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

def Num.toZNumNeg :

Converts x : Num to -x : ZNum.

Equations

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

def Num.ofNat' :

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 :

The negation of a ZNum.

Equations

instance ZNum.instNeg :

Equations

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

The absolute value of a ZNum as a Num.

Equations

def ZNum.succ :

The successor of a ZNum.

Equations

def ZNum.pred :

The predecessor of a ZNum.

Equations

def ZNum.bit0 :

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

Equations

def ZNum.bit1 :

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 :

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

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

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

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 :

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'

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

Equations

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

Divides a Num by 2

Equations

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 :

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

Num → Num → ZNum

Subtraction of two Nums, producing a ZNum.

Equations

def Num.psub (a b : Num) :

Subtraction of two Nums, producing an Option Num.

Equations

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

def Num.sub (a b : Num) :

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

Equations

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

instance Num.instSub :

Equations

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

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 :

Equations

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

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 :

Equations

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

ZNum → ZNum → Ordering

Ordering on ZNums.

Equations

instance ZNum.instLT :

Equations

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

instance ZNum.instLE :

Equations

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

instance ZNum.decidableLT :

DecidableLT ZNum

Equations

x✝¹.decidableLT x✝ = id inferInstance

instance ZNum.decidableLE :

DecidableLE ZNum

Equations

x✝¹.decidableLE x✝ = id inferInstance

def PosNum.divModAux (d : PosNum) (q r : 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) :

Division of PosNum

Equations

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

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

Modulus of PosNums.

Equations

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

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

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 :

Equations

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

instance Num.instMod :

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

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

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'

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 :

Equations

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

instance ZNum.instMod :

Equations

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

def ZNum.gcd (a b : ZNum) :

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 :

Equations

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