The values of the doubles of the model

The doubles of the model (Ratpoints.Double) are bits, with the operations of the C language and of the C library on them; the specification gives a double its value in ℚ extended by ⊥ and ⊤ (Ratpoints.doubleValue), which is ±∞ for the largest exponent field and the exact value Ratpoints.Double.toRat otherwise (Ratpoints.Double.doubleValue_bits, Ratpoints.Double.doubleValue_eq_toRat). This file proves that the operations do on the values what the C code relies on: a double that is not a NaN has an order value, its bits without the sign bit, negated when the sign bit is set (Ratpoints.Double.orderValue), in which its value is strictly increasing (Ratpoints.Double.strictMonoOn_valueOfOrderValue), so that the comparisons of the C language are the order of the values (Ratpoints.Double.lt_eq_true_iff, Ratpoints.Double.le_eq_true_iff, Ratpoints.Double.beq_eq_true_iff) and nextafter steps to the neighbouring double (Ratpoints.Double.orderValue_nextUp, Ratpoints.Double.nextUp_le_of_lt, and downwards Ratpoints.Double.orderValue_nextDown, the step upwards of the negation by Ratpoints.Double.nextDown_eq_neg_nextUp_neg); the negation and fabs act on the sign of the value; the double that Ratpoints.Double.assemble makes from a significand M and the exponent q of its last place has the fields of a subnormal, an infinity or a normal double (Ratpoints.Double.fields_assemble) and, in the range of the finite doubles, the value ±M 2 ^ q (Ratpoints.Double.toRat_assemble); the double Ratpoints.Double.ofDyadic nearest to ±m 2 ^ e, which ends with it, is exact when 0 < m < 2 ^ 53, e ≥ -1074 and m 2 ^ e < 2 ^ 1024 (Ratpoints.Double.ofDyadic_exact, where the last hypothesis reads Nat.log2 m + e ≤ 1023); hence (double)n is exact for |n| ≤ 2 ^ 53 (Ratpoints.Double.ofInt64_exact), ldexp and frexp are exact in the normal range (Ratpoints.Double.ldexp_exact, Ratpoints.Double.toRat_frexp_mul_zpow_eq_and_bounds), and the conversions to long and unsigned long truncate (Ratpoints.Double.toInt_toInt64, Ratpoints.Double.toNat_toUInt64).

Main definitions

• Ratpoints.Double.maxOrderValue, Ratpoints.Double.magnitudeUnits, Ratpoints.Double.orderValueUnits, Ratpoints.Double.valueOfOrderValue: the order value of +∞, and the value of the doubles of an order value.

Main statements

• Ratpoints.Double.doubleValue_eq_valueOfOrderValue, Ratpoints.Double.strictMonoOn_valueOfOrderValue: the value of a double that is not a NaN is that of its order value, strictly increasing in it.
• Ratpoints.Double.lt_eq_true_iff, Ratpoints.Double.le_eq_true_iff, Ratpoints.Double.beq_eq_true_iff: the comparisons of the C language off NaN.
• Ratpoints.Double.doubleValue_bits, Ratpoints.Double.doubleValue_eq_toRat: the value of a double by its fields, and that of a finite double.
• Ratpoints.Double.fields_assemble, Ratpoints.Double.isFinite_assemble_iff, Ratpoints.Double.toRat_assemble: the bits of a significand and an exponent.
• Ratpoints.Double.ofDyadic_exact, Ratpoints.Double.ofInt64_exact: the exact rounding of a dyadic number and the conversion of a long.
• Ratpoints.Double.ldexp_exact, Ratpoints.Double.toRat_frexp_mul_zpow_eq_and_bounds, Ratpoints.Double.toInt_toInt64, Ratpoints.Double.toNat_toUInt64: the functions of the C library and the conversions.
• Ratpoints.Double.orderValue_nextUp, Ratpoints.Double.nextUp_le_of_lt, Ratpoints.Double.nextDown_eq_neg_nextUp_neg, Ratpoints.Double.orderValue_nextDown, Ratpoints.Double.le_nextDown_of_lt: nextafter towards ±HUGE_VAL.

theorem Ratpoints.Double.expField_eq (x : Double) : x.expField = x.bits.toNat / 2 ^ 52 % 2 ^ 11

theorem Ratpoints.Double.fracField_eq (x : Double) : x.fracField = x.bits.toNat % 2 ^ 52

theorem Ratpoints.Double.toNat_and_mask (b : UInt64) : (b &&& 9223372036854775807).toNat = b.toNat % 2 ^ 63

theorem Ratpoints.Double.signBit_eq_decide (x : Double) : x.signBit = decide (2 ^ 63 ≤ x.bits.toNat)

theorem Ratpoints.Double.signBit_eq_true_iff (x : Double) : x.signBit = true ↔ 2 ^ 63 ≤ x.bits.toNat

theorem Ratpoints.Double.fracField_lt (x : Double) : x.fracField < 2 ^ 52

theorem Ratpoints.Double.expField_lt (x : Double) : x.expField < 2048

theorem Ratpoints.Double.toNat_bits (x : Double) : x.bits.toNat = (if x.signBit = true then 2 ^ 63 else 0) + (x.expField * 2 ^ 52 + x.fracField)

theorem Ratpoints.Double.expField_mul_add_fracField (x : Double) : x.expField * 2 ^ 52 + x.fracField = x.bits.toNat % 2 ^ 63

theorem Ratpoints.Double.isNaN_iff (x : Double) : x.isNaN = true ↔ IsNaN x.bits

theorem Ratpoints.Double.fields_eq_of_toNat_bits_eq {x : Double} {neg : Bool} {E F : ℕ} (hE : E < 2048) (hF : F < 2 ^ 52) (h : x.bits.toNat = (if neg = true then 2 ^ 63 else 0) + (E * 2 ^ 52 + F)) : x.signBit = neg ∧ x.expField = E ∧ x.fracField = F

The exact value of a finite double

theorem Ratpoints.Double.toRat_eq (x : Double) : x.toRat = ↑x.toDyadic.1 * 2 ^ x.toDyadic.2

theorem Ratpoints.Double.toDyadic_eq (x : Double) : x.toDyadic = ((if x.signBit = true then -1 else 1) * ↑(if x.expField = 0 then x.fracField else x.fracField + 2 ^ 52), if x.expField = 0 then -1074 else ↑x.expField - 1075)

theorem Ratpoints.Double.toRat_eq_fields (x : Double) : x.toRat = (if x.signBit = true then -1 else 1) * if x.expField = 0 then ↑x.fracField * 2 ^ (-1074) else (2 ^ 52 + ↑x.fracField) * 2 ^ (↑x.expField - 1075)

theorem Ratpoints.Double.doubleValue_bits (x : Double) : doubleValue x.bits = if x.expField = 2047 then if x.signBit = true then ⊥ else ⊤ else WithBotTop.coe x.toRat

The value that the specification gives the bits of a double (Ratpoints.doubleValue), by the fields of the model: ±∞ for the exponent field 2047 and the exact value Ratpoints.Double.toRat otherwise.

theorem Ratpoints.Double.doubleValue_eq_toRat {x : Double} (hx : x.isFinite = true) : doubleValue x.bits = WithBotTop.coe x.toRat

theorem Ratpoints.Double.doubleValue_eq_of_toDyadic_eq {x : Double} (hf : x.isFinite = true) {m e : ℤ} (hd : x.toDyadic = (m, e)) : doubleValue x.bits = WithBotTop.coe (↑(m * 2 ^ e.toNat) / ↑(2 ^ (-e).toNat))

The value of a finite double x with Ratpoints.Double.toDyadic x = (m, e) as the fraction of m 2 ^ max e 0 and 2 ^ max (-e) 0.

The order of the values

def Ratpoints.Double.maxOrderValue : ℕ

The order value (Ratpoints.Double.orderValue) of +∞, 2047 · 2 ^ 52, the bits of +∞; -maxOrderValue is that of -∞.

Equations

• Ratpoints.Double.maxOrderValue = 2047 * 2 ^ 52

def Ratpoints.Double.magnitudeUnits (a : ℕ) : ℕ

The value of the nonnegative finite double with the bits a, in units of the least subnormal 2 ^ (-1074): the fraction f for the exponent field 0, and (2 ^ 52 + f) 2 ^ (e - 1) for an exponent field e ≥ 1.

Equations

• Ratpoints.Double.magnitudeUnits a = if a / 2 ^ 52 = 0 then a % 2 ^ 52 else (2 ^ 52 + a % 2 ^ 52) * 2 ^ (a / 2 ^ 52 - 1)

def Ratpoints.Double.orderValueUnits (k : ℤ) : ℤ

Ratpoints.Double.magnitudeUnits with the sign of the order value k, the value of the finite doubles with the order value k in units of 2 ^ (-1074).

Equations

• Ratpoints.Double.orderValueUnits k = if k < 0 then -↑(Ratpoints.Double.magnitudeUnits k.natAbs) else ↑(Ratpoints.Double.magnitudeUnits k.natAbs)

def Ratpoints.Double.valueOfOrderValue (k : ℤ) : WithBotTop ℚ

The value of the doubles with the order value k (Ratpoints.Double.orderValue), for |k| ≤ Ratpoints.Double.maxOrderValue: ⊥ at -maxOrderValue, ⊤ at maxOrderValue, and Ratpoints.Double.orderValueUnits k times 2 ^ (-1074) between.

Equations

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

theorem Ratpoints.Double.magnitudeUnits_lt_two_pow (a : ℕ) : magnitudeUnits a < 2 ^ (52 + a / 2 ^ 52)

theorem Ratpoints.Double.two_pow_le_magnitudeUnits {a : ℕ} (h : a / 2 ^ 52 ≠ 0) : 2 ^ (51 + a / 2 ^ 52) ≤ magnitudeUnits a

theorem Ratpoints.Double.magnitudeUnits_strictMono : StrictMono magnitudeUnits

@[simp]

theorem Ratpoints.Double.magnitudeUnits_zero : magnitudeUnits 0 = 0

theorem Ratpoints.Double.orderValueUnits_strictMono : StrictMono orderValueUnits

theorem Ratpoints.Double.strictMonoOn_valueOfOrderValue : StrictMonoOn valueOfOrderValue (Set.Icc (-↑maxOrderValue) ↑maxOrderValue)

theorem Ratpoints.Double.orderValue_eq_mod (x : Double) : x.orderValue = if x.signBit = true then -↑(x.bits.toNat % 2 ^ 63) else ↑(x.bits.toNat % 2 ^ 63)

theorem Ratpoints.Double.orderValue_eq (x : Double) : x.orderValue = if x.signBit = true then -↑(x.expField * 2 ^ 52 + x.fracField) else ↑(x.expField * 2 ^ 52 + x.fracField)

theorem Ratpoints.Double.expField_lt_or_of_isNaN_eq_false {x : Double} (hx : x.isNaN = false) : x.expField < 2047 ∨ x.expField = 2047 ∧ x.fracField = 0

theorem Ratpoints.Double.natAbs_orderValue_le {x : Double} (hx : x.isNaN = false) : x.orderValue.natAbs ≤ maxOrderValue

theorem Ratpoints.Double.orderValue_mem_Icc {x : Double} (hx : x.isNaN = false) : x.orderValue ∈ Set.Icc (-↑maxOrderValue) ↑maxOrderValue

theorem Ratpoints.Double.magnitudeUnits_fields {E F : ℕ} (hF : F < 2 ^ 52) : magnitudeUnits (E * 2 ^ 52 + F) = if E = 0 then F else (2 ^ 52 + F) * 2 ^ (E - 1)

theorem Ratpoints.Double.orderValueUnits_natCast (n : ℕ) : orderValueUnits ↑n = ↑(magnitudeUnits n)

theorem Ratpoints.Double.orderValueUnits_neg_natCast (n : ℕ) : orderValueUnits (-↑n) = -↑(magnitudeUnits n)

theorem Ratpoints.Double.magnitudeUnits_mul_eq {E F : ℕ} (hF : F < 2 ^ 52) : ↑(magnitudeUnits (E * 2 ^ 52 + F)) * 2 ^ (-1074) = if E = 0 then ↑F * 2 ^ (-1074) else (2 ^ 52 + ↑F) * 2 ^ (↑E - 1075)

theorem Ratpoints.Double.valueOfOrderValue_natCast {k : ℕ} (hk : k < maxOrderValue) : valueOfOrderValue ↑k = WithBotTop.coe (↑(magnitudeUnits k) * 2 ^ (-1074))

theorem Ratpoints.Double.valueOfOrderValue_neg_natCast {k : ℕ} (hk : k < maxOrderValue) : valueOfOrderValue (-↑k) = WithBotTop.coe (-(↑(magnitudeUnits k) * 2 ^ (-1074)))

theorem Ratpoints.Double.doubleValue_eq_valueOfOrderValue {x : Double} (hx : x.isNaN = false) : doubleValue x.bits = valueOfOrderValue x.orderValue

theorem Ratpoints.Double.lt_eq_true_iff {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) : x.lt y = true ↔ doubleValue x.bits < doubleValue y.bits

theorem Ratpoints.Double.le_eq_true_iff {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) : x.le y = true ↔ doubleValue x.bits ≤ doubleValue y.bits

theorem Ratpoints.Double.beq_eq_true_iff {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) : x.beq y = true ↔ doubleValue x.bits = doubleValue y.bits

theorem Ratpoints.Double.isNaN_eq_false_iff (x : Double) : x.isNaN = false ↔ ¬IsNaN x.bits

The magnitude and the operations on the sign bit

theorem Ratpoints.Double.toNat_bits_eq_mod (x : Double) : x.bits.toNat = (if x.signBit = true then 2 ^ 63 else 0) + x.bits.toNat % 2 ^ 63

theorem Ratpoints.Double.isNaN_eq_false_iff_le (x : Double) : x.isNaN = false ↔ x.bits.toNat % 2 ^ 63 ≤ maxOrderValue

theorem Ratpoints.Double.signBit_and_mod_of_toNat_eq {x : Double} {s : Bool} {n : ℕ} (hn : n < 2 ^ 63) (h : x.bits.toNat = (if s = true then 2 ^ 63 else 0) + n) : x.signBit = s ∧ x.bits.toNat % 2 ^ 63 = n

theorem Ratpoints.Double.toNat_fabs (x : Double) : x.fabs.bits.toNat = x.bits.toNat % 2 ^ 63

theorem Ratpoints.Double.toNat_mod_fabs (x : Double) : x.fabs.bits.toNat % 2 ^ 63 = x.bits.toNat % 2 ^ 63

theorem Ratpoints.Double.signBit_fabs (x : Double) : x.fabs.signBit = false

theorem Ratpoints.Double.toNat_mod_neg (x : Double) : x.neg.bits.toNat % 2 ^ 63 = x.bits.toNat % 2 ^ 63

theorem Ratpoints.Double.toNat_bits_neg (x : Double) : x.neg.bits.toNat = (x.bits.toNat + 2 ^ 63) % 2 ^ 64

Flipping the sign bit adds 2 ^ 63 to the bits, modulo 2 ^ 64.

theorem Ratpoints.Double.signBit_neg (x : Double) : x.neg.signBit = !x.signBit

theorem Ratpoints.Double.bits_neg (x : Double) : x.neg.bits = x.bits + 9223372036854775808

theorem Ratpoints.Double.neg_neg (x : Double) : x.neg.neg = x

theorem Ratpoints.Double.orderValue_fabs (x : Double) : x.fabs.orderValue = ↑(x.bits.toNat % 2 ^ 63)

theorem Ratpoints.Double.orderValue_neg (x : Double) : x.neg.orderValue = -x.orderValue

theorem Ratpoints.Double.div_mod_eq_fields (x : Double) : x.bits.toNat % 2 ^ 63 / 2 ^ 52 = x.expField ∧ x.bits.toNat % 2 ^ 63 % 2 ^ 52 = x.fracField

theorem Ratpoints.Double.expField_eq_mod (x : Double) : x.expField = x.bits.toNat % 2 ^ 63 / 2 ^ 52

theorem Ratpoints.Double.fracField_eq_mod (x : Double) : x.fracField = x.bits.toNat % 2 ^ 63 % 2 ^ 52

theorem Ratpoints.Double.expField_neg (x : Double) : x.neg.expField = x.expField

theorem Ratpoints.Double.fracField_neg (x : Double) : x.neg.fracField = x.fracField

theorem Ratpoints.Double.expField_fabs (x : Double) : x.fabs.expField = x.expField

theorem Ratpoints.Double.fracField_fabs (x : Double) : x.fabs.fracField = x.fracField

theorem Ratpoints.Double.isNaN_fabs (x : Double) : x.fabs.isNaN = x.isNaN

theorem Ratpoints.Double.isNaN_neg (x : Double) : x.neg.isNaN = x.isNaN

theorem Ratpoints.Double.isFinite_neg (x : Double) : x.neg.isFinite = x.isFinite

theorem Ratpoints.Double.isFinite_fabs (x : Double) : x.fabs.isFinite = x.isFinite

theorem Ratpoints.Double.toRat_neg (x : Double) : x.neg.toRat = -x.toRat

theorem Ratpoints.Double.toRat_fabs (x : Double) : x.fabs.toRat = |x.toRat|

Doubles from their fields

theorem Ratpoints.Double.toNat_sign_or {neg : Bool} {n : ℕ} (hn : n < 2 ^ 63) : ((if neg = true then 9223372036854775808 else 0) ||| n.toUInt64).toNat = (if neg = true then 2 ^ 63 else 0) + n

theorem Ratpoints.Double.shiftLeft_or_eq {E F : ℕ} (hE : E < 2048) (hF : F < 2 ^ 52) : E.toUInt64 <<< 52 ||| F.toUInt64 = (E * 2 ^ 52 + F).toUInt64

theorem Ratpoints.Double.toNat_sign_or_or {neg : Bool} {E F : ℕ} (hE : E < 2048) (hF : F < 2 ^ 52) : ((if neg = true then 9223372036854775808 else 0) ||| E.toUInt64 <<< 52 ||| F.toUInt64).toNat = (if neg = true then 2 ^ 63 else 0) + (E * 2 ^ 52 + F)

theorem Ratpoints.Double.toRat_of_toNat_eq {x : Double} {neg : Bool} {E F : ℕ} (hE : E < 2047) (hF : F < 2 ^ 52) (h : x.bits.toNat = (if neg = true then 2 ^ 63 else 0) + (E * 2 ^ 52 + F)) : x.isFinite = true ∧ x.signBit = neg ∧ x.toRat = (if neg = true then -1 else 1) * if E = 0 then ↑F * 2 ^ (-1074) else (2 ^ 52 + ↑F) * 2 ^ (↑E - 1075)

theorem Ratpoints.Double.roundShift_of_nonpos {m : ℕ} {k : ℤ} (hk : k ≤ 0) : roundShift m k = m * 2 ^ (-k).toNat

The assembly of the bits

theorem Ratpoints.Double.ofSignificand_of_ne {neg : Bool} {M : ℕ} (q : ℤ) (h : M ≠ 2 ^ 53) : ofSignificand neg M q = assemble neg M q

theorem Ratpoints.Double.ofSignificand_two_pow (neg : Bool) (q : ℤ) : ofSignificand neg (2 ^ 53) q = assemble neg (2 ^ 52) (q + 1)

theorem Ratpoints.Double.fields_assemble (neg : Bool) {M : ℕ} (q : ℤ) (hM : M < 2 ^ 53) : (assemble neg M q).signBit = neg ∧ ((assemble neg M q).expField = if M < 2 ^ 52 then 0 else if 2047 ≤ q + 1075 then 2047 else (q + 1075).toNat) ∧ (assemble neg M q).fracField = if M < 2 ^ 52 then M else if 2047 ≤ q + 1075 then 0 else M - 2 ^ 52

The sign bit, the exponent field and the fraction of the double that Ratpoints.Double.assemble makes from a significand M < 2 ^ 53 and the exponent q of its last place: those of a subnormal or a zero for M < 2 ^ 52, of an infinity when the exponent field q + 1075 would reach 2047, and of a normal double otherwise.

theorem Ratpoints.Double.isFinite_assemble_iff {neg : Bool} {M : ℕ} {q : ℤ} (hM : M < 2 ^ 53) : (assemble neg M q).isFinite = true ↔ M < 2 ^ 52 ∨ q + 1075 < 2047

theorem Ratpoints.Double.toRat_assemble {neg : Bool} {M : ℕ} {q : ℤ} (hM : M < 2 ^ 53) (hsub : M < 2 ^ 52 → q = -1074) (hnorm : 2 ^ 52 ≤ M → -1074 ≤ q ∧ q + 1075 < 2047) : (assemble neg M q).toRat = (if neg = true then -1 else 1) * (↑M * 2 ^ q)

The value ±M 2 ^ q of the double that Ratpoints.Double.assemble makes from a significand M < 2 ^ 53 and the exponent q of its last place in the range of the finite doubles: q = -1074 for a subnormal or a zero (M < 2 ^ 52), and -1074 ≤ q with the exponent field q + 1075 below 2047 for a normal double.

theorem Ratpoints.Double.mul_two_pow_lt_two_pow_53 {m t : ℕ} (ht : m.log2 + t ≤ 52) : m * 2 ^ t < 2 ^ 53

theorem Ratpoints.Double.two_pow_le_mul_two_pow {m t : ℕ} (hm0 : m ≠ 0) (ht : m.log2 + t = 52) : 2 ^ 52 ≤ m * 2 ^ t

theorem Ratpoints.Double.natCast_mul_two_pow_mul_zpow (m : ℕ) {e q : ℤ} (h : q ≤ e) : ↑(m * 2 ^ (e - q).toNat) * 2 ^ q = ↑m * 2 ^ e

theorem Ratpoints.Double.ofDyadic_exact {neg : Bool} {m : ℕ} {e : ℤ} (hm0 : m ≠ 0) (hm : m < 2 ^ 53) (he : -1074 ≤ e) (he' : ↑m.log2 + e ≤ 1023) : (ofDyadic neg m e).isFinite = true ∧ (ofDyadic neg m e).signBit = neg ∧ (ofDyadic neg m e).toRat = (if neg = true then -1 else 1) * (↑m * 2 ^ e)

The neighbours

theorem Ratpoints.Double.isZero_eq_decide (x : Double) : x.isZero = decide (x.bits.toNat % 2 ^ 63 = 0)

theorem Ratpoints.Double.toNat_huge : huge.bits.toNat = maxOrderValue

theorem Ratpoints.Double.toNat_nextUp {x : Double} (hx : x.isNaN = false) (hi : x.bits ≠ huge.bits) : x.nextUp.bits.toNat = if x.bits.toNat % 2 ^ 63 = 0 then 1 else if x.signBit = true then x.bits.toNat - 1 else x.bits.toNat + 1

theorem Ratpoints.Double.orderValue_of_toNat_eq {x : Double} {s : Bool} {n : ℕ} (hn : n < 2 ^ 63) (h : x.bits.toNat = (if s = true then 2 ^ 63 else 0) + n) : (x.orderValue = if s = true then -↑n else ↑n) ∧ (x.isNaN = false ↔ n ≤ maxOrderValue)

The order value of a double whose bits are the sign bit s and the magnitude n < 2 ^ 63, and whether it is a NaN.

theorem Ratpoints.Double.orderValue_nextUp {x : Double} (hx : x.isNaN = false) (hi : x.bits ≠ huge.bits) : x.nextUp.orderValue = x.orderValue + 1 ∧ x.nextUp.isNaN = false

theorem Ratpoints.Double.nextUp_le_of_lt {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) (hi : x.bits ≠ huge.bits) (h : x.lt y = true) : x.nextUp.le y = true

theorem Ratpoints.Double.lt_nextUp {x : Double} (hx : x.isNaN = false) (hi : x.bits ≠ huge.bits) : x.lt x.nextUp = true

nextafter(x, HUGE_VAL) lies above x: with Ratpoints.Double.nextUp_le_of_lt, the least double above x, as the model describes Ratpoints.Double.nextUp.

theorem Ratpoints.Double.toNat_huge_neg : huge.neg.bits.toNat = 2 ^ 63 + maxOrderValue

theorem Ratpoints.Double.isZero_neg (x : Double) : x.neg.isZero = x.isZero

theorem Ratpoints.Double.nextDown_eq_neg_nextUp_neg (x : Double) : x.nextDown = x.neg.nextUp.neg

theorem Ratpoints.Double.orderValue_nextDown {x : Double} (hx : x.isNaN = false) (hi : x.bits ≠ huge.neg.bits) : x.nextDown.orderValue = x.orderValue - 1 ∧ x.nextDown.isNaN = false

theorem Ratpoints.Double.le_nextDown_of_lt {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) (hi : x.bits ≠ huge.neg.bits) (h : y.lt x = true) : y.le x.nextDown = true

theorem Ratpoints.Double.nextDown_lt {x : Double} (hx : x.isNaN = false) (hi : x.bits ≠ huge.neg.bits) : x.nextDown.lt x = true

nextafter(x, -HUGE_VAL) lies below x: with Ratpoints.Double.le_nextDown_of_lt, the greatest double below x, as the model describes Ratpoints.Double.nextDown.

The conversions

theorem Ratpoints.Double.toDyadic_bounds (x : Double) : x.toDyadic.1.natAbs < 2 ^ 53 ∧ -1074 ≤ x.toDyadic.2 ∧ x.toDyadic.2 ≤ 972

theorem Ratpoints.Double.toDyadic_fst_eq (x : Double) : x.toDyadic.1 = (if x.signBit = true then -1 else 1) * ↑x.toDyadic.1.natAbs

theorem Ratpoints.Double.isZero_eq_true_iff {x : Double} : x.isZero = true ↔ x.toRat = 0

theorem Ratpoints.Double.isZero_eq_false_iff {x : Double} : x.isZero = false ↔ x.toRat ≠ 0

theorem Ratpoints.Double.toNat_shift_eq_floor (m : ℕ) (e : ℤ) : (if 0 ≤ e then m <<< e.toNat else m >>> (-e).toNat) = ⌊↑m * 2 ^ e⌋₊

theorem Ratpoints.Double.toDyadic_fst_nonneg {x : Double} (h0 : 0 ≤ x.toRat) : 0 ≤ x.toDyadic.1

theorem Ratpoints.Double.shift_eq_floor_toRat {x : Double} (h0 : 0 ≤ x.toRat) {m e : ℤ} (hd : x.toDyadic = (m, e)) : (if 0 ≤ e then m.natAbs <<< e.toNat else m.natAbs >>> (-e).toNat) = ⌊x.toRat⌋₊

The truncation of the magnitude of Ratpoints.Double.toDyadic x = (m, e) that the conversions compute is the floor of a double x ≥ 0.

theorem Ratpoints.Double.toNat_toUInt64 {x : Double} (h0 : 0 ≤ x.toRat) (h1 : x.toRat < 2 ^ 64) : x.toUInt64.toNat = ⌊x.toRat⌋₊

theorem Ratpoints.Double.toInt_toInt64 {x : Double} (h0 : 0 ≤ x.toRat) (h1 : x.toRat < 2 ^ 63) : x.toInt64.toInt = ↑⌊x.toRat⌋₊

theorem Ratpoints.Double.isNaN_eq_false_of_isFinite {x : Double} (hx : x.isFinite = true) : x.isNaN = false

theorem Ratpoints.Double.isInf_eq_false_of_isFinite {x : Double} (hx : x.isFinite = true) : x.isInf = false

theorem Ratpoints.Double.abs_toRat (x : Double) : |x.toRat| = ↑x.toDyadic.1.natAbs * 2 ^ x.toDyadic.2

theorem Ratpoints.Double.lt_add_of_two_pow_le_mul {a : ℕ} {k L : ℤ} (ha : a < 2 ^ 53) (h : 2 ^ L ≤ ↑a * 2 ^ k) : L < 53 + k

theorem Ratpoints.Double.two_zpow_log2_le_mul {m : ℕ} (hm : m ≠ 0) (e : ℤ) : 2 ^ (↑m.log2 + e) ≤ ↑m * 2 ^ e ∧ ↑m * 2 ^ e < 2 ^ (↑m.log2 + 1 + e)

theorem Ratpoints.Double.log2_add_lt_of_mul_lt {a : ℕ} {k L : ℤ} (ha : a ≠ 0) (h : ↑a * 2 ^ k < 2 ^ L) : ↑a.log2 + k < L

theorem Ratpoints.Double.ldexp_eq {x : Double} (hx : x.isFinite = true) (hx0 : x.toRat ≠ 0) (n : ℤ) : x.ldexp n = ofDyadic x.signBit x.toDyadic.1.natAbs (x.toDyadic.2 + n)

theorem Ratpoints.Double.natAbs_toDyadic_fst_ne_zero {x : Double} (hx0 : x.toRat ≠ 0) : x.toDyadic.1.natAbs ≠ 0

theorem Ratpoints.Double.sign_mul_natAbs_mul_zpow (x : Double) (k : ℤ) : (if x.signBit = true then -1 else 1) * (↑x.toDyadic.1.natAbs * 2 ^ (x.toDyadic.2 + k)) = x.toRat * 2 ^ k

The value ±|m| 2 ^ (e + k) of a double with the sign of x and the magnitude of Ratpoints.Double.toDyadic x = (m, e) scaled by 2 ^ k is x 2 ^ k.

theorem Ratpoints.Double.ldexp_exact {x : Double} {n : ℤ} (hx : x.isFinite = true) (hx0 : x.toRat ≠ 0) (hlo : 2 ^ (-1022) ≤ |x.toRat| * 2 ^ n) (hhi : |x.toRat| * 2 ^ n < 2 ^ 1023) : (x.ldexp n).isFinite = true ∧ (x.ldexp n).signBit = x.signBit ∧ (x.ldexp n).toRat = x.toRat * 2 ^ n

theorem Ratpoints.Double.frexp_eq {x : Double} (hx : x.isFinite = true) (hx0 : x.toRat ≠ 0) : x.frexp = (ofDyadic x.signBit x.toDyadic.1.natAbs (-(↑x.toDyadic.1.natAbs.log2 + 1)), ↑x.toDyadic.1.natAbs.log2 + 1 + x.toDyadic.2)

theorem Ratpoints.Double.mul_zpow_neg_log2_mem_Ico {a : ℕ} (ha : a ≠ 0) : ↑a * 2 ^ (-(↑a.log2 + 1)) ∈ Set.Ico (1 / 2) 1

theorem Ratpoints.Double.abs_sign_mul (s : Bool) {v : ℚ} (h : 0 ≤ v) : |(if s = true then -1 else 1) * v| = v

theorem Ratpoints.Double.toRat_frexp_mul_zpow_eq_and_bounds {x : Double} (hx : x.isFinite = true) (hx0 : x.toRat ≠ 0) : x.frexp.1.isFinite = true ∧ x.frexp.1.signBit = x.signBit ∧ x.frexp.1.toRat * 2 ^ x.frexp.2 = x.toRat ∧ 1 / 2 ≤ |x.frexp.1.toRat| ∧ |x.frexp.1.toRat| < 1

frexp of a finite double x ≠ 0: a finite double f with the sign of x, f 2 ^ e = x and 1 / 2 ≤ |f| < 1.

theorem Ratpoints.Double.ofInt64_exact_of_lt {n : Int64} (hn : n.toInt.natAbs < 2 ^ 53) : (ofInt64 n).isFinite = true ∧ (ofInt64 n).toRat = ↑n.toInt

theorem Ratpoints.Double.ofInt64_exact {n : Int64} (hn : n.toInt.natAbs ≤ 2 ^ 53) : (ofInt64 n).isFinite = true ∧ (ofInt64 n).toRat = ↑n.toInt

(double)n is exact for |n| ≤ 2 ^ 53.

The ends of the search intervals

theorem Ratpoints.Double.le_eq_true_iff' {x y : Double} : x.le y = true ↔ ¬IsNaN x.bits ∧ ¬IsNaN y.bits ∧ doubleValue x.bits ≤ doubleValue y.bits

theorem Ratpoints.Double.lt_eq_true_iff' {x y : Double} : x.lt y = true ↔ ¬IsNaN x.bits ∧ ¬IsNaN y.bits ∧ doubleValue x.bits < doubleValue y.bits

theorem Ratpoints.Double.toDyadic_snd_nonneg {x : Double} (h : 2 ^ 52 ≤ |x.toRat|) : 0 ≤ x.toDyadic.2

A finite double of absolute value at least 2 ^ 52 is an integer: its exponent is not negative.

theorem Ratpoints.Double.toRat_eq_natCast_floor {x : Double} (h : 2 ^ 52 ≤ x.toRat) : x.toRat = ↑⌊x.toRat⌋₊

theorem Ratpoints.Double.toRat_nonneg {x : Double} (hs : x.signBit = false) : 0 ≤ x.toRat

theorem Ratpoints.Double.lt_zero_eq_true_iff {x : Double} (hx : x.isNaN = false) : x.lt zero = true ↔ x.orderValue < 0

theorem Ratpoints.Double.lt_twoPow63_eq_true_iff {x : Double} (hx : x.isNaN = false) : x.lt twoPow63 = true ↔ x.orderValue < 4890909195324358656

theorem Ratpoints.Double.le_doubleValue_or_of_lt_eq_false {x : Double} (hx : x.isNaN = false) (h : x.fabs.lt twoPow63 = false) : x.lt zero = false ∧ WithBotTop.coe (2 ^ 63) ≤ doubleValue x.bits ∨ x.lt zero = true ∧ doubleValue x.bits ≤ WithBotTop.coe (-2 ^ 63)

A double whose absolute value is not below 2 ^ 63 (|x| < 2 ^ 63 false in the C code) has a value of at least 2 ^ 63 or at most -2 ^ 63, by its sign.

theorem Ratpoints.Double.isFinite_and_abs_lt_of_lt {x : Double} (h : x.fabs.lt twoPow63 = true) : x.isFinite = true ∧ |x.toRat| < 2 ^ 63

theorem Ratpoints.Double.lt_twoPow63_eq_true_iff_toRat {x : Double} (hf : x.isFinite = true) : x.lt twoPow63 = true ↔ x.toRat < 2 ^ 63

theorem Ratpoints.Double.lt_zero_eq_true_iff_toRat {x : Double} (hf : x.isFinite = true) : x.lt zero = true ↔ x.toRat < 0

theorem Ratpoints.Double.le_toRat_of_not_toInt64_lt {x : Double} (h0 : 0 ≤ x.toRat) (h63 : x.toRat < 2 ^ 63) {H : ℕ} (hH63 : H < 2 ^ 63) (h : ¬x.toInt64 < H.toInt64) : ↑H ≤ x.toRat

A double 0 ≤ x < 2 ^ 63 whose conversion to a long is not below H is at least H.