Basics for the Rational Numbers

ink

theorem Rat.ext_iff (x : Rat) (y : Rat) : x = y ↔ x.num = y.num ∧ x.den = y.den

ink

theorem Rat.ext (x : Rat) (y : Rat) (num : x.num = y.num) (den : x.den = y.den) : x = y

ink

structure Rat : Type

• mk' :: (

• The numerator of the rational number is an integer.

  num : Int

• The denominator of the rational number is a natural number.

  den : Nat

• The denominator is nonzero.

  den_nz : autoParam (den ≠ 0) _auto✝

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

  reduced : autoParam (Nat.coprime (Int.natAbs num) den) _auto✝
• )

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

ink

instance instDecidableEqRat : DecidableEq Rat

Equations

• instDecidableEqRat = decEqRat✝

ink

instance instInhabitedRat : Inhabited Rat

Equations

• instInhabitedRat = { default := Rat.mk' 0 1 }

ink

instance instToStringRat : ToString Rat

Equations

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

ink

instance instReprRat : Repr Rat

Equations

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

ink

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

ink

@[inline]

def Rat.maybeNormalize (num : Int) (den : Nat) (g : Nat) (den_nz : den / g ≠ 0) (reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (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

• Rat.maybeNormalize num den g den_nz reduced = if hg : g = 1 then Rat.mk' num den else Rat.mk' (Int.div num ↑g) (den / g)

ink

theorem Rat.normalize.den_nz {num : Int} {den : Nat} {g : Nat} (den_nz : den ≠ 0) (e : g = Nat.gcd (Int.natAbs num) den) : den / g ≠ 0

ink

theorem Rat.normalize.reduced {num : Int} {den : Nat} {g : Nat} (den_nz : den ≠ 0) (e : g = Nat.gcd (Int.natAbs num) den) : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

ink

@[inline]

def Rat.normalize (num : Int) (den : optParam Nat 1) (den_nz : autoParam (den ≠ 0) _auto✝) : 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

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

ink

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 Rat.mk' 0 1 else Rat.normalize num den

ink

def Rat.ofInt (num : Int) : Rat

Embedding of Int in the rational numbers.

Equations

• Rat.ofInt num = Rat.mk' num 1

ink

instance Rat.instIntCastRat : IntCast Rat

Equations

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

ink

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

Equations

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

ink

@[inline]

def Rat.isInt (a : Rat) : Bool

Is this rational number integral?

Equations

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

ink

def Rat.divInt : Int → Int → Rat

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

Equations

• Rat.divInt x x = match x, x with | n, Int.ofNat d => inline (mkRat n d) | n, Int.negSucc d => Rat.normalize (-n) (Nat.succ d)

ink

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

ink

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

Implements "scientific notation" 123.4e-5 for rational numbers.

Equations

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

ink

instance Rat.instOfScientificRat : OfScientific Rat

Equations

• Rat.instOfScientificRat = { ofScientific := Rat.ofScientific }

ink

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

ink

instance Rat.instLTRat : LT Rat

Equations

• Rat.instLTRat = { lt := fun x x_1 => Rat.blt x x_1 = true }

ink

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

Equations

• Rat.instDecidableLtRatInstLTRat a b = inferInstanceAs (Decidable (Rat.blt a b = true))

ink

instance Rat.instLERat : LE Rat

Equations

• Rat.instLERat = { le := fun a b => Rat.blt b a = false }

ink

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

Equations

• Rat.instDecidableLeRatInstLERat a b = inferInstanceAs (Decidable (Rat.blt b a = false))

ink

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

• Rat.mul a b = let g1 := Nat.gcd (Int.natAbs a.num) b.den; let g2 := Nat.gcd (Int.natAbs b.num) a.den; Rat.mk' (Int.div a.num ↑g1 * Int.div b.num ↑g2) (a.den / g2 * (b.den / g1))

ink

instance Rat.instMulRat : Mul Rat

Equations

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

ink

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

• Rat.inv a = if h : a.num < 0 then Rat.mk' (-↑a.den) (Int.natAbs a.num) else if h : a.num > 0 then Rat.mk' (↑a.den) (Int.natAbs a.num) else a

ink

def Rat.div : Rat → Rat → Rat

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

Equations

• Rat.div x x = x * Rat.inv x

ink

instance Rat.instDivRat : 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.instDivRat = { div := Rat.div }

ink

theorem Rat.add.aux (a : Rat) (b : Rat) {g : Nat} {ad : Nat} {bd : Nat} (hg : g = Nat.gcd a.den 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; Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den

ink

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

ink

instance Rat.instAddRat : Add Rat

Equations

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

ink

def Rat.neg (a : Rat) : Rat

Negation of rational numbers.

Equations

• Rat.neg a = Rat.mk' (-a.num) a.den

ink

instance Rat.instNegRat : Neg Rat

Equations

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

ink

theorem Rat.sub.aux (a : Rat) (b : Rat) {g : Nat} {ad : Nat} {bd : Nat} (hg : g = Nat.gcd a.den 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; Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den

ink

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

ink

instance Rat.instSubRat : Sub Rat

Equations

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

ink

def Rat.floor (a : Rat) : Int

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

Equations

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

ink

def Rat.ceil (a : Rat) : Int

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

Equations

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