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

          Returns a boolean for whether the PosNum is one.

          Equations
          Instances For

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

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

                  Equations
                  Instances For
                    Equations
                    • PosNum.instOfNatPosNumHAddNatInstHAddInstAddNatOfNat = { ofNat := PosNum.ofNat (n + 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
                    @[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 +.

                      Equations
                      • x = match x with | Num.zero => 0 | Num.pos p => p
                      Instances For
                        @[deprecated]
                        instance posNumCoe {α : Type u_1} [One α] [Add α] :
                        Equations
                        • posNumCoe = { coe := castPosNum }
                        @[deprecated]
                        instance numNatCoe {α : Type u_1} [One α] [Add α] [Zero α] :
                        Equations
                        • numNatCoe = { coe := castNum }
                        Equations
                        instance instReprNum :
                        Equations

                        The successor of a Num as a PosNum.

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

                          The successor of a Num as a Num.

                          Equations
                          Instances For
                            def Num.add :
                            NumNumNum

                            Addition of two Nums.

                            Equations
                            Instances For
                              Equations
                              def Num.bit0 :
                              NumNum

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

                              Equations
                              Instances For
                                def Num.bit1 :
                                NumNum

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

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

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

                                    Equations
                                    Instances For

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

                                      Equations
                                      Instances For
                                        def Num.mul :
                                        NumNumNum

                                        Multiplication of two Nums.

                                        Equations
                                        Instances For
                                          Equations
                                          def Num.cmp :
                                          NumNumOrdering

                                          Ordering of Nums.

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

                                              Converts x : Num to -x : ZNum.

                                              Equations
                                              Instances For
                                                def Num.ofNat' :
                                                Num

                                                Converts a Nat to a Num.

                                                Equations
                                                Instances For

                                                  The negation of a ZNum.

                                                  Equations
                                                  Instances For
                                                    def ZNum.abs :
                                                    ZNumNum

                                                    The absolute value of a ZNum as a Num.

                                                    Equations
                                                    Instances For

                                                      The successor of a ZNum.

                                                      Equations
                                                      Instances For

                                                        The predecessor of a ZNum.

                                                        Equations
                                                        Instances For

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

                                                          Equations
                                                          Instances For

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

                                                            Equations
                                                            Instances For

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

                                                              Equations
                                                              Instances For

                                                                Converts an Int to a ZNum.

                                                                Equations
                                                                Instances For

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

                                                                  Equations
                                                                  Instances For

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

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

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

                                                                      Equations
                                                                      Instances For

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

                                                                        Equations
                                                                        Instances For
                                                                          def Num.pred :
                                                                          NumNum

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

                                                                          Equations
                                                                          Instances For
                                                                            def Num.div2 :
                                                                            NumNum

                                                                            Divides a Num by 2

                                                                            Equations
                                                                            Instances For

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

                                                                              Equations
                                                                              Instances For

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

                                                                                Equations
                                                                                Instances For
                                                                                  def Num.sub' :
                                                                                  NumNumZNum

                                                                                  Subtraction of two Nums, producing a ZNum.

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

                                                                                    Subtraction of two Nums, producing an Option Num.

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

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

                                                                                      Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                        def ZNum.add :
                                                                                        ZNumZNumZNum

                                                                                        Addition of ZNums.

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

                                                                                          Multiplication of ZNums.

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

                                                                                            Ordering on ZNums.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              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
                                                                                              Instances For

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

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

                                                                                                  Division of PosNum,

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

                                                                                                    Modulus of PosNums.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      def Num.div :
                                                                                                      NumNumNum

                                                                                                      Division of Nums, where x / 0 = 0.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def Num.mod :
                                                                                                        NumNumNum

                                                                                                        Modulus of Nums.

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

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              def ZNum.div :
                                                                                                              ZNumZNumZNum

                                                                                                              Division of ZNum, where x / 0 = 0.

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

                                                                                                                Modulus of ZNums.

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

                                                                                                                  Greatest Common Divisor (GCD) of two ZNums.

                                                                                                                  Equations
                                                                                                                  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

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[deprecated]
                                                                                                                      instance znumCoe {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
                                                                                                                      Equations
                                                                                                                      • znumCoe = { coe := castZNum }
                                                                                                                      Equations