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

        Instances For

          Returns a boolean for whether the PosNum is one.

          Instances For

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

            Instances For

              Multiplication of two PosNums.

              Equations
              Instances For

                ofNatSucc n is the PosNum corresponding to n + 1.

                Equations
                Instances For

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

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

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

                    Equations
                    Instances For
                      @[deprecated]
                      def castNum {α : Type u_1} [One α] [Add α] [Zero α] :
                      Numα

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

                      Instances For
                        @[deprecated]
                        instance posNumCoe {α : Type u_1} [One α] [Add α] :
                        @[deprecated]
                        instance numNatCoe {α : Type u_1} [One α] [Add α] [Zero α] :

                        The successor of a Num as a PosNum.

                        Instances For
                          def Num.succ (n : Num) :

                          The successor of a Num as a Num.

                          Instances For
                            def Num.add :
                            NumNumNum

                            Addition of two Nums.

                            Instances For
                              def Num.bit0 :
                              NumNum

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

                              Instances For
                                def Num.bit1 :
                                NumNum

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

                                Instances For
                                  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.

                                  Instances For
                                    def Num.size :
                                    NumNum

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

                                    Instances For

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

                                      Instances For
                                        def Num.mul :
                                        NumNumNum

                                        Multiplication of two Nums.

                                        Instances For
                                          def Num.cmp :
                                          NumNumOrdering

                                          Ordering of Nums.

                                          Instances For
                                            instance Num.decidableLT :
                                            DecidableRel fun x x_1 => x < x_1
                                            instance Num.decidableLE :
                                            DecidableRel fun x x_1 => x x_1

                                            Converts a Num to a ZNum.

                                            Instances For

                                              Converts x : Num to -x : ZNum.

                                              Instances For
                                                def Num.ofNat' :
                                                Num

                                                Converts a Nat to a Num.

                                                Instances For

                                                  The negation of a ZNum.

                                                  Instances For
                                                    def ZNum.abs :
                                                    ZNumNum

                                                    The absolute value of a ZNum as a Num.

                                                    Instances For

                                                      The successor of a ZNum.

                                                      Instances For

                                                        The predecessor of a ZNum.

                                                        Instances For

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

                                                          Instances For

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

                                                            Instances For

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

                                                              Instances For

                                                                Converts an Int to a ZNum.

                                                                Instances For

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

                                                                  Instances For

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

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

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

                                                                      Instances For

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

                                                                        Instances For
                                                                          def Num.pred :
                                                                          NumNum

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

                                                                          Instances For
                                                                            def Num.div2 :
                                                                            NumNum

                                                                            Divides a Num by 2

                                                                            Instances For

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

                                                                              Instances For

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

                                                                                Instances For
                                                                                  def Num.sub' :
                                                                                  NumNumZNum

                                                                                  Subtraction of two Nums, producing a ZNum.

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

                                                                                    Subtraction of two Nums, producing an Option Num.

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

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

                                                                                      Instances For
                                                                                        def ZNum.add :
                                                                                        ZNumZNumZNum

                                                                                        Addition of ZNums.

                                                                                        Instances For
                                                                                          def ZNum.mul :
                                                                                          ZNumZNumZNum

                                                                                          Multiplication of ZNums.

                                                                                          Instances For
                                                                                            def ZNum.cmp :

                                                                                            Ordering on ZNums.

                                                                                            Instances For
                                                                                              instance ZNum.decidableLT :
                                                                                              DecidableRel fun x x_1 => x < x_1
                                                                                              instance ZNum.decidableLE :
                                                                                              DecidableRel fun x x_1 => x x_1
                                                                                              def PosNum.divModAux (d : PosNum) (q : Num) (r : Num) :

                                                                                              Auxiliary definition for PosNum.divMod.

                                                                                              Instances For

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

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

                                                                                                  Division of PosNum,

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

                                                                                                    Modulus of PosNums.

                                                                                                    Instances For
                                                                                                      def Num.div :
                                                                                                      NumNumNum

                                                                                                      Division of Nums, where x / 0 = 0.

                                                                                                      Instances For
                                                                                                        def Num.mod :
                                                                                                        NumNumNum

                                                                                                        Modulus of Nums.

                                                                                                        Instances For
                                                                                                          def Num.gcdAux :
                                                                                                          NumNumNum

                                                                                                          Auxiliary definition for Num.gcd.

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

                                                                                                            Greatest Common Divisor (GCD) of two Nums.

                                                                                                            Instances For
                                                                                                              def ZNum.div :
                                                                                                              ZNumZNumZNum

                                                                                                              Division of ZNum, where x / 0 = 0.

                                                                                                              Instances For
                                                                                                                def ZNum.mod :
                                                                                                                ZNumZNumZNum

                                                                                                                Modulus of ZNums.

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

                                                                                                                  Greatest Common Divisor (GCD) of two ZNums.

                                                                                                                  Instances For
                                                                                                                    @[deprecated]
                                                                                                                    def castZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
                                                                                                                    ZNumα

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

                                                                                                                    Instances For
                                                                                                                      @[deprecated]
                                                                                                                      instance znumCoe {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :