Std.Internal.Rat

Rational numbers for implementing decision procedures. We should not confuse them with the Batteries rational numbers, also used by Mathlib.

source

structure Std.Internal.Rat :

Type

num : Int
den : Nat

Instances For

source

instance Std.Internal.instInhabitedRat :

Inhabited Rat

Equations

Std.Internal.instInhabitedRat = { default := { num := default, den := default } }

source

instance Std.Internal.instBEqRat :

BEq Rat

Equations

Std.Internal.instBEqRat = { beq := Std.Internal.beqRat✝ }

source

instance Std.Internal.instDecidableEqRat :

DecidableEq Rat

Equations

Std.Internal.instDecidableEqRat = Std.Internal.decEqRat✝

source

instance Std.Internal.instToStringRat :

ToString Rat

Equations

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

source

instance Std.Internal.instReprRat :

Repr Rat

Equations

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

source

@[inline]

def Std.Internal.Rat.normalize (a : Rat) :

Rat

Equations

a.normalize = if (a.num.natAbs.gcd a.den == 1) = true then a else { num := a.num.tdiv ↑(a.num.natAbs.gcd a.den), den := a.den / a.num.natAbs.gcd a.den }

source

def Std.Internal.mkRat (num : Int) (den : Nat) :

Rat

Equations

Std.Internal.mkRat num den = if (den == 0) = true then { num := 0 } else { num := num, den := den }.normalize

source

def Std.Internal.Rat.isInt (a : Rat) :

Bool

Equations

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

source

def Std.Internal.Rat.lt (a b : Rat) :

Bool

Equations

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

source

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

Rat

Equations

a.mul b = { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(a.den.gcd b.num.natAbs), den := b.den / a.num.natAbs.gcd b.den * (a.den / a.den.gcd b.num.natAbs) }

source

def Std.Internal.Rat.inv (a : Rat) :

Rat

Equations

a.inv = if a.num < 0 then { num := -↑a.den, den := a.num.natAbs } else if (a.num == 0) = true then a else { num := ↑a.den, den := a.num.natAbs }

source

def Std.Internal.Rat.div (a b : Rat) :

Rat

Equations

a.div b = a.mul b.inv

source

def Std.Internal.Rat.add (a b : Rat) :

Rat

Equations

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

source

def Std.Internal.Rat.sub (a b : Rat) :

Rat

Equations

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

source

def Std.Internal.Rat.neg (a : Rat) :

Rat

Equations

a.neg = { num := -a.num, den := a.den }

source

def Std.Internal.Rat.floor (a : Rat) :

Int

Equations

a.floor = if (a.den == 1) = true then a.num else a.num / ↑a.den

source

def Std.Internal.Rat.ceil (a : Rat) :

Int

Equations

a.ceil = if (a.den == 1) = true then a.num else Int.Linear.cdiv a.num ↑a.den

source

instance Std.Internal.Rat.instLT :

LT Rat

Equations

Std.Internal.Rat.instLT = { lt := fun (a b : Std.Internal.Rat) => a.lt b = true }

source

instance Std.Internal.Rat.instDecidableLt (a b : Rat) :

Decidable (a < b)

Equations

a.instDecidableLt b = inferInstanceAs (Decidable (a.lt b = true))

source

instance Std.Internal.Rat.instLE :

LE Rat

Equations

Std.Internal.Rat.instLE = { le := fun (a b : Std.Internal.Rat) => ¬b < a }

source

instance Std.Internal.Rat.instDecidableLe (a b : Rat) :

Decidable (a ≤ b)

Equations

a.instDecidableLe b = inferInstanceAs (Decidable ¬b < a)

source

instance Std.Internal.Rat.instAdd :

Add Rat

Equations

Std.Internal.Rat.instAdd = { add := Std.Internal.Rat.add }

source

instance Std.Internal.Rat.instSub :

Sub Rat

Equations

Std.Internal.Rat.instSub = { sub := Std.Internal.Rat.sub }

source

instance Std.Internal.Rat.instNeg :

Neg Rat

Equations

Std.Internal.Rat.instNeg = { neg := Std.Internal.Rat.neg }

source

instance Std.Internal.Rat.instMul :

Mul Rat

Equations

Std.Internal.Rat.instMul = { mul := Std.Internal.Rat.mul }

source

instance Std.Internal.Rat.instDiv :

Div Rat

Equations

Std.Internal.Rat.instDiv = { div := fun (a b : Std.Internal.Rat) => a * b.inv }

source

instance Std.Internal.Rat.instOfNat {n : Nat} :

OfNat Rat n

Equations

Std.Internal.Rat.instOfNat = { ofNat := { num := ↑n } }

source

instance Std.Internal.Rat.instCoeInt :

Coe Int Rat

Equations

Std.Internal.Rat.instCoeInt = { coe := fun (num : Int) => { num := num } }