The numbers and the search intervals of the program

The ends of the search intervals of the command line of ratpoints-lean, as Ratpoints.Model.CliNumbers reads, compares and joins them. strtod never reads a NaN (Ratpoints.Cli.isNaN_strtod); outward moves a double to the side of the end that its direction asks, and onto the largest double at most a lower end when it starts close enough to it (Ratpoints.Cli.outward_spec); so an end that scan_end reads has a double that is not a NaN, outward of the end (Ratpoints.Cli.inf_mem_and_isNaN_eq_false_and_le_of_run_scanEnd_eq_some). For a word of fewer than 2 ^ 56 characters, the double of a lower end is the largest double at most the end (Ratpoints.Cli.run_scanEnd_isMaxBelow): the parts of the word give its exact value (Ratpoints.Cli.floatParts_bounds_and_isDigit_exponentDigits, Ratpoints.Cli.wordValue), which lies below the successor of the double that strtod reads (Ratpoints.Cli.lt_nextUp_strtod), and the exponent that scan_end accumulates, which stops at LONG_MAX / 20, is the exact one for the doubles that are finite and not zero (Ratpoints.Cli.scanEndValue_eq_wordValue). The ends of a missing -l and -u lie beyond the height bound (Ratpoints.Cli.isFinite_heightEnd_and_le_toRat). The comparisons cmp_end and cmp_end_x compare the values (Ratpoints.Cli.cmpEnd_neg_iff, Ratpoints.Cli.cmpEndX_neg_iff), so that the binary search of in_region over increasing and disjoint intervals decides the membership of x / z (Ratpoints.Cli.inRegion_spec); and join_intervals keeps what the intervals hold and, for intervals that join well, gives intervals that the library accepts (Ratpoints.Cli.joinIntervals_spec).

Main definitions

• Ratpoints.Cli.ExactEnd.value, Ratpoints.Cli.InExactRegion: the value of an exact end, and the exact search region of the command line.
• Ratpoints.Cli.scanEndValue, Ratpoints.Cli.wordValue: the end that scan_end takes, and the exact value of a floating constant.
• Ratpoints.Cli.ChainEnds: the ends of increasing and disjoint intervals l ≤ u.
• Ratpoints.Cli.InPair, Ratpoints.Cli.NoNaN, Ratpoints.Cli.JoinsWell: intervals of doubles.

Main statements

• Ratpoints.Cli.outward_spec, Ratpoints.Cli.inf_mem_and_isNaN_eq_false_and_le_of_run_scanEnd_eq_some, Ratpoints.Cli.run_scanEnd_isMaxBelow, Ratpoints.Cli.isFinite_heightEnd_and_le_toRat: the doubles of the ends.
• Ratpoints.Cli.lt_nextUp_strtod: the exact value below the successor of the double of strtod.
• Ratpoints.Cli.inRegion_spec: the binary search.
• Ratpoints.Cli.joinIntervals_spec: the intervals that the library is given.

Implementation notes

The contracts of the loops are proved with vcgen, as those of the model's other loops.

def Ratpoints.Cli.ExactEnd.value (e : ExactEnd) : WithBotTop ℚ

The value of an exact end of a search interval of the command line (Ratpoints.Cli.ExactEnd): ⊥ and ⊤ for the infinite ends, and its rational number otherwise.

Equations

• e.value = if e.inf < 0 then ⊥ else if 0 < e.inf then ⊤ else WithBotTop.coe e.q

theorem Ratpoints.Cli.cmpEnd_neg_iff {e f : ExactEnd} (he : e.inf = -1 ∨ e.inf = 0 ∨ e.inf = 1) (hf : f.inf = -1 ∨ f.inf = 0 ∨ f.inf = 1) : cmpEnd e f < 0 ↔ e.value < f.value

theorem Ratpoints.Cli.cmpEnd_pos_iff {e f : ExactEnd} (he : e.inf = -1 ∨ e.inf = 0 ∨ e.inf = 1) (hf : f.inf = -1 ∨ f.inf = 0 ∨ f.inf = 1) : 0 < cmpEnd e f ↔ f.value < e.value

theorem Ratpoints.Cli.isNaN_nearestBinary (neg : Bool) (m : ℕ) (t : ℤ) : (nearestBinary neg m t).isNaN = false

theorem Ratpoints.Cli.isNaN_nearestDecimal (neg : Bool) (m : ℕ) (t : ℤ) : (nearestDecimal neg m t).isNaN = false

theorem Ratpoints.Cli.isNaN_strtod (w : List Char) : (strtod w).isNaN = false

def Ratpoints.Cli.OutwardInvariant (x0 : Double) (v : ℚ) (dir : ℤ) : Std.WP.WhileInvariant Double Prop

The invariant of the loop of Ratpoints.Cli.outward from the double x0 towards v, dir < 0 for a lower end, on the double x: it is not a NaN, an infinite x is that of the direction, at the exit a finite x is on the side of v that the direction asks, and for a lower end, when v lies below the successor of x0, every double at most v is at most x.

Equations

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

theorem Ratpoints.Cli.outwardInvariant_start {x : Double} (v : ℚ) (dir : ℤ) (hf : x.isFinite = true) : OutwardInvariant x v dir false x

theorem Ratpoints.Cli.OutwardInvariant.exit_of_cond {x0 x : Double} {v : ℚ} {dir : ℤ} {k : ℕ} (hc : if dir < 0 then x.toRat ≤ v else v ≤ x.toRat) (h : (if dir < 0 then (x.orderValue + ↑Double.maxOrderValue).toNat else (↑Double.maxOrderValue - x.orderValue).toNat) = k ∧ OutwardInvariant x0 v dir false x) : OutwardInvariant x0 v dir true x

theorem Ratpoints.Cli.OutwardInvariant.exit_of_not_isFinite {x0 x : Double} {v : ℚ} {dir : ℤ} {k : ℕ} (hf : ¬x.isFinite = true) (h : (if dir < 0 then (x.orderValue + ↑Double.maxOrderValue).toNat else (↑Double.maxOrderValue - x.orderValue).toNat) = k ∧ OutwardInvariant x0 v dir false x) : OutwardInvariant x0 v dir true x

theorem Ratpoints.Cli.OutwardInvariant.step {x0 x : Double} {v : ℚ} {dir : ℤ} {k : ℕ} (hf : x.isFinite = true) (hc : ¬if dir < 0 then x.toRat ≤ v else v ≤ x.toRat) (h : (if dir < 0 then (x.orderValue + ↑Double.maxOrderValue).toNat else (↑Double.maxOrderValue - x.orderValue).toNat) = k ∧ OutwardInvariant x0 v dir false x) : (if dir < 0 then ((if dir < 0 then x.nextDown else x.nextUp).orderValue + ↑Double.maxOrderValue).toNat else (↑Double.maxOrderValue - (if dir < 0 then x.nextDown else x.nextUp).orderValue).toNat) < k ∧ OutwardInvariant x0 v dir false (if dir < 0 then x.nextDown else x.nextUp)

theorem Ratpoints.Cli.OutwardInvariant.post {x0 x : Double} {v : ℚ} {dir : ℤ} (h : OutwardInvariant x0 v dir true x) : x.isNaN = false ∧ (dir < 0 → doubleValue x.bits ≤ WithBotTop.coe v) ∧ (¬dir < 0 → WithBotTop.coe v ≤ doubleValue x.bits) ∧ (dir < 0 → WithBotTop.coe v < doubleValue x0.nextUp.bits → ∀ (y : Double), y.isNaN = false → doubleValue y.bits ≤ WithBotTop.coe v → doubleValue y.bits ≤ doubleValue x.bits)

theorem Ratpoints.Cli.outward_spec (x : Double) (v : ℚ) (dir : ℤ) : ⦃ x.isFinite = true ⦄ outward x v dir ⦃ fun (r : Double) => r.isNaN = false ∧ (dir < 0 → doubleValue r.bits ≤ WithBotTop.coe v) ∧ (¬dir < 0 → WithBotTop.coe v ≤ doubleValue r.bits) ∧ (dir < 0 → WithBotTop.coe v < doubleValue x.nextUp.bits → ∀ (y : Double), y.isNaN = false → doubleValue y.bits ≤ WithBotTop.coe v → doubleValue y.bits ≤ doubleValue r.bits) ⦄

outward moves the double x to the side of v that the direction asks, below v for a lower end (dir < 0) and above it otherwise, and for a lower end it lands on the largest double at most v when it starts from a double whose successor lies above v.

theorem Ratpoints.Cli.run_outward {x : Double} (v : ℚ) (dir : ℤ) (hf : x.isFinite = true) : (outward x v dir).run.isNaN = false ∧ (dir < 0 → doubleValue (outward x v dir).run.bits ≤ WithBotTop.coe v) ∧ (¬dir < 0 → WithBotTop.coe v ≤ doubleValue (outward x v dir).run.bits) ∧ (dir < 0 → WithBotTop.coe v < doubleValue x.nextUp.bits → ∀ (y : Double), y.isNaN = false → doubleValue y.bits ≤ WithBotTop.coe v → doubleValue y.bits ≤ doubleValue (outward x v dir).run.bits)

def Ratpoints.Cli.scanEndValue (w : List Char) (x : Double) : ℚ

The number q that Ratpoints.Cli.scanEnd takes as the end that the word w denotes, x being the double that strtod reads from it, copied from Ratpoints.Cli.scanEnd (Ratpoints.Cli.eq_of_run_scanEnd_eq_some).

Equations

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

theorem Ratpoints.Cli.eq_some_of_scanDouble?_eq_some {s : String} {x : Double} (h : scanDouble? s = some x) : ∃ (w : List Char), onlyWord? s = some w ∧ isDoubleWord w = true ∧ x = strtod w

theorem Ratpoints.Cli.eq_of_run_scanEnd_eq_some {s : String} {dir : ℤ} {e : ExactEnd} {d : Double} (h : (scanEnd s dir).run = some (e, d)) : ∃ (w : List Char), onlyWord? s = some w ∧ isDoubleWord w = true ∧ ((strtod w).isInf = true ∧ e = { inf := if Double.zero.lt (strtod w) = true then 1 else -1 } ∧ d = strtod w ∨ (strtod w).isInf = false ∧ e = { q := scanEndValue w (strtod w) } ∧ d = (outward (strtod w) (scanEndValue w (strtod w)) dir).run)

theorem Ratpoints.Cli.value_inf_eq_doubleValue {x : Double} (hi : x.isInf = true) : { inf := if Double.zero.lt x = true then 1 else -1 }.value = doubleValue x.bits

theorem Ratpoints.Cli.inf_mem_and_isNaN_eq_false_and_le_of_run_scanEnd_eq_some {s : String} {dir : ℤ} {e : ExactEnd} {d : Double} (h : (scanEnd s dir).run = some (e, d)) : (e.inf = -1 ∨ e.inf = 0 ∨ e.inf = 1) ∧ d.isNaN = false ∧ (dir < 0 → doubleValue d.bits ≤ e.value) ∧ (¬dir < 0 → e.value ≤ doubleValue d.bits)

An end that scan_end reads: its inf is -1, 0 or 1, its double is not a NaN, and it is outward of the end, below a lower end and above an upper one.

theorem Ratpoints.Cli.isFinite_heightEnd_and_le_toRat {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) : (heightEnd H).isFinite = true ∧ ↑H ≤ (heightEnd H).toRat

The end of a missing first -l (negated) and of a missing last -u for a height bound 1 ≤ H < 2 ^ 63 is a finite double of a value at least H.

The largest double below a lower end

theorem Ratpoints.Cli.mantissaDigits_bounds_and_eq_dropWhile (isDigit : Char → Bool) (point : Bool) (s : List Char) : (mantissaDigits isDigit point s).2.1 ≤ (mantissaDigits isDigit point s).1.length ∧ (mantissaDigits isDigit point s).1.length ≤ s.length ∧ (∀ ch ∈ (mantissaDigits isDigit point s).1, isDigit ch = true) ∧ (mantissaDigits isDigit point s).2.2 = List.dropWhile (fun (ch : Char) => isDigit ch || ch == '.') s

The digits that Ratpoints.Cli.mantissaDigits takes from s: as many after the point at most as in all, no more than the characters of s, all digits, and the rest of s without the digits and the points.

theorem Ratpoints.Cli.length_dropSign_le (w : List Char) : (dropSign w).length ≤ w.length

theorem Ratpoints.Cli.exponentDigits_snd_isDigit {isD : Char → Bool} {exp s : List Char} (hexp : ∀ x ∈ exp, "eEpP".contains x = true) (h : isFloatBody isD exp s = true) (ch : Char) : ch ∈ (exponentDigits (List.dropWhile (fun (ch : Char) => isD ch || ch == '.') s)).2 → ch.isDigit = true

theorem Ratpoints.Cli.digitValue_of_isDigit {ch : Char} (h : ch.isDigit = true) : digitValue ch = ch.toNat - '0'.toNat

theorem Ratpoints.Cli.digitValue_lt_ten {ch : Char} (h : ch.isDigit = true) : digitValue ch < 10

theorem Ratpoints.Cli.digitValue_lt_sixteen {ch : Char} (h : ch.isHexDigit = true) : digitValue ch < 16

theorem Ratpoints.Cli.foldl_digits_lt {b : ℕ} {ds : List Char} (h : ∀ ch ∈ ds, digitValue ch < b) (n : ℕ) : List.foldl (fun (n : ℕ) (ch : Char) => b * n + digitValue ch) n ds < (n + 1) * b ^ ds.length

theorem Ratpoints.Cli.natOfDigitsIn_lt {b : ℕ} {ds : List Char} (h : ∀ ch ∈ ds, digitValue ch < b) : natOfDigitsIn b ds < b ^ ds.length

theorem Ratpoints.Cli.le_foldl_digits (b : ℕ) (hb : 1 ≤ b) (ds : List Char) (n : ℕ) : n ≤ List.foldl (fun (n : ℕ) (ch : Char) => b * n + digitValue ch) n ds

theorem Ratpoints.Cli.foldl_capped_eq {L : ℤ} {ds : List Char} (h : ∀ ch ∈ ds, ch.isDigit = true) (n : ℕ) (hlt : ↑(List.foldl (fun (n : ℕ) (ch : Char) => 10 * n + digitValue ch) n ds) < L) : List.foldl (fun (ex : ℤ) (ch : Char) => if ex < L then 10 * ex + (↑ch.toNat - ↑'0'.toNat) else ex) (↑n) ds = ↑(List.foldl (fun (n : ℕ) (ch : Char) => 10 * n + digitValue ch) n ds)

The exponent that scan_end accumulates, which stops taking digits once it reaches L, is the exponent of the digits when that lies below L.

theorem Ratpoints.Cli.nearestBinary_eq {neg : Bool} {m : ℕ} {t : ℤ} (hf : (nearestBinary neg m t).isFinite = true) (hz : (nearestBinary neg m t).beq Double.zero = false) : m ≠ 0 ∧ ↑m.log2 + t < 1024 ∧ -1075 < ↑m.log2 + 1 + t ∧ nearestBinary neg m t = Double.ofDyadic neg m t

theorem Ratpoints.Cli.nearestDecimal_eq {neg : Bool} {m : ℕ} {t : ℤ} (hf : (nearestDecimal neg m t).isFinite = true) (hz : (nearestDecimal neg m t).beq Double.zero = false) : m ≠ 0 ∧ (0 ≤ t → ↑m.log2 + 3 * t < 1024 ∧ nearestDecimal neg m t = Double.ofRatio neg (m * 10 ^ t.toNat) 1) ∧ (t < 0 → 3 * -t < ↑m.log2 + 1076 ∧ nearestDecimal neg m t = Double.ofRatio neg m (10 ^ (-t).toNat))

theorem Ratpoints.Cli.lt_nextUp_nearestBinary {neg : Bool} {m : ℕ} {t : ℤ} (hf : (nearestBinary neg m t).isFinite = true) (hz : (nearestBinary neg m t).beq Double.zero = false) : WithBotTop.coe (if neg = true then -(↑m * 2 ^ t) else ↑m * 2 ^ t) < doubleValue (nearestBinary neg m t).nextUp.bits

theorem Ratpoints.Cli.lt_nextUp_nearestDecimal {neg : Bool} {m : ℕ} {t : ℤ} (hf : (nearestDecimal neg m t).isFinite = true) (hz : (nearestDecimal neg m t).beq Double.zero = false) : WithBotTop.coe (if neg = true then -(↑m * 10 ^ t) else ↑m * 10 ^ t) < doubleValue (nearestDecimal neg m t).nextUp.bits

def Ratpoints.Cli.wordValue (w : List Char) : ℚ

The exact value of the floating constant w that is not an infinity, from the parts of its word (Ratpoints.Cli.floatParts): ±m 2 ^ (ex - 4 k) for a hexadecimal constant and ±m 10 ^ (ex - k) for a decimal one, for the digits m of its mantissa, the number k of them after the point and its exponent ex, as strtod takes it.

Equations

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

theorem Ratpoints.Cli.strtod_eq {w : List Char} (hi : isInfWord (dropSign w) = false) : strtod w = if (floatParts w).2.1 = true then nearestBinary (floatParts w).1 (natOfDigitsIn 16 (floatParts w).2.2.1) ((if (exponentDigits (floatParts w).2.2.2.2).1 = true then -↑(natOfDigitsIn 10 (exponentDigits (floatParts w).2.2.2.2).2) else ↑(natOfDigitsIn 10 (exponentDigits (floatParts w).2.2.2.2).2)) - 4 * ↑(floatParts w).2.2.2.1) else nearestDecimal (floatParts w).1 (natOfDigitsIn 10 (floatParts w).2.2.1) ((if (exponentDigits (floatParts w).2.2.2.2).1 = true then -↑(natOfDigitsIn 10 (exponentDigits (floatParts w).2.2.2.2).2) else ↑(natOfDigitsIn 10 (exponentDigits (floatParts w).2.2.2.2).2)) - ↑(floatParts w).2.2.2.1)

theorem Ratpoints.Cli.lt_nextUp_strtod {w : List Char} (hi : isInfWord (dropSign w) = false) (hf : (strtod w).isFinite = true) (hz : (strtod w).beq Double.zero = false) : WithBotTop.coe (wordValue w) < doubleValue (strtod w).nextUp.bits

The exact value of a floating constant lies below the successor of the finite double other than a zero that strtod reads from it: the upper half of the faithful rounding of Ratpoints.Double.ofRatio and Ratpoints.Double.ofDyadic (Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofRatio, Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofDyadic).

theorem Ratpoints.Cli.floatParts_bounds_and_isDigit_exponentDigits (w : List Char) : (floatParts w).2.2.2.1 ≤ (floatParts w).2.2.1.length ∧ (floatParts w).2.2.1.length ≤ w.length ∧ (∀ ch ∈ (floatParts w).2.2.1, digitValue ch < if (floatParts w).2.1 = true then 16 else 10) ∧ (isDoubleWord w = true → isInfWord (dropSign w) = false → ∀ ch ∈ (exponentDigits (floatParts w).2.2.2.2).2, ch.isDigit = true)

The parts of the word w (Ratpoints.Cli.floatParts): as many digits after the point at most as in all, no more than the characters of w, all digits of the base, and the decimal digits of the exponent when w is a floating constant that is not an infinity.

theorem Ratpoints.Cli.ite_natCast_mul_pow_eq (m b : ℕ) (t : ℤ) : (if 0 ≤ t then ↑(m * b ^ t.natAbs) else mkRat (↑m) (b ^ t.natAbs)) = ↑m * ↑b ^ t

theorem Ratpoints.Cli.log2_natOfDigitsIn_lt {w : List Char} : (natOfDigitsIn (if (floatParts w).2.1 = true then 16 else 10) (floatParts w).2.2.1).log2 < 4 * (floatParts w).2.2.1.length + 1

theorem Ratpoints.Cli.scanEndValue_eq_wordValue {w : List Char} (hd : isDoubleWord w = true) (hi : isInfWord (dropSign w) = false) (hf : (strtod w).isFinite = true) (hz : (strtod w).beq Double.zero = false) (hlen : w.length < 2 ^ 56) : scanEndValue w (strtod w) = wordValue w

For a floating constant of fewer than 2 ^ 56 characters whose double is finite and not a zero, the end that scan_end takes is its exact value.

theorem Ratpoints.Cli.lt_nextUp_of_beq_zero (w : List Char) {x : Double} (hz : x.beq Double.zero = true) : WithBotTop.coe (scanEndValue w x) < doubleValue x.nextUp.bits

When strtod reads a zero, the end that scan_end takes is 0 or ±2 ^ (-1075), below the least positive double, the successor of the zero.

theorem Ratpoints.Cli.lt_nextUp_scanEndValue {w : List Char} (hd : isDoubleWord w = true) (hi : isInfWord (dropSign w) = false) (hf : (strtod w).isFinite = true) (hlen : w.length < 2 ^ 56) : WithBotTop.coe (scanEndValue w (strtod w)) < doubleValue (strtod w).nextUp.bits

theorem Ratpoints.Cli.isInfWord_eq_false_of_isInf {w : List Char} (hi : (strtod w).isInf = false) : isInfWord (dropSign w) = false

theorem Ratpoints.Cli.length_le_of_onlyWord?_eq_some {s : String} {w : List Char} (h : onlyWord? s = some w) : w.length ≤ s.length

theorem Ratpoints.Cli.run_scanEnd_isMaxBelow {s : String} {e : ExactEnd} {d : Double} (h : (scanEnd s (-1)).run = some (e, d)) (hlen : s.length < 2 ^ 56) (y : Double) (hy : y.isNaN = false) (hye : doubleValue y.bits ≤ e.value) : doubleValue y.bits ≤ doubleValue d.bits

The double that scan_end gives for a lower end of fewer than 2 ^ 56 characters is the largest double at most the end: every double at most the end is at most it.

The search region of the command line

def Ratpoints.Cli.InExactRegion (ends : Array ExactEnd) (n : ℕ) (x : ℚ) : Prop

The rational number x lies in one of the n search intervals of the command line with the exact ends ends: ends[2 j] ≤ x ≤ ends[2 j + 1] for some j < n.

Equations

• Ratpoints.Cli.InExactRegion ends n x = ∃ j < n, ends[2 * j]!.value ≤ WithBotTop.coe x ∧ WithBotTop.coe x ≤ ends[2 * j + 1]!.value

theorem Ratpoints.Cli.cmpEndX_neg_iff (e : ExactEnd) (a b : ℤ) : cmpEndX e a b < 0 ↔ e.value < WithBotTop.coe (↑a / ↑b)

theorem Ratpoints.Cli.cmpEndX_nonpos_iff (e : ExactEnd) (a b : ℤ) : cmpEndX e a b ≤ 0 ↔ e.value ≤ WithBotTop.coe (↑a / ↑b)

def Ratpoints.Cli.ChainEnds (v : ℕ → WithBotTop ℚ) (m : ℕ) : Prop

The values v 0, v 1, …, v (m - 1) of the ends of intervals, in turn a lower and an upper end, increase, the upper end of each strictly below the lower end of the next, as the checks of error 7 make those of the command line.

Equations

• Ratpoints.Cli.ChainEnds v m = ∀ (i : ℕ), i + 1 < m → v i ≤ v (i + 1) ∧ (i % 2 = 1 → v i < v (i + 1))

theorem Ratpoints.Cli.ChainEnds.le {v : ℕ → WithBotTop ℚ} {m : ℕ} (h : ChainEnds v m) {i k : ℕ} (hik : i ≤ k) (hk : k < m) : v i ≤ v k

theorem Ratpoints.Cli.ChainEnds.lt {v : ℕ → WithBotTop ℚ} {m : ℕ} (h : ChainEnds v m) {i k : ℕ} (hi : i % 2 = 1) (hik : i < k) (hk : k < m) : v i < v k

def Ratpoints.Cli.InRegionInvariant (v : ℕ → WithBotTop ℚ) (x : WithBotTop ℚ) (n : ℕ) : Std.WP.WhileInvariant (ℕ × ℕ) Prop

The invariant of the binary search of Ratpoints.Cli.inRegion for x among the n intervals with the ends of the values v, on its state (lo, hi): the upper ends before lo lie below x, those from hi on not, and lo = hi at the exit.

Equations

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

theorem Ratpoints.Cli.inRegionInvariant_zero (v : ℕ → WithBotTop ℚ) (x : WithBotTop ℚ) (n : ℕ) : InRegionInvariant v x n false (0, n)

theorem Ratpoints.Cli.InRegionInvariant.exit {v : ℕ → WithBotTop ℚ} {x : WithBotTop ℚ} {n lo hi : ℕ} (hlt : ¬lo < hi) (h : InRegionInvariant v x n false (lo, hi)) : InRegionInvariant v x n true (lo, hi)

theorem Ratpoints.Cli.InRegionInvariant.step_lt {e : Array ExactEnd} {a b : ℤ} {n lo hi k : ℕ} (hc : ChainEnds (fun (j : ℕ) => e[j]!.value) (2 * n)) (hlt : lo < hi) (hx : cmpEndX e[2 * (lo + (hi - lo) / 2) + 1]! a b < 0) (h : hi - lo = k ∧ InRegionInvariant (fun (j : ℕ) => e[j]!.value) (WithBotTop.coe (↑a / ↑b)) n false (lo, hi)) : hi - (lo + (hi - lo) / 2 + 1) < k ∧ InRegionInvariant (fun (j : ℕ) => e[j]!.value) (WithBotTop.coe (↑a / ↑b)) n false (lo + (hi - lo) / 2 + 1, hi)

theorem Ratpoints.Cli.InRegionInvariant.step_ge {e : Array ExactEnd} {a b : ℤ} {n lo hi k : ℕ} (hc : ChainEnds (fun (j : ℕ) => e[j]!.value) (2 * n)) (hlt : lo < hi) (hx : ¬cmpEndX e[2 * (lo + (hi - lo) / 2) + 1]! a b < 0) (h : hi - lo = k ∧ InRegionInvariant (fun (j : ℕ) => e[j]!.value) (WithBotTop.coe (↑a / ↑b)) n false (lo, hi)) : lo + (hi - lo) / 2 - lo < k ∧ InRegionInvariant (fun (j : ℕ) => e[j]!.value) (WithBotTop.coe (↑a / ↑b)) n false (lo, lo + (hi - lo) / 2)

theorem Ratpoints.Cli.InRegionInvariant.post {e : Array ExactEnd} {a b : ℤ} {n lo hi : ℕ} (hc : ChainEnds (fun (j : ℕ) => e[j]!.value) (2 * n)) (h : InRegionInvariant (fun (j : ℕ) => e[j]!.value) (WithBotTop.coe (↑a / ↑b)) n true (lo, hi)) : (decide (lo < n) && decide (cmpEndX e[2 * lo]! a b ≤ 0)) = true ↔ InExactRegion e n (↑a / ↑b)

theorem Ratpoints.Cli.inRegion_spec (a b : ℤ) (e : Array ExactEnd) (n : ℕ) : ⦃ ChainEnds (fun (j : ℕ) => e[j]!.value) (2 * n) ⦄ inRegion a b e n ⦃ fun (r : Bool) => r = true ↔ InExactRegion e n (↑a / ↑b) ⦄

The binary search of in_region over increasing and disjoint intervals decides whether a / b lies in one of them.

theorem Ratpoints.Cli.run_inRegion (a b : ℤ) {e : Array ExactEnd} {n : ℕ} (hc : ChainEnds (fun (j : ℕ) => e[j]!.value) (2 * n)) : (inRegion a b e n).run = true ↔ InExactRegion e n (↑a / ↑b)

Joining the intervals

def Ratpoints.Cli.InPair (p : Double × Double) (x : ℚ) : Prop

x lies in the interval p, over the values of its ends.

Equations

• Ratpoints.Cli.InPair p x = (Ratpoints.doubleValue p.1.bits ≤ WithBotTop.coe x ∧ WithBotTop.coe x ≤ Ratpoints.doubleValue p.2.bits)

def Ratpoints.Cli.NoNaN (dom : List (Double × Double)) : Prop

No end of the intervals dom is a NaN.

Equations

• Ratpoints.Cli.NoNaN dom = ∀ p ∈ dom, p.1.isNaN = false ∧ p.2.isNaN = false

def Ratpoints.Cli.JoinsWell (dom : List (Double × Double)) : Prop

The intervals dom have l ≤ u, and their lower ends increase from the second one on, as those of the command line do.

Equations

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

structure Ratpoints.Cli.JoinInvariant (dom : List (Double × Double)) (k : ℕ) (iv : Array (Double × Double)) (n : ℕ) : Prop

The invariant of the loop of Ratpoints.Cli.joinIntervals over the intervals dom, after the intervals up to the k-th, on its state (iv, n), the array of the intervals and the index of the last interval kept.

• size_eq : iv.size = dom.length

  The array has the length of dom.

• le_k : n ≤ k

  The last interval kept has an index at most k.

• k_lt : k < dom.length

  The intervals up to the k-th are among those of dom.

• tail_eq (j : ℕ) : k < j → iv[j]! = dom[j]!

  The intervals after the k-th are those of dom.

• noNaN (j : ℕ) : j ≤ n → iv[j]!.1.isNaN = false ∧ iv[j]!.2.isNaN = false

  The intervals kept, iv[0] to iv[n], have no NaN.

• covers (i : ℕ) : i ≤ k → ∀ (x : ℚ), InPair dom[i]! x → ∃ j ≤ n, InPair iv[j]! x

  The intervals kept hold every interval of dom up to the k-th.

• wellJoined : JoinsWell dom → (∀ j ≤ n, doubleValue iv[j]!.1.bits ≤ doubleValue iv[j]!.2.bits) ∧ (∀ j < n, doubleValue iv[j]!.2.bits < doubleValue iv[j + 1]!.1.bits) ∧ (n ≠ 0 → ∀ (i : ℕ), k < i → i < dom.length → doubleValue iv[n]!.1.bits ≤ doubleValue dom[i]!.1.bits)

  For intervals that join well, the intervals kept have l ≤ u and are increasing and strictly apart, and the lower end of the last one, when it is not the first, is at most those of the intervals of dom after the k-th.

theorem Ratpoints.Cli.joinInvariant_zero {dom : List (Double × Double)} (hnan : NoNaN dom) (h : ¬dom.isEmpty = true) : JoinInvariant dom 0 dom.toArray 0

theorem Ratpoints.Cli.doubleValue_pick_lt {a c : Double} (ha : a.isNaN = false) (hc : c.isNaN = false) : doubleValue (if c.lt a = true then c else a).bits = min (doubleValue a.bits) (doubleValue c.bits)

theorem Ratpoints.Cli.doubleValue_pick_gt {a c : Double} (ha : a.isNaN = false) (hc : c.isNaN = false) : doubleValue (if a.lt c = true then c else a).bits = max (doubleValue a.bits) (doubleValue c.bits)

theorem Ratpoints.Cli.joinWF_merge {dom : List (Double × Double)} {k n : ℕ} {iv iv' : Array (Double × Double)} {p : Double × Double} (hk : k + 1 < dom.length) (hc : iv[k + 1]! = dom[k + 1]!) (hp1 : doubleValue p.1.bits = min (doubleValue iv[n]!.1.bits) (doubleValue iv[k + 1]!.1.bits)) (hp2 : doubleValue p.2.bits = max (doubleValue iv[n]!.2.bits) (doubleValue iv[k + 1]!.2.bits)) (hn : iv'[n]! = p) (hne : ∀ (j : ℕ), j ≠ n → iv'[j]! = iv[j]!) (w1 : ∀ j ≤ n, doubleValue iv[j]!.1.bits ≤ doubleValue iv[j]!.2.bits) (w2 : ∀ j < n, doubleValue iv[j]!.2.bits < doubleValue iv[j + 1]!.1.bits) (w3 : n ≠ 0 → ∀ (i : ℕ), k < i → i < dom.length → doubleValue iv[n]!.1.bits ≤ doubleValue dom[i]!.1.bits) : (∀ j ≤ n, doubleValue iv'[j]!.1.bits ≤ doubleValue iv'[j]!.2.bits) ∧ (∀ j < n, doubleValue iv'[j]!.2.bits < doubleValue iv'[j + 1]!.1.bits) ∧ (n ≠ 0 → ∀ (i : ℕ), k + 1 < i → i < dom.length → doubleValue iv'[n]!.1.bits ≤ doubleValue dom[i]!.1.bits)

The order of the intervals kept by the loop of Ratpoints.Cli.joinIntervals after the next interval is joined to the last one kept, p, the least lower and the greatest upper end.

theorem Ratpoints.Cli.JoinInvariant.merge {dom : List (Double × Double)} {k n : ℕ} {iv iv' : Array (Double × Double)} {p : Double × Double} (hk : k + 1 < dom.length) (h : JoinInvariant dom k iv n) (hp1 : doubleValue p.1.bits = min (doubleValue iv[n]!.1.bits) (doubleValue iv[k + 1]!.1.bits)) (hp2 : doubleValue p.2.bits = max (doubleValue iv[n]!.2.bits) (doubleValue iv[k + 1]!.2.bits)) (hpn : p.1.isNaN = false ∧ p.2.isNaN = false) (hs : iv'.size = iv.size) (hn : iv'[n]! = p) (hne : ∀ (j : ℕ), j ≠ n → iv'[j]! = iv[j]!) : JoinInvariant dom (k + 1) iv' n

theorem Ratpoints.Cli.joinWF_push {dom : List (Double × Double)} {k n : ℕ} {iv : Array (Double × Double)} (hw : JoinsWell dom) (hk : k + 1 < dom.length) (hc : iv[k + 1]! = dom[k + 1]!) (hs : n + 1 < iv.size) (hgt : doubleValue iv[n]!.2.bits < doubleValue iv[k + 1]!.1.bits) (w1 : ∀ j ≤ n, doubleValue iv[j]!.1.bits ≤ doubleValue iv[j]!.2.bits) (w2 : ∀ j < n, doubleValue iv[j]!.2.bits < doubleValue iv[j + 1]!.1.bits) : (∀ j ≤ n + 1, doubleValue (iv.set! (n + 1) iv[k + 1]!)[j]!.1.bits ≤ doubleValue (iv.set! (n + 1) iv[k + 1]!)[j]!.2.bits) ∧ (∀ j < n + 1, doubleValue (iv.set! (n + 1) iv[k + 1]!)[j]!.2.bits < doubleValue (iv.set! (n + 1) iv[k + 1]!)[j + 1]!.1.bits) ∧ (n + 1 ≠ 0 → ∀ (i : ℕ), k + 1 < i → i < dom.length → doubleValue (iv.set! (n + 1) iv[k + 1]!)[n + 1]!.1.bits ≤ doubleValue dom[i]!.1.bits)

The order of the intervals kept by the loop of Ratpoints.Cli.joinIntervals after the next interval, which lies above the last one kept, is kept after it.

theorem Ratpoints.Cli.JoinInvariant.push {dom : List (Double × Double)} {k n : ℕ} {iv : Array (Double × Double)} (hnan : NoNaN dom) (hk : k + 1 < dom.length) (h : JoinInvariant dom k iv n) (hgt : doubleValue iv[n]!.2.bits < doubleValue iv[k + 1]!.1.bits) : JoinInvariant dom (k + 1) (iv.set! (n + 1) iv[k + 1]!) (n + 1)

theorem Ratpoints.Cli.JoinInvariant.lt_cur {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv : Array (Double × Double)} (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) : pref.length + 1 = cur ∧ cur < dom.length ∧ n < cur ∧ cur < iv.size

theorem Ratpoints.Cli.JoinInvariant.merge_pick {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv iv' : Array (Double × Double)} (hnan : NoNaN dom) (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) (hle : iv[cur]!.1.le iv[n]!.2 = true) (hs : iv'.size = iv.size) (hn : iv'[n]! = (if iv[cur]!.1.lt iv[n]!.1 = true then iv[cur]!.1 else iv[n]!.1, if iv[n]!.2.lt iv[cur]!.2 = true then iv[cur]!.2 else iv[n]!.2)) (hne : ∀ (j : ℕ), j ≠ n → iv'[j]! = iv[j]!) : JoinInvariant dom (pref ++ [cur]).length iv' n

A step of the loop of Ratpoints.Cli.joinIntervals that joins the next interval to the last one kept: the slot of that one holds the least lower and the greatest upper end.

theorem Ratpoints.Cli.JoinInvariant.merge_lt_lt {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv : Array (Double × Double)} (hnan : NoNaN dom) (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) (h1 : iv[cur]!.1.le iv[n]!.2 = true) (h2 : iv[cur]!.1.lt iv[n]!.1 = true) (h3 : (iv.set! n (iv[cur]!.1, iv[n]!.2))[n]!.2.lt (iv.set! n (iv[cur]!.1, iv[n]!.2))[cur]!.2 = true) : JoinInvariant dom (pref ++ [cur]).length ((iv.set! n (iv[cur]!.1, iv[n]!.2)).set! n ((iv.set! n (iv[cur]!.1, iv[n]!.2))[n]!.1, (iv.set! n (iv[cur]!.1, iv[n]!.2))[cur]!.2)) n

theorem Ratpoints.Cli.JoinInvariant.merge_lt_ge {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv : Array (Double × Double)} (hnan : NoNaN dom) (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) (h1 : iv[cur]!.1.le iv[n]!.2 = true) (h2 : iv[cur]!.1.lt iv[n]!.1 = true) (h3 : ¬(iv.set! n (iv[cur]!.1, iv[n]!.2))[n]!.2.lt (iv.set! n (iv[cur]!.1, iv[n]!.2))[cur]!.2 = true) : JoinInvariant dom (pref ++ [cur]).length (iv.set! n (iv[cur]!.1, iv[n]!.2)) n

theorem Ratpoints.Cli.JoinInvariant.merge_ge_lt {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv : Array (Double × Double)} (hnan : NoNaN dom) (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) (h1 : iv[cur]!.1.le iv[n]!.2 = true) (h2 : ¬iv[cur]!.1.lt iv[n]!.1 = true) (h3 : iv[n]!.2.lt iv[cur]!.2 = true) : JoinInvariant dom (pref ++ [cur]).length (iv.set! n (iv[n]!.1, iv[cur]!.2)) n

theorem Ratpoints.Cli.JoinInvariant.merge_ge_ge {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv : Array (Double × Double)} (hnan : NoNaN dom) (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) (h1 : iv[cur]!.1.le iv[n]!.2 = true) (h2 : ¬iv[cur]!.1.lt iv[n]!.1 = true) (h3 : ¬iv[n]!.2.lt iv[cur]!.2 = true) : JoinInvariant dom (pref ++ [cur]).length iv n

theorem Ratpoints.Cli.JoinInvariant.push_cur {dom : List (Double × Double)} {pref suff : List ℕ} {cur n : ℕ} {iv : Array (Double × Double)} (hnan : NoNaN dom) (hh : ForIn.toList [1:dom.length] = pref ++ cur :: suff) (h : JoinInvariant dom pref.length iv n) (h1 : ¬iv[cur]!.1.le iv[n]!.2 = true) : JoinInvariant dom (pref ++ [cur]).length (iv.set! (n + 1) iv[cur]!) (n + 1)

theorem Ratpoints.Cli.joinIntervals_post_of_isEmpty {dom : List (Double × Double)} (hnan : NoNaN dom) (h : dom.isEmpty = true) : (dom = [] ↔ dom = []) ∧ NoNaN dom ∧ (∀ (x : ℚ), (∃ p ∈ dom, InPair p x) → ∃ p ∈ dom, InPair p x) ∧ (JoinsWell dom → AreSearchIntervals (List.map (fun (p : Double × Double) => (doubleValue p.1.bits, doubleValue p.2.bits)) dom))

theorem Ratpoints.Cli.JoinInvariant.post {dom : List (Double × Double)} {iv : Array (Double × Double)} {n : ℕ} (h : JoinInvariant dom (ForIn.toList [1:dom.length]).length iv n) : (List.take (n + 1) iv.toList = [] ↔ dom = []) ∧ NoNaN (List.take (n + 1) iv.toList) ∧ (∀ (x : ℚ), (∃ p ∈ dom, InPair p x) → ∃ p ∈ List.take (n + 1) iv.toList, InPair p x) ∧ (JoinsWell dom → AreSearchIntervals (List.map (fun (p : Double × Double) => (doubleValue p.1.bits, doubleValue p.2.bits)) (List.take (n + 1) iv.toList)))

theorem Ratpoints.Cli.joinIntervals_spec (dom : List (Double × Double)) : ⦃ NoNaN dom ⦄ joinIntervals dom ⦃ fun (r : List (Double × Double)) => (r = [] ↔ dom = []) ∧ NoNaN r ∧ (∀ (x : ℚ), (∃ p ∈ dom, InPair p x) → ∃ p ∈ r, InPair p x) ∧ (JoinsWell dom → AreSearchIntervals (List.map (fun (p : Double × Double) => (doubleValue p.1.bits, doubleValue p.2.bits)) r)) ⦄

join_intervals keeps the search intervals of the command line, without NaN: it gives none exactly when there are none, the intervals it gives hold the values of the intervals it joins, and for intervals that join well (with l ≤ u and the lower ends increasing from the second on) the intervals it gives have l ≤ u and are increasing and strictly apart.

theorem Ratpoints.Cli.run_joinIntervals {dom : List (Double × Double)} (h : NoNaN dom) : ((joinIntervals dom).run = [] ↔ dom = []) ∧ NoNaN (joinIntervals dom).run ∧ (∀ (x : ℚ), (∃ p ∈ dom, InPair p x) → ∃ p ∈ (joinIntervals dom).run, InPair p x) ∧ (JoinsWell dom → AreSearchIntervals (List.map (fun (p : Double × Double) => (doubleValue p.1.bits, doubleValue p.2.bits)) (joinIntervals dom).run))