Documentation

Batteries.Data.Rat.Basic

Basics for the Rational Numbers #

structure Rat :

Rational numbers, implemented as a pair of integers num / den such that the denominator is positive and the numerator and denominator are coprime.

  • mk' :: (
    • num : Int

      The numerator of the rational number is an integer.

    • den : Nat

      The denominator of the rational number is a natural number.

    • den_nz : self.den 0

      The denominator is nonzero.

    • reduced : self.num.natAbs.Coprime self.den

      The numerator and denominator are coprime: it is in "reduced form".

  • )
Instances For
    instance instReprRat :
    Equations
      theorem Rat.den_pos (self : Rat) :
      0 < self.den
      @[inline]
      def Rat.maybeNormalize (num : Int) (den g : Nat) (dvd_num : g num) (dvd_den : g den) (den_nz : den / g 0) (reduced : (num / g).natAbs.Coprime (den / g)) :

      Auxiliary definition for Rat.normalize. Constructs num / den as a rational number, dividing both num and den by g (which is the gcd of the two) if it is not 1.

      Equations
        Instances For
          theorem Rat.normalize.dvd_num {num : Int} {den g : Nat} (e : g = num.natAbs.gcd den) :
          g num
          theorem Rat.normalize.dvd_den {num : Int} {den g : Nat} (e : g = num.natAbs.gcd den) :
          g den
          theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den 0) (e : g = num.natAbs.gcd den) :
          den / g 0
          theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den 0) (e : g = num.natAbs.gcd den) :
          (num / g).natAbs.Coprime (den / g)
          @[inline]
          def Rat.normalize (num : Int) (den : Nat := 1) (den_nz : den 0 := by decide) :

          Construct a normalized Rat from a numerator and nonzero denominator. This is a "smart constructor" that divides the numerator and denominator by the gcd to ensure that the resulting rational number is normalized.

          Equations
            Instances For
              def mkRat (num : Int) (den : Nat) :

              Construct a rational number from a numerator and denominator. This is a "smart constructor" that divides the numerator and denominator by the gcd to ensure that the resulting rational number is normalized, and returns zero if den is zero.

              Equations
                Instances For
                  def Rat.ofInt (num : Int) :

                  Embedding of Int in the rational numbers.

                  Equations
                    Instances For
                      Equations
                        Equations
                          instance Rat.instOfNat {n : Nat} :
                          Equations
                            @[inline]
                            def Rat.isInt (a : Rat) :

                            Is this rational number integral?

                            Equations
                              Instances For
                                def Rat.divInt :
                                IntIntRat

                                Form the quotient n / d where n d : Int.

                                Equations
                                  Instances For

                                    Form the quotient n / d where n d : Int.

                                    Equations
                                      Instances For
                                        @[irreducible]
                                        def Rat.ofScientific (m : Nat) (s : Bool) (e : Nat) :

                                        Implements "scientific notation" 123.4e-5 for rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.ofScientific_def, Rat.ofScientific_true_def, or Rat.ofScientific_false_def instead.)

                                        Equations
                                          Instances For
                                            def Rat.blt (a b : Rat) :

                                            Rational number strictly less than relation, as a Bool.

                                            Equations
                                              Instances For
                                                instance Rat.instLT :
                                                Equations
                                                  instance Rat.instDecidableLt (a b : Rat) :
                                                  Decidable (a < b)
                                                  Equations
                                                    instance Rat.instLE :
                                                    Equations
                                                      instance Rat.instDecidableLe (a b : Rat) :
                                                      Equations
                                                        @[irreducible]
                                                        def Rat.mul (a b : Rat) :

                                                        Multiplication of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.mul_def instead.)

                                                        Equations
                                                          Instances For
                                                            instance Rat.instMul :
                                                            Equations
                                                              @[irreducible]
                                                              def Rat.inv (a : Rat) :

                                                              The inverse of a rational number. Note: inv 0 = 0. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.inv_def instead.)

                                                              Equations
                                                                Instances For
                                                                  def Rat.div :
                                                                  RatRatRat

                                                                  Division of rational numbers. Note: div a 0 = 0.

                                                                  Equations
                                                                    Instances For
                                                                      instance Rat.instDiv :

                                                                      Division of rational numbers. Note: div a 0 = 0. Written with a separate function Rat.div as a wrapper so that the definition is not unfolded at .instance transparency.

                                                                      Equations
                                                                        theorem Rat.add.aux (a b : Rat) {g ad bd : Nat} (hg : g = a.den.gcd b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) :
                                                                        let den := ad * b.den; let num := a.num * bd + b.num * ad; num.natAbs.gcd g = num.natAbs.gcd den
                                                                        @[irreducible]
                                                                        def Rat.add (a b : Rat) :

                                                                        Addition of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.add_def instead.)

                                                                        Equations
                                                                          Instances For
                                                                            instance Rat.instAdd :
                                                                            Equations
                                                                              def Rat.neg (a : Rat) :

                                                                              Negation of rational numbers.

                                                                              Equations
                                                                                Instances For
                                                                                  instance Rat.instNeg :
                                                                                  Equations
                                                                                    theorem Rat.sub.aux (a b : Rat) {g ad bd : Nat} (hg : g = a.den.gcd b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) :
                                                                                    let den := ad * b.den; let num := a.num * bd - b.num * ad; num.natAbs.gcd g = num.natAbs.gcd den
                                                                                    @[irreducible]
                                                                                    def Rat.sub (a b : Rat) :

                                                                                    Subtraction of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.sub_def instead.)

                                                                                    Equations
                                                                                      Instances For
                                                                                        instance Rat.instSub :
                                                                                        Equations
                                                                                          def Rat.floor (a : Rat) :

                                                                                          The floor of a rational number a is the largest integer less than or equal to a.

                                                                                          Equations
                                                                                            Instances For
                                                                                              def Rat.ceil (a : Rat) :

                                                                                              The ceiling of a rational number a is the smallest integer greater than or equal to a.

                                                                                              Equations
                                                                                                Instances For