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

Instances For
    inductive Num :

    The type of nonnegative binary numbers, using PosNum.

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

    Instances For
      instance instZeroNum :
      Equations
      instance instOneNum :
      Equations
      Equations
      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)))

      Instances For
        Equations
        instance instOneZNum :
        Equations
        Equations
        def PosNum.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

        Returns a boolean for whether the PosNum is one.

        Equations

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

        Equations

        ofNatSucc n is the PosNum corresponding to n + 1.

        Equations

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

        Equations
        Equations
        instance PosNum.decidableLT :
        DecidableRel fun x x_1 => x < x_1
        Equations
        instance PosNum.decidableLE :
        DecidableRel fun x x_1 => x x_1
        Equations
        def castPosNum {α : Type u_1} [inst : One α] [inst : Add α] :
        PosNumα

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

        Equations
        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
        instance posNumCoe {α : Type u_1} [inst : One α] [inst : Add α] :
        Equations
        • posNumCoe = { coe := castPosNum }
        instance numNatCoe {α : Type u_1} [inst : One α] [inst : Add α] [inst : Zero α] :
        Equations
        • numNatCoe = { coe := castNum }
        Equations
        instance instReprNum :
        Equations

        The successor of a Num as a PosNum.

        Equations
        def Num.succ (n : Num) :

        The successor of a Num as a Num.

        Equations
        def Num.add :
        NumNumNum

        Addition of two Nums.

        Equations
        Equations
        def Num.bit0 :
        NumNum

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

        Equations
        def Num.bit1 :
        NumNum

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

        Equations
        def Num.bit (b : Bool) :
        NumNum

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

        Equations
        def Num.size :
        NumNum

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

        Equations

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

        Equations
        def Num.mul :
        NumNumNum

        Multiplication of two Nums.

        Equations
        Equations
        def Num.cmp :
        NumNumOrdering

        Ordering of Nums.

        Equations
        instance Num.instLTNum :
        Equations
        instance Num.instLENum :
        Equations
        instance Num.decidableLT :
        DecidableRel fun x x_1 => x < x_1
        Equations
        instance Num.decidableLE :
        DecidableRel fun x x_1 => x x_1
        Equations

        Converts a Num to a ZNum.

        Equations

        Converts x : Num to -x : ZNum.

        Equations
        def Num.ofNat' :
        Num

        Converts a Nat to a Num.

        Equations

        The negation of a ZNum.

        Equations
        def ZNum.abs :
        ZNumNum

        The absolute value of a ZNum as a Num.

        Equations

        The successor of a ZNum.

        Equations

        The predecessor of a ZNum.

        Equations

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

        Equations

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

        Equations

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

        Equations

        Converts an Int to a ZNum.

        Equations

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

        Equations

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

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

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

        Equations

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

        Equations
        def Num.pred :
        NumNum

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

        Equations
        def Num.div2 :
        NumNum

        Divides a Num by 2

        Equations

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

        Equations

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

        Equations
        def Num.sub' :
        NumNumZNum

        Subtraction of two Nums, producing a ZNum.

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

        Subtraction of two Nums, producing an Option Num.

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

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

        Equations
        Equations
        def ZNum.add :
        ZNumZNumZNum

        Addition of ZNums.

        Equations
        • One or more equations did not get rendered due to their size.
        def ZNum.mul :
        ZNumZNumZNum

        Multiplication of ZNums.

        Equations
        • One or more equations did not get rendered due to their size.
        def ZNum.cmp :

        Ordering on ZNums.

        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Equations
        instance ZNum.decidableLT :
        DecidableRel fun x x_1 => x < x_1
        Equations
        instance ZNum.decidableLE :
        DecidableRel fun x x_1 => x x_1
        Equations
        def PosNum.divModAux (d : PosNum) (q : Num) (r : Num) :

        Auxiliary definition for PosNum.divMod.

        Equations

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

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

        Division of PosNum,

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

        Modulus of PosNums.

        Equations
        def Num.div :
        NumNumNum

        Division of Nums, where x / 0 = 0.

        Equations
        def Num.mod :
        NumNumNum

        Modulus of Nums.

        Equations
        Equations
        Equations
        def Num.gcdAux :
        NumNumNum

        Auxiliary definition for Num.gcd.

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

        Greatest Common Divisor (GCD) of two Nums.

        Equations
        def ZNum.div :
        ZNumZNumZNum

        Division of ZNum, where x / 0 = 0.

        Equations
        • One or more equations did not get rendered due to their size.
        def ZNum.mod :
        ZNumZNumZNum

        Modulus of ZNums.

        Equations
        • One or more equations did not get rendered due to their size.
        def ZNum.gcd (a : ZNum) (b : ZNum) :

        Greatest Common Divisor (GCD) of two ZNums.

        Equations
        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
        instance znumCoe {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Add α] [inst : Neg α] :
        Equations
        • znumCoe = { coe := castZNum }
        Equations