Exact rationals with an IEEE sign

A rational number has no negative zero, but every IEEE binary format does. Converting a value through Rat therefore forgets whether a zero was -0 or +0. A cast or mixed-format operation cannot recover that sign from the rational value alone.

SignedRat is a rational together with the sign bit an IEEE format would store for it. For a nonzero value the sign bit is determined by the value, and the structure carries that fact as a proof field, so two SignedRats are equal exactly when their values and sign bits agree. Only a zero has a free sign bit.

The arithmetic operations implement the IEEE sign rules for exact results. A product or quotient has the exclusive-or of the operand signs. An exact zero sum is negative only when both operands are negative, which is the round-to-nearest rule. Callers use addWithCancellationSign to choose the sign of an exact cancellation for directed rounding.

Executable conversion uses this type as the exact domain of every binary destination. Rational sources such as posits and fixed point enter through ofRat, and binary sources decode through ofDyadic, which keeps the dyadic sign.

structure FloatLib.Numerics.SignedRat : Type

An exact rational together with the IEEE sign bit of its zero.

negative is the sign bit. For a nonzero value it is forced to decide (value < 0); for zero it distinguishes -0 from +0.

• value : ℚ

  The exact rational value; zero for both signed zeros.

• negative : Bool

  The IEEE sign bit.

• negative_eq_of_ne_zero : self.value ≠ 0 → self.negative = decide (self.value < 0)

  A nonzero value determines its sign bit.

def FloatLib.Numerics.instDecidableEqSignedRat.decEq (x✝ x✝¹ : SignedRat) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqSignedRat : DecidableEq SignedRat

theorem FloatLib.Numerics.SignedRat.ext {x y : SignedRat} (hvalue : x.value = y.value) (hnegative : x.negative = y.negative) : x = y

Two signed rationals are equal when their values and sign bits are equal.

theorem FloatLib.Numerics.SignedRat.ext_iff {x y : SignedRat} : x = y ↔ x.value = y.value ∧ x.negative = y.negative

@[inline]

def FloatLib.Numerics.SignedRat.sameValue (x y : SignedRat) : Bool

Numerical equality, ignoring the sign attached to zero.

Ordinary == remains structural, just like =. Use sameValue only when positive and negative zero should represent the same rational number.

@[simp]

theorem FloatLib.Numerics.SignedRat.sameValue_eq_true_iff (x y : SignedRat) : x.sameValue y = true ↔ x.value = y.value

sameValue compares exactly the underlying rational values.

def FloatLib.Numerics.SignedRat.toString (x : SignedRat) : String

A negative zero prints as -0; every other value prints as its rational value.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instToString : ToString SignedRat

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instRepr : Repr SignedRat

Constructors

@[inline]

def FloatLib.Numerics.SignedRat.ofRat (q : ℚ) : SignedRat

The signed rational of a rational; zero receives the positive sign.

@[simp]

theorem FloatLib.Numerics.SignedRat.value_ofRat (q : ℚ) : (ofRat q).value = q

ofRat keeps the rational value.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_ofRat (q : ℚ) : (ofRat q).negative = decide (q < 0)

ofRat marks exactly the negative rationals; zero is positive.

theorem FloatLib.Numerics.SignedRat.ofRat_value_of_ne_zero {x : SignedRat} (hvalue : x.value ≠ 0) : ofRat x.value = x

A nonzero signed rational is recovered from its value alone.

def FloatLib.Numerics.SignedRat.negZero : SignedRat

Negative zero, the value a signed rational adds to Rat.

@[simp]

theorem FloatLib.Numerics.SignedRat.value_negZero : negZero.value = 0

Negative zero has value zero.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_negZero : negZero.negative = true

Negative zero carries the negative sign bit.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instZero : Zero SignedRat

@[simp]

theorem FloatLib.Numerics.SignedRat.value_zero : value 0 = 0

The zero of SignedRat has value zero.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instExactZero : ExactZero SignedRat

Both signed-zero representations are mathematical zero for checked exact arithmetic.

theorem FloatLib.Numerics.SignedRat.exactZero_test_eq_true_iff (x : SignedRat) : ExactZero.test x = true ↔ x.value = 0

The generic executable zero test recognizes exactly the zero-valued signed rationals.

theorem FloatLib.Numerics.SignedRat.exactZero_test_eq_false_iff (x : SignedRat) : ExactZero.test x = false ↔ x.value ≠ 0

Failing the generic zero test means that the rational value is nonzero.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_zero : negative 0 = false

The zero of SignedRat is positive zero.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instOfNat (n : ℕ) : OfNat SignedRat n

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instNatCast : NatCast SignedRat

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instIntCast : IntCast SignedRat

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instRatCast : RatCast SignedRat

def FloatLib.Numerics.SignedRat.ofDyadic (d : Dyadic) : SignedRat

The signed rational of an exact dyadic, keeping the dyadic sign.

Dyadic.toRat forgets the sign of a zero dyadic; this constructor is the sign-preserving replacement used when a binary format is decoded.

@[simp]

theorem FloatLib.Numerics.SignedRat.value_ofDyadic (d : Dyadic) : (ofDyadic d).value = d.toRat

ofDyadic keeps the exact rational value of the dyadic.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_ofDyadic (d : Dyadic) : (ofDyadic d).negative = d.negative

ofDyadic keeps the dyadic sign bit, so a negative dyadic zero stays negative.

Arithmetic

def FloatLib.Numerics.SignedRat.neg (x : SignedRat) : SignedRat

Negation flips the sign bit, including the sign of zero.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instNeg : Neg SignedRat

@[simp]

theorem FloatLib.Numerics.SignedRat.value_neg (x : SignedRat) : (-x).value = -x.value

Negation negates the value.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_neg (x : SignedRat) : (-x).negative = !x.negative

Negation flips the sign bit, also for zero.

theorem FloatLib.Numerics.SignedRat.ofDyadic_neg (d : Dyadic) : ofDyadic d.neg = -ofDyadic d

Negating a dyadic and then converting agrees with converting and then negating.

def FloatLib.Numerics.SignedRat.add (x y : SignedRat) : SignedRat

Exact addition with the round-to-nearest sign rule for an exact zero sum.

A nonzero sum takes the sign of its value. A zero sum is negative only when both operands are negative, so -0 + -0 = -0 while x + -x = +0 and -0 + +0 = +0.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instAdd : Add SignedRat

@[simp]

theorem FloatLib.Numerics.SignedRat.value_add (x y : SignedRat) : (x + y).value = x.value + y.value

Addition is exact on values.

theorem FloatLib.Numerics.SignedRat.negative_add_of_ne_zero {x y : SignedRat} (hsum : x.value + y.value ≠ 0) : (x + y).negative = decide (x.value + y.value < 0)

A nonzero exact sum has the sign of its value.

theorem FloatLib.Numerics.SignedRat.negative_add_of_eq_zero {x y : SignedRat} (hsum : x.value + y.value = 0) : (x + y).negative = (x.negative && y.negative)

An exact zero sum is negative exactly when both operands are negative.

def FloatLib.Numerics.SignedRat.addWithCancellationSign (negativeCancellation : Bool) (x y : SignedRat) : SignedRat

Exact addition with a caller-selected sign for cancellation between opposite signs.

Set negativeCancellation for rounding toward negative infinity. Same-sign zeros keep their sign in either mode: +0 + +0 = +0 and -0 + -0 = -0. A nonzero sum always takes the sign of its rational value.

@[simp]

theorem FloatLib.Numerics.SignedRat.value_addWithCancellationSign (negativeCancellation : Bool) (x y : SignedRat) : (addWithCancellationSign negativeCancellation x y).value = x.value + y.value

Choosing a cancellation sign leaves the exact rational sum unchanged.

@[simp]

theorem FloatLib.Numerics.SignedRat.addWithCancellationSign_false (x y : SignedRat) : addWithCancellationSign false x y = x + y

Positive cancellation uses the ordinary round-to-nearest signed-rational addition.

theorem FloatLib.Numerics.SignedRat.negative_addWithCancellationSign_of_ne_zero (negativeCancellation : Bool) {x y : SignedRat} (hsum : x.value + y.value ≠ 0) : (addWithCancellationSign negativeCancellation x y).negative = decide (x.value + y.value < 0)

A nonzero sum has its numerical sign, independent of the cancellation policy.

theorem FloatLib.Numerics.SignedRat.negative_addWithCancellationSign_of_eq_zero (negativeCancellation : Bool) {x y : SignedRat} (hsum : x.value + y.value = 0) : (addWithCancellationSign negativeCancellation x y).negative = if negativeCancellation = true then x.negative || y.negative else x.negative && y.negative

An exact zero sum follows the selected direction while preserving same-sign zeros.

def FloatLib.Numerics.SignedRat.sub (x y : SignedRat) : SignedRat

Subtraction is addition of the negation, as in IEEE 754.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instSub : Sub SignedRat

@[simp]

theorem FloatLib.Numerics.SignedRat.value_sub (x y : SignedRat) : (x - y).value = x.value - y.value

Subtraction is exact on values.

def FloatLib.Numerics.SignedRat.mul (x y : SignedRat) : SignedRat

Exact multiplication; the sign bit is the exclusive-or of the operand sign bits.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instMul : Mul SignedRat

@[simp]

theorem FloatLib.Numerics.SignedRat.value_mul (x y : SignedRat) : (x * y).value = x.value * y.value

Multiplication is exact on values.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_mul (x y : SignedRat) : (x * y).negative = (x.negative ^^ y.negative)

A product takes the exclusive-or of the operand signs, the IEEE rule for exact products.

def FloatLib.Numerics.SignedRat.div (x y : SignedRat) : SignedRat

Exact division; the sign bit is the exclusive-or of the operand sign bits.

Division by a zero value returns a zero value, following Rat; callers reject zero divisors before quantizing.

@[instance_reducible]

instance FloatLib.Numerics.SignedRat.instDiv : Div SignedRat

@[simp]

theorem FloatLib.Numerics.SignedRat.value_div (x y : SignedRat) : (x / y).value = x.value / y.value

Division is exact on values, with Rat division by zero giving zero.

@[simp]

theorem FloatLib.Numerics.SignedRat.negative_div (x y : SignedRat) : (x / y).negative = (x.negative ^^ y.negative)

A quotient takes the exclusive-or of the operand signs, the IEEE rule for exact quotients.