Basics for the Rational Numbers

structure Rat : Type

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

• )

instance instDecidableEqRat : DecidableEq Rat

Equations

• instDecidableEqRat = decEqRat✝

instance instInhabitedRat : Inhabited Rat

Equations

• instInhabitedRat = { default := { num := 0, den := 1, den_nz := instInhabitedRat.proof_1, reduced := instInhabitedRat.proof_2 } }

instance instToStringRat : ToString Rat

Equations

• instToStringRat = { toString := fun (a : Rat) => if a.den = 1 then toString a.num else toString "" ++ toString a.num ++ toString "/" ++ toString a.den ++ toString "" }

instance instReprRat : Repr Rat

Equations

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

theorem Rat.den_pos (self : Rat) : 0 < self.den

@[inline]

def Rat.maybeNormalize (num : Int) (den g : Nat) (den_nz : den / g ≠ 0) (reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)) : Rat

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

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

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.tdiv ↑g).natAbs.Coprime (den / g)

@[inline]

def Rat.normalize (num : Int) (den : Nat := 1) (den_nz : den ≠ 0 := by decide) : Rat

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

• Rat.normalize num den den_nz = Rat.maybeNormalize num den (num.natAbs.gcd den) ⋯ ⋯

def mkRat (num : Int) (den : Nat) : Rat

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

• mkRat num den = if den_nz : den = 0 then { num := 0, den := 1, den_nz := mkRat.proof_1, reduced := mkRat.proof_2 } else Rat.normalize num den den_nz

def Rat.ofInt (num : Int) : Rat

Embedding of Int in the rational numbers.

Equations

• Rat.ofInt num = { num := num, den := 1, den_nz := Rat.ofInt.proof_1, reduced := ⋯ }

instance Rat.instNatCast : NatCast Rat

Equations

• Rat.instNatCast = { natCast := fun (n : Nat) => Rat.ofInt ↑n }

instance Rat.instIntCast : IntCast Rat

Equations

• Rat.instIntCast = { intCast := Rat.ofInt }

instance Rat.instOfNat {n : Nat} : OfNat Rat n

Equations

• Rat.instOfNat = { ofNat := ↑n }

@[inline]

def Rat.isInt (a : Rat) : Bool

Is this rational number integral?

Equations

• a.isInt = (a.den == 1)

def Rat.divInt : Int → Int → Rat

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

Equations

• Rat.divInt x (Int.ofNat d) = inline (mkRat x d)
• Rat.divInt x (Int.negSucc d) = Rat.normalize (-x) d.succ ⋯

def Rat.«term_/._» : Lean.TrailingParserDescr

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

Equations

• Rat.«term_/._» = Lean.ParserDescr.trailingNode `Rat.«term_/._» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /. ") (Lean.ParserDescr.cat `term 71))

@[irreducible]

def Rat.ofScientific (m : Nat) (s : Bool) (e : Nat) : Rat

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

• Rat.ofScientific m s e = if s = true then Rat.normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

instance Rat.instOfScientific : OfScientific Rat

Equations

• Rat.instOfScientific = { ofScientific := fun (m : Nat) (s : Bool) (e : Nat) => Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) }

def Rat.blt (a b : Rat) : Bool

Rational number strictly less than relation, as a Bool.

Equations

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

instance Rat.instLT : LT Rat

Equations

• Rat.instLT = { lt := fun (x1 x2 : Rat) => x1.blt x2 = true }

instance Rat.instDecidableLt (a b : Rat) : Decidable (a < b)

Equations

• a.instDecidableLt b = inferInstanceAs (Decidable (a.blt b = true))

instance Rat.instLE : LE Rat

Equations

• Rat.instLE = { le := fun (a b : Rat) => b.blt a = false }

instance Rat.instDecidableLe (a b : Rat) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = inferInstanceAs (Decidable (b.blt a = false))

@[irreducible]

def Rat.mul (a b : Rat) : Rat

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

Equations

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

instance Rat.instMul : Mul Rat

Equations

• Rat.instMul = { mul := Rat.mul }

@[irreducible]

def Rat.inv (a : Rat) : 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

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

def Rat.div : Rat → Rat → Rat

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

Equations

• x1.div x2 = x1 * x2.inv

instance Rat.instDiv : Div Rat

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

• Rat.instDiv = { div := Rat.div }

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

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

Equations

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

instance Rat.instAdd : Add Rat

Equations

• Rat.instAdd = { add := Rat.add }

def Rat.neg (a : Rat) : Rat

Negation of rational numbers.

Equations

• a.neg = { num := -a.num, den := a.den, den_nz := ⋯, reduced := ⋯ }

instance Rat.instNeg : Neg Rat

Equations

• Rat.instNeg = { neg := Rat.neg }

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

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

Equations

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

instance Rat.instSub : Sub Rat

Equations

• Rat.instSub = { sub := Rat.sub }

def Rat.floor (a : Rat) : Int

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

Equations

• a.floor = if a.den = 1 then a.num else a.num / ↑a.den

def Rat.ceil (a : Rat) : Int

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

Equations

• a.ceil = if a.den = 1 then a.num else a.num / ↑a.den + 1