structure Data.Ratio : Type

A rational number $\frac{\text{num}}{\text{den}}$ in canonical form.

Invariants:

• $\text{den} > 0$ (denominator is a positive natural number)
• $\gcd(|\text{num}|, \text{den}) = 1$ (fully reduced)

The sign is carried solely by num; den is always positive. These invariants make structural equality correct: two Ratio values are equal iff they represent the same rational number.

• num : Int

  The numerator (carries the sign).

• den : Nat

  The denominator (always positive).

• den_pos : self.den > 0

  Proof that the denominator is positive: $\text{den} > 0$.

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

  Proof of coprimality: $\gcd(|\text{num}|, \text{den}) = 1$.

def Data.instReprRatio.repr : Ratio → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.instReprRatio : Repr Ratio

Equations

• Data.instReprRatio = { reprPrec := Data.instReprRatio.repr }

def Data.Ratio.zero : Ratio

The rational number $0 = \frac{0}{1}$.

Equations

• Data.Ratio.zero = { num := 0, den := 1, den_pos := Nat.one_pos, coprime := Data.Ratio.coprime_one✝ }

def Data.Ratio.one : Ratio

The rational number $1 = \frac{1}{1}$.

Equations

• Data.Ratio.one = { num := 1, den := 1, den_pos := Nat.one_pos, coprime := Data.Ratio.one._proof_1 }

@[implicit_reducible]

instance Data.Ratio.instOfNatOfNatNat : OfNat Ratio 0

Equations

• Data.Ratio.instOfNatOfNatNat = { ofNat := Data.Ratio.zero }

@[implicit_reducible]

instance Data.Ratio.instOfNatOfNatNat_1 : OfNat Ratio 1

Equations

• Data.Ratio.instOfNatOfNatNat_1 = { ofNat := Data.Ratio.one }

@[implicit_reducible]

instance Data.Ratio.instInhabited : Inhabited Ratio

Equations

• Data.Ratio.instInhabited = { default := Data.Ratio.zero }

def Data.Ratio.mk' (n d : Int) (hd : d ≠ 0) : Ratio

Smart constructor: normalize $\frac{n}{d}$ to canonical form.

Given integers $n$ and $d \neq 0$:

1. Compute $g = \gcd(|n|, |d|)$
2. Adjust sign so denominator is positive
3. Divide both by $g$

$$\text{mk'}(n, d) = \frac{n / g}{d / g} \quad \text{where } g = \gcd(|n|, |d|)$$

Equations

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

@[inline]

def Data.Ratio.fromInt (n : Int) : Ratio

Create a ratio from an integer: $n \mapsto \frac{n}{1}$.

Equations

• Data.Ratio.fromInt n = { num := n, den := 1, den_pos := Nat.one_pos, coprime := ⋯ }

@[inline]

def Data.Ratio.fromNat (n : Nat) : Ratio

Create a ratio from a natural number: $n \mapsto \frac{n}{1}$.

Equations

• Data.Ratio.fromNat n = Data.Ratio.fromInt ↑n

def Data.Ratio.neg (r : Ratio) : Ratio

Negation: $-\frac{p}{q} = \frac{-p}{q}$. Preserves coprimality since $\gcd(|-p|, q) = \gcd(|p|, q)$.

Equations

• r.neg = { num := -r.num, den := r.den, den_pos := ⋯, coprime := ⋯ }

def Data.Ratio.abs (r : Ratio) : Ratio

Absolute value: $\left|\frac{p}{q}\right| = \frac{|p|}{q}$.

Equations

• r.abs = { num := ↑r.num.natAbs, den := r.den, den_pos := ⋯, coprime := ⋯ }

def Data.Ratio.add (r s : Ratio) : Ratio

Addition of rationals: $$\frac{a}{b} + \frac{c}{d} = \frac{ad + bc}{bd}$$ (normalized to canonical form).

Equations

• r.add s = Data.Ratio.mk' (r.num * ↑s.den + s.num * ↑r.den) (↑r.den * ↑s.den) ⋯

def Data.Ratio.sub (r s : Ratio) : Ratio

Subtraction: $\frac{a}{b} - \frac{c}{d} = \frac{a}{b} + \frac{-c}{d}$.

Equations

• r.sub s = r.add s.neg

def Data.Ratio.mul (r s : Ratio) : Ratio

Multiplication: $$\frac{a}{b} \times \frac{c}{d} = \frac{ac}{bd}$$ (normalized to canonical form).

Equations

• r.mul s = Data.Ratio.mk' (r.num * s.num) (↑r.den * ↑s.den) ⋯

def Data.Ratio.inv (r : Ratio) (h : r.num ≠ 0) : Ratio

Reciprocal: $\frac{q}{p}$ for $p \neq 0$. Swaps numerator and denominator, adjusting sign.

Equations

• r.inv h = Data.Ratio.mk' (↑r.den) r.num h

def Data.Ratio.div (r s : Ratio) (h : s.num ≠ 0) : Ratio

Division: $\frac{a}{b} \div \frac{c}{d} = \frac{a}{b} \times \frac{d}{c}$. Requires $c/d \neq 0$.

Equations

• r.div s h = r.mul (s.inv h)

@[implicit_reducible]

instance Data.Ratio.instLE : LE Ratio

Comparison: $\frac{a}{b} \leq \frac{c}{d} \iff ad \leq bc$ (since $b, d > 0$).

Equations

• Data.Ratio.instLE = { le := fun (r s : Data.Ratio) => r.num * ↑s.den ≤ s.num * ↑r.den }

@[implicit_reducible]

instance Data.Ratio.instLT : LT Ratio

Equations

• Data.Ratio.instLT = { lt := fun (r s : Data.Ratio) => r.num * ↑s.den < s.num * ↑r.den }

@[implicit_reducible]

instance Data.Ratio.instBEq : BEq Ratio

Equations

• Data.Ratio.instBEq = { beq := fun (r s : Data.Ratio) => r.num == s.num && r.den == s.den }

@[implicit_reducible]

instance Data.Ratio.instOrd : Ord Ratio

Equations

• Data.Ratio.instOrd = { compare := fun (r s : Data.Ratio) => compare (r.num * ↑s.den) (s.num * ↑r.den) }

@[implicit_reducible]

instance Data.Ratio.instAdd : Add Ratio

Equations

• Data.Ratio.instAdd = { add := Data.Ratio.add }

@[implicit_reducible]

instance Data.Ratio.instSub : Sub Ratio

Equations

• Data.Ratio.instSub = { sub := Data.Ratio.sub }

@[implicit_reducible]

instance Data.Ratio.instMul : Mul Ratio

Equations

• Data.Ratio.instMul = { mul := Data.Ratio.mul }

@[implicit_reducible]

instance Data.Ratio.instNeg : Neg Ratio

Equations

• Data.Ratio.instNeg = { neg := Data.Ratio.neg }

@[implicit_reducible]

instance Data.Ratio.instToString : ToString Ratio

Equations

• Data.Ratio.instToString = { toString := fun (r : Data.Ratio) => if (r.den == 1) = true then toString r.num else toString r.num ++ toString "/" ++ toString r.den }

def Data.Ratio.floor (r : Ratio) : Int

Floor: the greatest integer $\leq r$. $$\lfloor r \rfloor = \lfloor \text{num} / \text{den} \rfloor$$

Equations

• r.floor = r.num / ↑r.den

def Data.Ratio.ceil (r : Ratio) : Int

Ceiling: the least integer $\geq r$. $$\lceil r \rceil = -\lfloor -r \rfloor$$

Equations

• r.ceil = -(-r.num / ↑r.den)

def Data.Ratio.round (r : Ratio) : Int

Round to the nearest integer (half rounds away from zero). $$\text{round}(r) = \lfloor r + 1/2 \rfloor$$

Equations

• r.round = (2 * r.num + if r.num ≥ 0 then ↑r.den else -↑r.den) / (2 * ↑r.den)