Malachite for Azurite Users: Rationals
This page maps the operations of Azurite’s AzRat type,
its rational number in lowest terms, onto their Malachite counterparts on
Rational, from
the malachite-q crate. It is a companion of
Malachite for Azurite Users: Naturals and
Integers, whose
Conventions carry over; only what is new for rationals
is repeated here. The page covers Azurite as of commit 4932438 (2026-10-04). The
mapping index lists the whole family of pages.
Conventions
The types
An AzRat is a sign, an AzNat numerator magnitude, and an AzNat denominator, with proofs
that the denominator is nonzero, that the numerator and denominator are coprime, and that zero
carries the positive sign. A
Rational is the
same construction, a sign and two
Naturals in
lowest terms with a single zero, so both representations are canonical, equality is structural on
both sides, and the two print identically: "0", "4", "1/3", "-1/3".
Total functions
As on the other pages, Lean’s totality shows up where Malachite panics: x / 0 = 0, 0⁻¹ = 0
(the GroupWithZero convention), 0 ^ (-k) = 0, and a zero denominator passed to a constructor
gives 0 (Lean’s mkRat convention), while Malachite panics on division by zero, on the
reciprocal of zero, on 0.pow(-k), and on a zero denominator. Rows for such pairs are ✓, the two
agreeing wherever Azurite defines the result; Malachite’s
checked_div
is the Option form of division.
Typeclasses and traits
AzRat is a verified Mathlib Field and IsStrictOrderedRing with a LinearOrder, so the
whole linearly-ordered-field API applies to it, including Neg, Inv, Div, HShiftLeft and
HShiftRight by a Nat, OfNat literals, and NatCast/IntCast/RatCast. Malachite has no
field abstraction; the operators and the
malachite_base traits stand in.
Categories
Each definition falls into one of five categories:
| meaning | |
|---|---|
| ✓ | A Malachite function does the same thing. |
| ≈ | A Malachite function serves the same purpose, but its specification differs. The notes say how. |
| ⚙ | Malachite does not expose this algorithm or helper; the Malachite column or the notes say what to call instead. |
| — | No counterpart is needed, either because Rust handles it for you or because it is outside Malachite’s scope. The notes say which. |
| ✗ | Malachite does not fully support this yet, but will in a future version. |
Construction and conversion
| Azurite | Malachite | |
|---|---|---|
| ✓ | instance : OfNat AzRat 0, instance : Zero AzRat |
Rational::ZERO |
| ✓ | instance : OfNat AzRat 1, instance : One AzRat |
Rational::ONE |
| ✓ | ofSignAzNats (s : Bool) (num den : AzNat) : AzRat |
from_sign_and_naturals |
| ✓ | ofAzNats (num den : AzNat) : AzRat |
from_naturals |
| ✓ | ofAzInts (num den : AzInt) : AzRat |
from_integers |
| ✓ | AzNat.toAzRat (n : AzNat) : AzRat, instance : NatCast AzRat |
From<Natural> |
| ✓ | AzInt.toAzRat (z : AzInt) : AzRat, instance : IntCast AzRat |
From<Integer> |
| ✓ | UInt64.toAzRat, UInt32.toAzRat, UInt16.toAzRat, UInt8.toAzRat, USize.toAzRat, Int64.toAzRat, Int32.toAzRat, Int16.toAzRat, Int8.toAzRat, ISize.toAzRat |
From |
| ✓ | AzRat.num : AzNat, AzRat.den : AzNat |
to_numerator, to_denominator |
| ✓ | AzRat.sign : Bool |
Sign |
| ⚙ | numInt (q : AzRat) : AzInt |
to_numerator, Integer::from_sign_and_abs |
| — | ofRat (r : ℚ) : AzRat, toRat (q : AzRat) : ℚ, instance : RatCast AzRat, instance : NNRatCast AzRat |
Constructors. ofSignAzNats s n d reduces n / d, canonicalizes zero, and gives it sign s,
which is Rational::from_sign_and_naturals(s, n, d); ofAzNats and ofAzInts are
from_naturals and from_integers, the latter taking its sign from the two integers’ signs. The
difference is a zero denominator, 0 in Azurite and a panic in Malachite. The ten machine-integer
conversions and the two casts are Rational::from(x), and Rational has const_from_unsigneds
and const_from_signeds for compile-time constants, which need no Azurite counterpart.
Fields. q.num and q.den are the magnitudes q.to_numerator() and q.to_denominator()
(or numerator_ref() and denominator_ref() to borrow); q.sign is q >= 0, and sign() is
the Ordering against zero. numInt is the signed numerator, which Malachite does not expose
directly: Integer::from_sign_and_abs(q >= 0, q.to_numerator()). Malachite’s
mutate_numerator
family edits a rational in place; an AzRat is rebuilt with a constructor.
ofRat, toRat. The bridge to Mathlib’s ℚ, the specification side of Azurite’s proofs,
as toNat is on the naturals page; it has no counterpart.
Comparison
| Azurite | Malachite | |
|---|---|---|
| ✓ | cmp (x y : AzRat) : Ordering, instance : Ord AzRat, LE, LT, LinearOrder |
Ord, PartialOrd |
| ✓ | deriving DecidableEq |
Eq, PartialEq |
| ✓ | instance : Max AzRat, instance : Min AzRat |
Ord::max, Ord::min |
| ✓ | signOrd (x : AzRat) : Ordering |
Sign |
Comparison. Both compare exactly, Azurite by a staged algorithm (signs, then the position
relative to 1, then bit lengths, then a cross-multiplication) and Malachite similarly without
forming the cross products when it can avoid them. Malachite also compares a Rational against
Natural, Integer, and every primitive integer and float
(PartialOrd<Natural>
and siblings), and by magnitude
(OrdAbs);
Azurite converts the other operand with toAzRat and compares, and compares abs values.
Arithmetic
| Azurite | Malachite | |
|---|---|---|
| ✓ | add (x y : AzRat) : AzRat, instance : Add AzRat |
Add, AddAssign |
| ✓ | sub (x y : AzRat) : AzRat, instance : Sub AzRat |
Sub, SubAssign |
| ✓ | mul (x y : AzRat) : AzRat, instance : Mul AzRat |
Mul, MulAssign |
| ✓ | div (x y : AzRat) : AzRat, instance : Div AzRat |
Div, DivAssign |
| ✓ | neg (q : AzRat) : AzRat, instance : Neg AzRat |
Neg, NegAssign |
| ✓ | AzRat.abs (q : AzRat) : AzRat |
Abs, AbsAssign |
| ✓ | inv (q : AzRat) : AzRat, instance : Inv AzRat |
Reciprocal, ReciprocalAssign |
| ✓ | AzRat.pow (q : AzRat) (n : ℕ) : AzRat, the Field npow |
Pow<u64>, PowAssign |
| ✓ | AzRat.zpow (q : AzRat) : ℤ → AzRat, the Field zpow |
Pow<i64> |
| ✓ | AzRat.shiftLeft (x : AzRat) (n : Nat) : AzRat, instance : HShiftLeft AzRat Nat AzRat |
Shl, ShlAssign |
| ✓ | AzRat.shiftRight (x : AzRat) (n : Nat) : AzRat, instance : HShiftRight AzRat Nat AzRat |
Shr, ShrAssign |
| — | combineSigned (sx sy : Bool) (u v : AzNat) : Bool × AzNat |
|
| — | instance : Field AzRat, instance : IsStrictOrderedRing AzRat |
Field operations. The four operations agree, with x / 0 = 0 against Malachite’s panic (or
checked_div’s None); both keep results in lowest terms by reducing the cross pairs rather than
the products. inv is reciprocal(), with 0⁻¹ = 0 against a panic. pow is pow(e) with a
u64 exponent and zpow with an i64 one, where 0^(-k) is 0 in Azurite and a panic in
Malachite. Shifts multiply or divide by \(2^n\) without a GCD on either side; Malachite’s shift
count may be any primitive integer, a negative count reversing the direction. Malachite also has
Square,
AddMul,
and the other derived operations of the GMP and FLINT pages, which Azurite spells with the ring
operations, and functions with no Azurite counterpart at all
(approximate,
simplest_rational_in_interval,
continued fractions, roots). combineSigned is the sign bookkeeping shared by add and sub.
Rounding and logarithms
| Azurite | Malachite | |
|---|---|---|
| ✓ | round (q : AzRat) (mode : RoundingMode) : AzInt × Ordering |
RoundingFrom<Rational> for Integer |
| ✓ | floorLogBase2Abs (q : AzRat) : ℤ, ceilingLogBase2Abs (q : AzRat) : ℤ |
floor_log_base_2_abs, ceiling_log_base_2_abs |
| ✓ | floorLogBaseAbs (b : UInt64) (q : AzRat) : ℤ |
FloorLogBase<u64> |
| — | cmpPowAbs (b : UInt64) (e : ℤ) (q : AzRat) : Ordering, floorLogSearch |
Rounding to an integer. round q mode is Integer::rounding_from(q, mode): both return the
rounded integer and its Ordering against q, with ties to even under Nearest; Malachite’s
Exact mode panics unless q is an integer. Malachite’s
Floor
and
Ceiling
are the Floor and Ceiling modes with the Ordering dropped, and
RoundToMultiple
rounds to a multiple of another rational, which Azurite spells as round (q / m) mode scaled back.
Logarithms. The base-2 pair agrees exactly, both reading the exponent off the bit lengths of
the numerator and denominator. floorLogBaseAbs b q is q.floor_log_base(b) for a u64 base,
where Malachite requires q > 0 and Azurite takes |q| (returning 0 for q = 0); Azurite
brackets the exponent and binary-searches it, Malachite estimates it with floating-point
logarithms and corrects, and the results agree. Malachite’s
CeilingLogBase
and
CheckedLogBase
follow from the floor and a comparison of \(b^e\) with \(|q|\) (cmpPowAbs), and its
floor_log_base(&Rational) family takes a rational base, which Azurite does not. The three
FloorLogBase2/CeilingLogBase2/CheckedLogBase2 traits are the positive-only versions of the
_abs functions.
Strings and scientific notation
| Azurite | Malachite | |
|---|---|---|
| ✓ | toString (q : AzRat) : String, toChars, instance : ToString AzRat |
Display |
| ≈ | parse (s : String) : Option AzRat |
FromStr |
| ✓ | fromSci (s : String) (b : UInt64 := 10) : Option AzRat |
FromSciString |
| ✓ | toSci (q : AzRat) (o : SciOptions := {}) : Option String, toSciString (q : AzRat) : String |
ToSci |
| ✓ | toSciExact (q : AzRat) (o : SciOptions) : Bool |
fmt_sci_valid |
| ✓ | SciOptions, SciSizeOptions, SciFormat |
ToSciOptions, SciSizeOptions |
| ✓ | lengthAfterPoint (b : UInt64) (q : AzRat) : Option Nat |
length_after_point_in_small_base |
| — | toSciNumber, SciNumber, zeroScale, sizeScale, scaledRound, basePrimeFactors, countFactor, the fromSci helpers (splitLast, splitExponent, parseSignedDigits, …) |
|
| — | instance : ParsableElement AzRat |
Plain strings. Both print "-1/3" style, the sign on the numerator and no /1 for an
integer, so toString is Display (and Malachite’s Debug is the same). parse and
Rational::from_str both read num, -num, num/den and reduce an unreduced fraction, but
differ at the edges: Malachite accepts a single leading + on the numerator and on the
denominator and rejects a zero denominator, while Azurite rejects +, accepts 0x/0o/0b
prefixes through AzNat.parse, maps a zero denominator to 0, and rejects -0. Malachite’s
other bases are
FromStringBase
and
ToStringBase.
Scientific notation. Azurite’s fromSci and toSci are ports of Malachite’s
from_sci_string and to_sci, so the accepted language and the output agree digit for digit:
fromSci s b is Rational::from_sci_string_with_options(s, options) with options set to base
b (the rounding mode in
FromSciStringOptions
is for integer targets and does not affect a Rational), and toSci q o is
q.to_sci_with_options(o), with SciOptions’ base, mode, and size the ToSciOptions
fields base, rounding_mode, and size_options, and SciFormat’s negExpThreshold,
lowercase, eLowercase, forceExponentPlusSign, and includeTrailingZeros the remaining five.
The defaults coincide (base 10, Nearest, 16 significant digits, exponent notation below
\(10^{-6}\)). Malachite’s Exact rounding mode is Azurite’s toSciExact predicate, which is
fmt_sci_valid for Exact options; toSci returns none where to_sci_with_options panics
(invalid options, or Complete for a non-terminating expansion). Malachite’s
from_sci_string_simplest finds the simplest rational in the string’s rounding interval and has
no Azurite counterpart. lengthAfterPoint b q is q.length_after_point_in_small_base(b), the
number of digits after the point in a terminating base-b expansion.
Exhaustive generation
Azurite has no ExhaustiveGenerator instances for AzRat yet; Malachite’s
exhaustive_rationals
and its range variants are unmapped.