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 :

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

The type of positive binary numbers.

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

Instances For

instance instDecidableEqPosNum :

DecidableEq PosNum

Equations

instDecidableEqPosNum = decEqPosNum✝

instance instOnePosNum :

Equations

instOnePosNum = { one := PosNum.one }

instance instInhabitedPosNum :

Inhabited PosNum

Equations

instInhabitedPosNum = { default := 1 }

inductive Num :

zero: Num
pos: PosNum → Num

The type of nonnegative binary numbers, using PosNum.

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

Instances For

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 :

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

Instances For

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

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.

Equations

PosNum.isOne x = match x with | PosNum.one => true | x => false

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 :

Equations

PosNum.instAddPosNum = { add := PosNum.add }

def PosNum.pred' :

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

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

Equations

PosNum.pred a = Num.casesOn (PosNum.pred' a) 1 id

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 :

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 :

Equations

PosNum.instMulPosNum = { mul := PosNum.mul }

def PosNum.ofNatSucc :

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

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

Equations

PosNum.ofNat n = PosNum.ofNatSucc (Nat.pred n)

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 :

Equations

PosNum.instLTPosNum = { lt := fun a b => PosNum.cmp a b = Ordering.lt }

instance PosNum.instLEPosNum :

Equations

PosNum.instLEPosNum = { le := fun a b => ¬b < a }

instance PosNum.decidableLT :

DecidableRel fun x x_1 => x < x_1

Equations

PosNum.decidableLT x x = match x, x with | a, b => id inferInstance

instance PosNum.decidableLE :

DecidableRel fun x x_1 => x ≤ x_1

Equations

PosNum.decidableLE x x = match x, x with | a, b => id inferInstance

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

PosNum → α

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

Equations

castPosNum PosNum.one = 1
castPosNum (PosNum.bit0 n) = bit0 (castPosNum n)
castPosNum (PosNum.bit1 n) = bit1 (castPosNum n)

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

Num → α

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

Equations

castNum x = match x with | Num.zero => 0 | Num.pos p => castPosNum p

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

CoeTC PosNum α

Equations

posNumCoe = { coe := castPosNum }

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

Equations

numNatCoe = { coe := castNum }

instance instReprPosNum :

Equations

instReprPosNum = { reprPrec := fun n x => repr (castPosNum n) }

instance instReprNum :

Equations

instReprNum = { reprPrec := fun n x => repr (castNum n) }

def Num.succ' :

The successor of a Num as a PosNum.

Equations

Num.succ' x = match x with | Num.zero => 1 | Num.pos p => PosNum.succ p

def Num.succ (n : Num) :

The successor of a Num as a Num.

Equations

Num.succ n = Num.pos (Num.succ' n)

Num → Num → Num

Addition of two Nums.

Equations

Num.add x x = match x, x with | Num.zero, a => a | b, Num.zero => b | Num.pos a, Num.pos b => Num.pos (a + b)

instance Num.instAddNum :

Equations

Num.instAddNum = { add := Num.add }

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

Equations

Num.bit0 x = match x with | Num.zero => 0 | Num.pos n => Num.pos (PosNum.bit0 n)

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

Equations

Num.bit1 x = match x with | Num.zero => 1 | Num.pos n => Num.pos (PosNum.bit1 n)

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.size x = match x with | Num.zero => 0 | Num.pos n => Num.pos (PosNum.size n)

def Num.natSize :

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

Equations

Num.natSize x = match x with | Num.zero => 0 | Num.pos n => PosNum.natSize n

Num → Num → Num

Multiplication of two Nums.

Equations

Num.mul x x = match x, x with | Num.zero, x => 0 | x, Num.zero => 0 | Num.pos a, Num.pos b => Num.pos (a * b)

instance Num.instMulNum :

Equations

Num.instMulNum = { mul := Num.mul }

Num → Num → Ordering

Ordering of Nums.

Equations

Num.cmp x x = match x, x with | Num.zero, Num.zero => Ordering.eq | x, Num.zero => Ordering.gt | Num.zero, x => Ordering.lt | Num.pos a, Num.pos b => PosNum.cmp a b

instance Num.instLTNum :

Equations

Num.instLTNum = { lt := fun a b => Num.cmp a b = Ordering.lt }

instance Num.instLENum :

Equations

Num.instLENum = { le := fun a b => ¬b < a }

instance Num.decidableLT :

DecidableRel fun x x_1 => x < x_1

Equations

Num.decidableLT x x = match x, x with | a, b => id inferInstance

instance Num.decidableLE :

DecidableRel fun x x_1 => x ≤ x_1

Equations

Num.decidableLE x x = match x, x with | a, b => id inferInstance

def Num.toZNum :

Converts a Num to a ZNum.

Equations

Num.toZNum x = match x with | Num.zero => 0 | Num.pos a => ZNum.pos a

def Num.toZNumNeg :

Converts x : Num to -x : ZNum.

Equations

Num.toZNumNeg x = match x with | Num.zero => 0 | Num.pos a => ZNum.neg a

def Num.ofNat' :

Converts a Nat to a Num.

Equations

Num.ofNat' = Nat.binaryRec 0 fun b x => bif b then Num.bit1 else Num.bit0

def ZNum.zNeg :

The negation of a ZNum.

Equations

ZNum.zNeg x = match x with | ZNum.zero => 0 | ZNum.pos a => ZNum.neg a | ZNum.neg a => ZNum.pos a

instance ZNum.instNegZNum :

Equations

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

The absolute value of a ZNum as a Num.

Equations

ZNum.abs x = match x with | ZNum.zero => 0 | ZNum.pos a => Num.pos a | ZNum.neg a => Num.pos a

def ZNum.succ :

The successor of a ZNum.

Equations

ZNum.succ x = match x with | ZNum.zero => 1 | ZNum.pos a => ZNum.pos (PosNum.succ a) | ZNum.neg a => Num.toZNumNeg (PosNum.pred' a)

def ZNum.pred :

The predecessor of a ZNum.

Equations

ZNum.pred x = match x with | ZNum.zero => ZNum.neg 1 | ZNum.pos a => Num.toZNum (PosNum.pred' a) | ZNum.neg a => ZNum.neg (PosNum.succ a)

def ZNum.bit0 :

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

Equations

ZNum.bit0 x = match x with | ZNum.zero => 0 | ZNum.pos n => ZNum.pos (PosNum.bit0 n) | ZNum.neg n => ZNum.neg (PosNum.bit0 n)

def ZNum.bit1 :

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

Equations

ZNum.bit1 x = match x with | ZNum.zero => 1 | ZNum.pos n => ZNum.pos (PosNum.bit1 n) | ZNum.neg n => ZNum.neg (Num.casesOn (PosNum.pred' n) 1 PosNum.bit1)

def ZNum.bitm1 :

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

Equations

ZNum.bitm1 x = match x with | ZNum.zero => ZNum.neg 1 | ZNum.pos n => ZNum.pos (Num.casesOn (PosNum.pred' n) 1 PosNum.bit1) | ZNum.neg n => ZNum.neg (PosNum.bit1 n)

def ZNum.ofInt' :

Converts an Int to a ZNum.

Equations

ZNum.ofInt' x = match x with | Int.ofNat n => Num.toZNum (Num.ofNat' n) | Int.negSucc n => Num.toZNumNeg (Num.ofNat' (n + 1))

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.

Equations

PosNum.ofZNum' x = match x with | ZNum.pos p => some p | x => none

def PosNum.ofZNum :

ZNum → PosNum

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

Equations

PosNum.ofZNum x = match x with | ZNum.pos p => p | x => 1

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

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

Equations

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

instance PosNum.instSubPosNum :

Equations

PosNum.instSubPosNum = { sub := PosNum.sub }

def Num.ppred :

Num → Option Num

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

Equations

Num.ppred x = match x with | Num.zero => none | Num.pos p => some (PosNum.pred' p)

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

Equations

Num.pred x = match x with | Num.zero => 0 | Num.pos p => PosNum.pred' p

Divides a Num by 2

Equations

Num.div2 x = match x with | Num.zero => 0 | Num.pos PosNum.one => 0 | Num.pos (PosNum.bit0 p) => Num.pos p | Num.pos (PosNum.bit1 p) => 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' x = match x with | ZNum.zero => some 0 | ZNum.pos p => some (Num.pos p) | ZNum.neg a => none

def Num.ofZNum :

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

Equations

Num.ofZNum x = match x with | ZNum.pos p => Num.pos p | x => 0

Num → Num → ZNum

Subtraction of two Nums, producing a ZNum.

Equations

Num.sub' x x = match x, x with | Num.zero, Num.zero => 0 | Num.pos a, Num.zero => ZNum.pos a | Num.zero, Num.pos b => ZNum.neg b | Num.pos a, Num.pos b => PosNum.sub' a b

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

Subtraction of two Nums, producing an Option Num.

Equations

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

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

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

Equations

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

instance Num.instSubNum :

Equations

Num.instSubNum = { sub := Num.sub }

ZNum → ZNum → ZNum

Addition of ZNums.

Equations

One or more equations did not get rendered due to their size.

instance ZNum.instAddZNum :

Equations

ZNum.instAddZNum = { add := ZNum.add }

ZNum → ZNum → ZNum

Multiplication of ZNums.

Equations

One or more equations did not get rendered due to their size.

instance ZNum.instMulZNum :

Equations

ZNum.instMulZNum = { mul := ZNum.mul }

ZNum → ZNum → Ordering

Ordering on ZNums.

Equations

One or more equations did not get rendered due to their size.

instance ZNum.instLTZNum :

Equations

ZNum.instLTZNum = { lt := fun a b => ZNum.cmp a b = Ordering.lt }

instance ZNum.instLEZNum :

Equations

ZNum.instLEZNum = { le := fun a b => ¬b < a }

instance ZNum.decidableLT :

DecidableRel fun x x_1 => x < x_1

Equations

ZNum.decidableLT x x = match x, x with | a, b => id inferInstance

instance ZNum.decidableLE :

DecidableRel fun x x_1 => x ≤ x_1

Equations

ZNum.decidableLE x x = match x, x with | a, b => id inferInstance

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

Auxiliary definition for PosNum.divMod.

Equations

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

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

Division of PosNum,

Equations

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

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

Modulus of PosNums.

Equations

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

Num → Num → Num

Division of Nums, where x / 0 = 0.

Equations

Num.div x x = match x, x with | Num.zero, x => 0 | x, Num.zero => 0 | Num.pos n, Num.pos d => PosNum.div' n d

Num → Num → Num

Modulus of Nums.

Equations

Num.mod x x = match x, x with | Num.zero, x => 0 | n, Num.zero => n | Num.pos n, Num.pos d => PosNum.mod' n d

instance Num.instDivNum :

Equations

Num.instDivNum = { div := Num.div }

instance Num.instModNum :

Equations

Num.instModNum = { mod := Num.mod }

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

Greatest Common Divisor (GCD) of two Nums.

Equations

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

ZNum → ZNum → ZNum

Division of ZNum, where x / 0 = 0.

Equations

One or more equations did not get rendered due to their size.

ZNum → ZNum → ZNum

Modulus of ZNums.

Equations

One or more equations did not get rendered due to their size.

instance ZNum.instDivZNum :

Equations

ZNum.instDivZNum = { div := ZNum.div }

instance ZNum.instModZNum :

Equations

ZNum.instModZNum = { mod := ZNum.mod }

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

Greatest Common Divisor (GCD) of two ZNums.

Equations

ZNum.gcd a b = Num.gcd (ZNum.abs a) (ZNum.abs b)

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

ZNum → α

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

Equations

castZNum x = match x with | ZNum.zero => 0 | ZNum.pos p => castPosNum p | ZNum.neg p => -castPosNum p

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

Equations

znumCoe = { coe := castZNum }

instance instReprZNum :

Equations

instReprZNum = { reprPrec := fun n x => repr (castZNum n) }