The search region

The search region of ratpoints: search intervals [l, u] for x / z, whose ends are IEEE binary64 doubles, given here by their bits, and a range of the denominators z. A double has a value in ℚ extended by ⊥ and ⊤ (WithBotTop ℚ), the two infinities; a NaN has none (its value here is junk), and both zeros have the value 0; ratpoints refuses search intervals with a NaN end, with l > u or that are not increasing and strictly apart. A point lies in the region when it is at infinity, or its denominator is in the range and x / z lies in one of the intervals (in any, when there are none). The specification uses Mathlib and nothing of the model; the comparator challenge restates its definitions verbatim.

Main definitions

• Ratpoints.IsNaN, Ratpoints.doubleValue: whether the bits of a double are a NaN, and the value of a double.
• Ratpoints.AreSearchIntervals, Ratpoints.IntervalsWF: closed intervals, increasing and strictly apart, over values and over the bits of doubles.
• Ratpoints.InIntervals: a rational number lies in one of a list of intervals.
• Ratpoints.InRegion: a point lies in the search region.
• Ratpoints.IsFullBox: the search region is the whole box of height H, so that ratpoints may reverse the polynomial.
• Ratpoints.denominatorBound: the largest denominator of the search.

Implementation notes

The file imports Mathlib.Order.WithBotTop for the extended values and Mathlib.Algebra.Order.Field.Rat for the order and the field operations of ℚ, both publicly: the comparator challenge imports the Mathlib modules among the public imports of the files of the specification that it restates, so that the definitions it restates elaborate to the same terms as here.

def Ratpoints.IsNaN (x : UInt64) : Prop

Whether the IEEE binary64 bits x are a NaN: the exponent field all ones and the fraction nonzero.

Equations

• Ratpoints.IsNaN x = (x.toNat / 2 ^ 52 % 2 ^ 11 = 2047 ∧ x.toNat % 2 ^ 52 ≠ 0)

@[instance_reducible]

instance Ratpoints.instDecidableIsNaN (x : UInt64) : Decidable (IsNaN x)

Equations

• Ratpoints.instDecidableIsNaN x = { decide := decide (x.toNat / 2 ^ 52 % 2 ^ 11 = 2047) && decide (x.toNat % 2 ^ 52 ≠ 0), reflects_decide := ⋯ }

def Ratpoints.doubleValue (x : UInt64) : WithBotTop ℚ

The value of the IEEE binary64 double with the bits x: ±f 2 ^ (-1074) for the exponent field 0 (the zeros and the subnormals, both zeros giving 0), ±(2 ^ 52 + f) 2 ^ (e - 1075) for an exponent field e from 1 to 2046, and ⊥ and ⊤ for the infinities, where f is the fraction and the sign is that of the top bit. The value of a NaN (the exponent field 2047 with a nonzero fraction) is junk, an infinity: Ratpoints.IntervalsWF excludes NaNs.

Equations

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

def Ratpoints.AreSearchIntervals (dom : List (WithBotTop ℚ × WithBotTop ℚ)) : Prop

Closed intervals [l, u] with l ≤ u, increasing and strictly apart: the upper end of each below the lower end of the next.

Equations

• Ratpoints.AreSearchIntervals dom = ((∀ i ∈ dom, i.1 ≤ i.2) ∧ List.IsChain (fun (i j : WithBotTop ℚ × WithBotTop ℚ) => i.2 < j.1) dom)

@[instance_reducible]

instance Ratpoints.instDecidableAreSearchIntervals (dom : List (WithBotTop ℚ × WithBotTop ℚ)) : Decidable (AreSearchIntervals dom)

Equations

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

def Ratpoints.IntervalsWF (dom : List (UInt64 × UInt64)) : Prop

The search intervals with the ends of the bits of doubles that ratpoints accepts, the test of RATPOINTS_BAD_ARGS: no end is a NaN, and the values are closed intervals, increasing and strictly apart (Ratpoints.AreSearchIntervals); -0 and 0 have the same value.

Equations

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

@[instance_reducible]

instance Ratpoints.instDecidableIntervalsWF (dom : List (UInt64 × UInt64)) : Decidable (IntervalsWF dom)

Equations

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

def Ratpoints.InIntervals (D : List (WithBotTop ℚ × WithBotTop ℚ)) (x : ℚ) : Prop

The rational number x lies in one of the intervals D, over the values of their ends, both ends included.

Equations

• Ratpoints.InIntervals D x = ∃ i ∈ D, i.1 ≤ WithBotTop.coe x ∧ WithBotTop.coe x ≤ i.2

@[instance_reducible]

instance Ratpoints.instDecidablePredInIntervals (D : List (WithBotTop ℚ × WithBotTop ℚ)) : DecidablePred (InIntervals D)

Equations

• Ratpoints.instDecidablePredInIntervals D x✝ = Ratpoints.instDecidablePredInIntervals._aux_1 D x✝

def Ratpoints.InRegion (dom : List (WithBotTop ℚ × WithBotTop ℚ)) (bLow bHigh : ℤ) (p : ℤ × ℤ × ℤ) : Prop

The triple p = (x, y, z) lies in the search region of the intervals dom (over the values of their ends) and the range of the denominators from bLow to bHigh: z = 0 (a point at infinity), or bLow ≤ z, z ≤ bHigh unless bHigh < 1 (no bound beyond the height bound), and x / z in one of the intervals (Ratpoints.InIntervals), or anywhere when there are none.

Equations

• Ratpoints.InRegion dom bLow bHigh p = (p.2.2 = 0 ∨ bLow ≤ p.2.2 ∧ (bHigh < 1 ∨ p.2.2 ≤ bHigh) ∧ (dom = [] ∨ Ratpoints.InIntervals dom (↑p.1 / ↑p.2.2)))

@[instance_reducible]

instance Ratpoints.instDecidablePredInRegion (dom : List (WithBotTop ℚ × WithBotTop ℚ)) (bLow bHigh : ℤ) : DecidablePred (InRegion dom bLow bHigh)

Equations

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

def Ratpoints.IsFullBox {α : Type u_1} (dom : List α) (bLow bHigh : ℤ) (H : ℕ) : Prop

The search region of the intervals dom and the range of the denominators from bLow to bHigh is the whole box of the height bound H: no intervals, bLow ≤ 1 and no bound below H on the denominators (bHigh < 1 or H ≤ bHigh). Only then may ratpoints reverse the polynomial (otherwise it sets RATPOINTS_NO_REVERSE_AUTO).

Equations

• Ratpoints.IsFullBox dom bLow bHigh H = (dom = [] ∧ bLow ≤ 1 ∧ (bHigh < 1 ∨ ↑H ≤ bHigh))

@[instance_reducible]

instance Ratpoints.instDecidableIsFullBox {α : Type u_1} (dom : List α) (bLow bHigh : ℤ) (H : ℕ) : Decidable (IsFullBox dom bLow bHigh H)

Equations

• Ratpoints.instDecidableIsFullBox dom bLow bHigh H = { decide := decide (dom = []) && decide (bLow ≤ 1 ∧ (bHigh < 1 ∨ ↑H ≤ bHigh)), reflects_decide := ⋯ }

def Ratpoints.denominatorBound (bHigh : ℤ) (H : ℕ) : ℕ

The largest denominator of the search for the bound bHigh and the height bound H: bHigh when 1 ≤ bHigh ≤ H, and H otherwise.

Equations

• Ratpoints.denominatorBound bHigh H = if 1 ≤ bHigh ∧ bHigh ≤ ↑H then bHigh.toNat else H

Examples, checked by decide