The output of the program

What the program ratpoints-lean prints for the points of a successful search. Its callback Ratpoints.Cli.process, called for the points of a list L in turn from the data Ratpoints.Cli.Data.ofOutput u o of the settings u of the output and the options o of the search, counts the points of L that it keeps (Ratpoints.Cli.Data.keeps: all but those at infinity under -i and the affine ones outside the search intervals of the command line), of these only the first under -1, at which it stops the search (Ratpoints.Cli.countedPoints), and prints them unless -z, each after the string before the points (-fs) if it is the first and else after the string between them (-fm), in the format of -f: so the text printed, with the string before the points when no point was printed, is the string before the points followed by the formatted points with the string between them in between (Ratpoints.Cli.out_append_deliver_process_ofOutput), and the count is their number (Ratpoints.Cli.total_deliver_process). By the protocol of the delivery (Ratpoints.map_findPointsWith_eq_map_findPoints), which says that for every value of the options of the sieve the search delivers to a callback the points of Ratpoints.findPoints in their order until a call stops it, this is what Ratpoints.Cli.run prints between the head of the report and its end, without -v, whose report of the library comes between the points; under -q it is all that it prints, with the string after the points (-fe) at the end, and under -1 the one point printed is the first point of the list of Ratpoints.findPoints that the callback keeps. The search runs on the search intervals of the command line joined (Ratpoints.Cli.joinIntervals).

The search region of the command line: the reading of -l and -u keeps an invariant (Ratpoints.Cli.Intervals.ReadsWF: the exact ends are those of increasing and disjoint intervals l ≤ u, checked by error 7, and the doubles of each interval hold it as far as the search goes), which Ratpoints.Cli.Intervals.lower, Ratpoints.Cli.Intervals.upper and Ratpoints.Cli.Intervals.complete keep, over the options by Ratpoints.Cli.checkOptions_preserves; so the test of the callback is the exact search region of the command line, and the joined intervals hold it for the numbers |x| ≤ H of the search. For words of fewer than 2 ^ 56 characters, the doubles of the lower ends after the first are moreover the largest doubles at most their ends (Ratpoints.Cli.Intervals.LowerMax), which makes the joined intervals well formed: the library never refuses them, and error 9 is unreachable from the command line.

Main definitions

• Ratpoints.Cli.Data.keeps, Ratpoints.Cli.countedPoints: the points that the callback keeps, and those that it counts.
• Ratpoints.Cli.IntervalOf, Ratpoints.Cli.Intervals.ReadsWF, Ratpoints.Cli.Intervals.LowerMax: the invariants of the reading of the search intervals of the command line.

Main statements

• Ratpoints.Cli.deliver_process: the delivery of a list to the callback of the program.
• Ratpoints.Cli.out_append_deliver_process_ofOutput, Ratpoints.Cli.total_deliver_process: the text that the callback prints and the count.
• Ratpoints.Cli.run_eq_of_findPointsWith_eq_ok, Ratpoints.Cli.total_eq_of_findPointsWith_eq_ok: what the program prints for a successful search without -v, and the count that its report gives.
• Ratpoints.Cli.findPointsVerbose_eq_ok_of_findPointsWith_eq_ok, Ratpoints.Cli.verbose_eq_false_of_input_eq_ok: the search with the print channel that prints nothing, which the program runs without -v, and -q cancels -v.
• Ratpoints.Cli.run_eq_of_findPoints_eq_ok: what the program prints under -q.
• Ratpoints.Cli.run_eq_of_onePoint: under -q -1, the first point that the callback keeps.
• Ratpoints.Cli.reads_of_input_eq_ok: the search intervals of a command line that the program accepts.
• Ratpoints.Cli.inRegion_iff_of_input_eq_ok, Ratpoints.Cli.inIntervals_joinIntervals_of_inExactRegion, Ratpoints.Cli.intervalsWF_joinIntervals_of_input_eq_ok: the test of the callback is the exact search region of the command line (Ratpoints.Cli.InExactRegion), and the joined search intervals hold it for |x| ≤ H and, for words of fewer than 2 ^ 56 characters, are well formed.
• Ratpoints.Cli.mem_filter_keeps_iff_of_input_eq_ok: assuming Sturm's theorem when the Sturm step is on, the points that the program prints are exactly the points in the exact search region of its command line.

The points that the callback counts

def Ratpoints.Cli.Data.keeps (d : Data) (p : ℤ × ℤ × ℤ) : Bool

Whether the callback Ratpoints.Cli.process of the program with the data d keeps the point p = (x, y, z), counting it, printing it unless -z and stopping the search at it under -1: a point at infinity (z = 0) unless the points at infinity are passed over (-i), and an affine point when the command line gives no search intervals or x / z lies in one of them (Ratpoints.Cli.inRegion).

Equations

• d.keeps p = ((d.pointsAtInfty || p.2.2 != 0) && (p.2.2 == 0 || d.numInter == 0 || (Ratpoints.Cli.inRegion p.1 p.2.2 d.ends d.numInter).run))

def Ratpoints.Cli.countedPoints (keep : ℤ × ℤ × ℤ → Bool) (onePoint : Bool) (L : List (ℤ × ℤ × ℤ)) : List (ℤ × ℤ × ℤ)

The points of the list L, in their order, that the callback Ratpoints.Cli.process of the program counts when it is called for the points of L in turn, from data that keeps the points that pass keep (Ratpoints.Cli.Data.keeps) and whose setting of one point is onePoint, while it has not stopped the search: the points of L that pass keep, and of these only the first when one point is enough (-1, onePoint set), at which the callback stops the search.

Equations

• Ratpoints.Cli.countedPoints keep onePoint L = if onePoint = true then List.take 1 (List.filter keep L) else List.filter keep L

theorem Ratpoints.Cli.countedPoints_nil (keep : ℤ × ℤ × ℤ → Bool) (onePoint : Bool) : countedPoints keep onePoint [] = []

theorem Ratpoints.Cli.countedPoints_cons_of_not_keep {keep : ℤ × ℤ × ℤ → Bool} {p : ℤ × ℤ × ℤ} (h : keep p = false) (onePoint : Bool) (L : List (ℤ × ℤ × ℤ)) : countedPoints keep onePoint (p :: L) = countedPoints keep onePoint L

theorem Ratpoints.Cli.countedPoints_cons_of_keep {keep : ℤ × ℤ × ℤ → Bool} {p : ℤ × ℤ × ℤ} (h : keep p = true) (onePoint : Bool) (L : List (ℤ × ℤ × ℤ)) : countedPoints keep onePoint (p :: L) = if onePoint = true then [p] else p :: countedPoints keep onePoint L

What the callback prints

def Ratpoints.Cli.Data.printPoint (d : Data) (p : ℤ × ℤ × ℤ) : Data

The data d of the callback Ratpoints.Cli.process after it has printed the point p = (x, y, z): d itself when no point is printed (-z), and otherwise d with the flag printBetween set and with the text of the point appended to the text printed so far, the string between the points (-fm) if a point was printed before and else the string before the points (-fs), then the point in the format (Ratpoints.Cli.formatPoint). This is what a call of the callback that does not pass over the point does to its data.

Equations

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

theorem Ratpoints.Cli.Data.printPoint_of_noOutput {d : Data} (h : d.noOutput = true) (p : ℤ × ℤ × ℤ) : d.printPoint p = d

theorem Ratpoints.Cli.Data.printPoint_of_not_noOutput {d : Data} (h : d.noOutput = false) (p : ℤ × ℤ × ℤ) : d.printPoint p = { printBetween := true, noOutput := d.noOutput, onePoint := d.onePoint, pointsAtInfty := d.pointsAtInfty, noY := d.noY, pf := d.pf, stringBefore := d.stringBefore, stringBetween := d.stringBetween, numInter := d.numInter, ends := d.ends, out := d.out ++ printString (if d.printBetween = true then d.stringBetween else d.stringBefore) ++ formatPoint d.noY p.1 p.2.2 p.2.1 d.pf.toList }

@[simp]

theorem Ratpoints.Cli.Data.onePoint_printPoint (d : Data) (p : ℤ × ℤ × ℤ) : (d.printPoint p).onePoint = d.onePoint

@[simp]

theorem Ratpoints.Cli.Data.keeps_printPoint (d : Data) (p : ℤ × ℤ × ℤ) : (d.printPoint p).keeps = d.keeps

theorem Ratpoints.Cli.Data.foldl_printPoint_of_noOutput {d : Data} (h : d.noOutput = true) (K : List (ℤ × ℤ × ℤ)) : List.foldl printPoint d K = d

theorem Ratpoints.Cli.Data.foldl_printPoint_of_printBetween {d : Data} (hn : d.noOutput = false) (hb : d.printBetween = true) (K : List (ℤ × ℤ × ℤ)) : List.foldl printPoint d K = { printBetween := d.printBetween, noOutput := d.noOutput, onePoint := d.onePoint, pointsAtInfty := d.pointsAtInfty, noY := d.noY, pf := d.pf, stringBefore := d.stringBefore, stringBetween := d.stringBetween, numInter := d.numInter, ends := d.ends, out := d.out ++ String.join (List.map (fun (p : ℤ × ℤ × ℤ) => printString d.stringBetween ++ formatPoint d.noY p.1 p.2.2 p.2.1 d.pf.toList) K) }

Once a point was printed, each point printed appends the string between the points and the point in the format.

theorem Ratpoints.Cli.Data.out_append_foldl_printPoint {d : Data} (hb : d.printBetween = false) (ho : d.out = "") (K : List (ℤ × ℤ × ℤ)) : ((List.foldl printPoint d K).out ++ if (List.foldl printPoint d K).printBetween = true then "" else printString d.stringBefore) = printString d.stringBefore ++ (printString d.stringBetween).intercalate (List.map (fun (p : ℤ × ℤ × ℤ) => formatPoint d.noY p.1 p.2.2 p.2.1 d.pf.toList) (if d.noOutput = true then [] else K))

From data that has printed nothing, the text printed for the points of K, with the string before the points when no point was printed, is the string before the points followed by the points printed in the format, with the string between them in between: none under -z.

The delivery to the callback

theorem Ratpoints.Cli.call_process_of_keep {r : Delivery Data} {p : ℤ × ℤ × ℤ} (h : r.info.keeps p = true) : Delivery.call process r p.1 p.2.2 p.2.1 = { info := r.info.printPoint p, total := r.total + 1, quit := r.info.onePoint }

A call of the callback for a point p = (x, y, z) that it keeps (Ratpoints.Cli.Data.keeps) prints it (Ratpoints.Cli.Data.printPoint), counts it and stops the search under -1.

theorem Ratpoints.Cli.call_process_of_not_keep {r : Delivery Data} {p : ℤ × ℤ × ℤ} (h : r.info.keeps p = false) : Delivery.call process r p.1 p.2.2 p.2.1 = { info := r.info, total := r.total, quit := false }

theorem Ratpoints.Cli.deliver_process (d : Data) (t : ℤ) (L : List (ℤ × ℤ × ℤ)) : Delivery.deliver process { info := d, total := t, quit := false } L = { info := List.foldl Data.printPoint d (countedPoints d.keeps d.onePoint L), total := t + ↑(countedPoints d.keeps d.onePoint L).length, quit := d.onePoint && L.any d.keeps }

The delivery of the points of L to the callback of the program from the data d and the count t, with the flag of the stop clear: the points that the callback counts (Ratpoints.Cli.countedPoints) are printed in turn and counted, and the search is stopped when one point is enough and L has a point that the callback keeps (Ratpoints.Cli.Data.keeps).

theorem Ratpoints.Cli.total_deliver_process (d : Data) (t : ℤ) (L : List (ℤ × ℤ × ℤ)) : (Delivery.deliver process { info := d, total := t, quit := false } L).total = t + ↑(countedPoints d.keeps d.onePoint L).length

theorem Ratpoints.Cli.out_append_deliver_process_ofOutput (u : Output) (o : Options) (L : List (ℤ × ℤ × ℤ)) : ((Delivery.deliver process { info := Data.ofOutput u o, total := 0, quit := false } L).info.out ++ if (Delivery.deliver process { info := Data.ofOutput u o, total := 0, quit := false } L).info.printBetween = true then "" else printString u.stringBefore) = printString u.stringBefore ++ (printString u.stringBetween).intercalate (List.map (fun (p : ℤ × ℤ × ℤ) => formatPoint (o.noCheck || o.noY) p.1 p.2.2 p.2.1 (u.printFormat.getD "").toList) (if u.noOutput = true then [] else countedPoints (Data.ofOutput u o).keeps u.onePoint L))

The text that the callback of the program prints for the points of L, from the data of the settings u of the output and the options o of the search, with the string before the points when it printed no point, as the program prints it: the string before the points, then the points that the callback counts (Ratpoints.Cli.countedPoints), in the format, with the string between the points in between, none under -z.

The program

theorem Ratpoints.Cli.preamble_eq_empty_of_quiet (c : List ℤ) (H : ℕ) {u : Output} (hq : u.quiet = true) (dom : List (Double × Double)) : preamble c H u dom = ""

theorem Ratpoints.Cli.report_eq_empty_of_quiet {σ : Type} (s : SieveOptions) (o : Options) {u : Output} (hq : u.quiet = true) (r : Outcome σ) : report s o u r = ""

theorem Ratpoints.Cli.findPointsVerbose_eq_ok_of_findPointsWith_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {info : σ} {r : Outcome σ} (hr : findPointsWith c H s o process info = Except.ok r) : (findPointsVerbose c H s o process info fun (x : String) (s : σ) => s) = Except.ok r

A search with the print channel that prints nothing returns the outcome of Ratpoints.findPointsVerbose with that channel.

theorem Ratpoints.Cli.run_eq_of_findPointsWith_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} {r : Outcome Data} {L : List (ℤ × ℤ × ℤ)} (hi : input args = Except.ok (c, H, s, o, u)) (hv : u.verbose = false) (hr : findPointsWith c H { numPrimes := s.numPrimes, sp1 := s.sp1, sp2 := s.sp2, survivorsPerWord := s.survivorsPerWord, sp2Extra := s.sp2Extra, sp2U0 := s.sp2U0, costTable := s.costTable, adapt := s.adapt, sp3Extra := s.sp3Extra, sp3PerDenom := s.sp3PerDenom, checkCost := s.checkCost, maxForbidden := s.maxForbidden, jacobi := s.jacobi } { reverse := o.reverse, sturm := o.sturm, noCheck := o.noCheck, noY := o.noY, domain := (joinIntervals o.domain).run, bLow := o.bLow, bHigh := o.bHigh } process (Data.ofOutput u o) = Except.ok r) (hL : findPoints c H { numPrimes := s.numPrimes, sp1 := s.sp1, sp2 := s.sp2, survivorsPerWord := s.survivorsPerWord, sp2Extra := s.sp2Extra, sp2U0 := s.sp2U0, costTable := s.costTable, adapt := s.adapt, sp3Extra := s.sp3Extra, sp3PerDenom := s.sp3PerDenom, checkCost := s.checkCost, maxForbidden := s.maxForbidden, jacobi := s.jacobi } { reverse := o.reverse, sturm := o.sturm, noCheck := o.noCheck, noY := o.noY, domain := (joinIntervals o.domain).run, bLow := o.bLow, bHigh := o.bHigh } = Except.ok L) : run args = (preamble c H u o.domain ++ printString u.stringBefore ++ (printString u.stringBetween).intercalate (List.map (fun (p : ℤ × ℤ × ℤ) => formatPoint (o.noCheck || o.noY) p.1 p.2.2 p.2.1 (u.printFormat.getD "").toList) (if u.noOutput = true then [] else countedPoints (Data.ofOutput u o).keeps u.onePoint L)) ++ printString u.stringAfter ++ report s { reverse := o.reverse, sturm := o.sturm, noCheck := o.noCheck, noY := o.noY, domain := (joinIntervals o.domain).run, bLow := o.bLow, bHigh := o.bHigh } u r, 0)

What the program prints for a command line that it reads as the coefficients c, the height bound H, the options s of the sieve, the options o of the search and the settings u of the output, without -v, when the search Ratpoints.findPoints with the program's array size on the search intervals of the command line joined (Ratpoints.Cli.joinIntervals) returns the list L and the search with the callback of the program the outcome r: the head of the report, the string before the points, the points of L that the callback counts (Ratpoints.Cli.countedPoints: those that it keeps, Ratpoints.Cli.Data.keeps, only the first of these under -1) in the format, with the string between them in between, none under -z, the string after the points and the end of the report; the protocol of the delivery holds for every value of the options (Ratpoints.map_findPointsWith_eq_map_findPoints).

theorem Ratpoints.Cli.total_eq_of_findPointsWith_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o o' : Options} {u : Output} {r : Outcome Data} {L : List (ℤ × ℤ × ℤ)} (hr : findPointsWith c H s o' process (Data.ofOutput u o) = Except.ok r) (hL : findPoints c H s o' = Except.ok L) : r.total = ↑(countedPoints (Data.ofOutput u o).keeps u.onePoint L).length

The count of the points that the report of the program gives: the number of the points of the list of Ratpoints.findPoints that the callback of the program counts (Ratpoints.Cli.countedPoints), for every value of the options of the sieve.

theorem Ratpoints.Cli.le_and_lt_of_heightBound_eq_ok {h : String} {H : ℕ} (hH : heightBound h = Except.ok H) : 1 ≤ H ∧ H < 2 ^ 63

theorem Ratpoints.Cli.exists_checkOptions_eq_ok_of_input_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hi : input args = Except.ok (c, H, s, o, u)) : ∃ (os : List String) (iv : Intervals), (∀ a ∈ os, a ∈ args) ∧ 1 ≤ H ∧ H < 2 ^ 63 ∧ (∃ (s' : SieveOptions) (o' : Options) (u' : Output), checkOptions H ({ }, { bHigh := ↑H }, { }, { }) os = Except.ok (s', o', u', iv)) ∧ o.domain = List.take (iv.complete H).numInter (iv.complete H).domain.toList ∧ u.ends = (iv.complete H).ends ∧ (u.quiet = true → u.verbose = false)

What a command line that the program accepts gives: the options are words of the command line, the height bound is a positive long, the reading of the options from the defaults succeeds, the search intervals of the options and the exact ends of the settings of the output are those of the intervals read and completed (Ratpoints.Cli.Intervals.complete), and -q cancels -v.

theorem Ratpoints.Cli.verbose_eq_false_of_input_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hi : input args = Except.ok (c, H, s, o, u)) (hq : u.quiet = true) : u.verbose = false

The program reads -v only without -q: under -q the settings of the output have the flag of the report of the library clear.

theorem Ratpoints.Cli.run_eq_of_findPoints_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} {L : List (ℤ × ℤ × ℤ)} (hi : input args = Except.ok (c, H, s, o, u)) (hq : u.quiet = true) (hL : findPoints c H { numPrimes := s.numPrimes, sp1 := s.sp1, sp2 := s.sp2, survivorsPerWord := s.survivorsPerWord, sp2Extra := s.sp2Extra, sp2U0 := s.sp2U0, costTable := s.costTable, adapt := s.adapt, sp3Extra := s.sp3Extra, sp3PerDenom := s.sp3PerDenom, checkCost := s.checkCost, maxForbidden := s.maxForbidden, jacobi := s.jacobi } { reverse := o.reverse, sturm := o.sturm, noCheck := o.noCheck, noY := o.noY, domain := (joinIntervals o.domain).run, bLow := o.bLow, bHigh := o.bHigh } = Except.ok L) : run args = (printString u.stringBefore ++ (printString u.stringBetween).intercalate (List.map (fun (p : ℤ × ℤ × ℤ) => formatPoint (o.noCheck || o.noY) p.1 p.2.2 p.2.1 (u.printFormat.getD "").toList) (if u.noOutput = true then [] else countedPoints (Data.ofOutput u o).keeps u.onePoint L)) ++ printString u.stringAfter, 0)

What the program prints under -q for a command line on which the search Ratpoints.findPoints on the search intervals of the command line joined returns the list L: the string before the points, the points of L that the callback of the program counts (Ratpoints.Cli.countedPoints: those that it keeps, Ratpoints.Cli.Data.keeps, only the first of these under -1) in the format, with the string between them in between, none under -z, and the string after the points; it exits with the status 0.

theorem Ratpoints.Cli.run_eq_of_onePoint {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} {L : List (ℤ × ℤ × ℤ)} {p : ℤ × ℤ × ℤ} (hi : input args = Except.ok (c, H, s, o, u)) (hq : u.quiet = true) (h1 : u.onePoint = true) (hz : u.noOutput = false) (hL : findPoints c H { numPrimes := s.numPrimes, sp1 := s.sp1, sp2 := s.sp2, survivorsPerWord := s.survivorsPerWord, sp2Extra := s.sp2Extra, sp2U0 := s.sp2U0, costTable := s.costTable, adapt := s.adapt, sp3Extra := s.sp3Extra, sp3PerDenom := s.sp3PerDenom, checkCost := s.checkCost, maxForbidden := s.maxForbidden, jacobi := s.jacobi } { reverse := o.reverse, sturm := o.sturm, noCheck := o.noCheck, noY := o.noY, domain := (joinIntervals o.domain).run, bLow := o.bLow, bHigh := o.bHigh } = Except.ok L) (hK : (List.filter (Data.ofOutput u o).keeps L).head? = some p) : run args = (printString u.stringBefore ++ formatPoint (o.noCheck || o.noY) p.1 p.2.2 p.2.1 (u.printFormat.getD "").toList ++ printString u.stringAfter, 0)

Under -q -1, without -z, the program prints the first point p of the list of Ratpoints.findPoints on the search intervals of the command line joined that the callback keeps (Ratpoints.Cli.Data.keeps: all of it but the points at infinity under -i and the affine points outside the search intervals of the command line), in the format, between the string before the points and the string after them.

The search region of the command line

theorem Ratpoints.Cli.Intervals.eq_of_lower_eq_ok {iv iv' : Intervals} {a : String} (h : iv.lower a = Except.ok iv') : iv.lSeen = false ∧ iv.numInter ≠ maxDegree ∧ ∃ (e : ExactEnd) (d : Double), (scanEnd a (-1)).run = some (e, d) ∧ (0 < iv.numInter → cmpEnd iv.ends[2 * iv.numInter - 1]! e < 0) ∧ iv' = { lSeen := true, numInter := iv.numInter, domain := iv.domain.set! iv.numInter (d, iv.domain[iv.numInter]!.2), ends := iv.ends.set! (2 * iv.numInter) e }

theorem Ratpoints.Cli.Intervals.eq_of_upper_eq_ok_of_lSeen {iv iv' : Intervals} {H : ℕ} {a : String} (hl : iv.lSeen = true) (h : iv.upper H a = Except.ok iv') : ∃ (e : ExactEnd) (d : Double), (scanEnd a 1).run = some (e, d) ∧ ¬0 < cmpEnd (iv.ends.set! (2 * iv.numInter + 1) e)[2 * iv.numInter]! (iv.ends.set! (2 * iv.numInter + 1) e)[2 * iv.numInter + 1]! ∧ iv' = { numInter := iv.numInter + 1, domain := iv.domain.set! iv.numInter (iv.domain[iv.numInter]!.1, d), ends := iv.ends.set! (2 * iv.numInter + 1) e }

theorem Ratpoints.Cli.Intervals.eq_of_upper_eq_ok_of_lSeen_eq_false {iv iv' : Intervals} {H : ℕ} {a : String} (hl : iv.lSeen = false) (hd : 0 < iv.domain.size) (he : 1 < iv.ends.size) (h : iv.upper H a = Except.ok iv') : iv.numInter = 0 ∧ ∃ (e : ExactEnd) (d : Double), (scanEnd a 1).run = some (e, d) ∧ ¬↑0 < cmpEnd (have __src := iv.ends[0]!; { inf := -1, q := __src.q }) e ∧ iv' = { numInter := 1, domain := iv.domain.set! 0 (if d.lt (heightEnd H).neg = true then Double.huge.neg else (heightEnd H).neg, d), ends := (iv.ends.set! 0 (have __src := iv.ends[0]!; { inf := -1, q := __src.q })).set! 1 e }

def Ratpoints.Cli.IntervalOf (H : ℕ) (d : Double × Double) (el eu : ExactEnd) : Prop

The interval d of doubles holds the exact interval from el to eu of the command line as far as the search goes: neither end of d is a NaN, the lower end of d is at most its upper end, and every x with |x| ≤ H between the exact ends lies in d.

Equations

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

structure Ratpoints.Cli.Intervals.ReadsWF (H : ℕ) (iv : Intervals) (n : ℕ) (l : Bool) : Prop

The reading iv of the search intervals of the command line for the height bound H, with n complete intervals and a lower end read after them when l: the arrays have their 2 maxDegree entries and room for the intervals, the exact ends are infinite only as ±1 and are the ends of increasing and disjoint intervals l ≤ u, the double of a pending lower end is below it, and the doubles of each complete interval hold it as far as the search goes.

• size_ends : iv.ends.size = 2 * maxDegree

  The exact ends have their 2 maxDegree entries.

• size_domain : iv.domain.size = 2 * maxDegree

  The doubles of the intervals have their 2 maxDegree entries.

• le_maxDegree : (n + if l = true then 1 else 0) ≤ maxDegree

  There is room for the intervals read.

• inf_mem (j : ℕ) : iv.ends[j]!.inf = -1 ∨ iv.ends[j]!.inf = 0 ∨ iv.ends[j]!.inf = 1

  An exact end is infinite only as -1 or 1.

• chain : ChainEnds (fun (j : ℕ) => iv.ends[j]!.value) (2 * n + if l = true then 1 else 0)

  The exact ends read are the ends of increasing and disjoint intervals l ≤ u.

• pending : l = true → iv.domain[n]!.1.isNaN = false ∧ doubleValue iv.domain[n]!.1.bits ≤ iv.ends[2 * n]!.value

  The double of a pending lower end is not a NaN and lies at or below it.

• interval (j : ℕ) : j < n → IntervalOf H iv.domain[j]! iv.ends[2 * j]! iv.ends[2 * j + 1]!

  The doubles of each complete interval hold it as far as the search goes.

theorem Ratpoints.Cli.Intervals.ReadsWF.lt_maxDegree {H n : ℕ} {iv : Intervals} (hw : ReadsWF H iv n true) : n < maxDegree

theorem Ratpoints.Cli.Intervals.ReadsWF.le_maxDegree' {H n : ℕ} {iv : Intervals} (hw : ReadsWF H iv n false) : n ≤ maxDegree

theorem Ratpoints.Cli.Intervals.ReadsWF.chainEnds_two_mul {H n : ℕ} {iv : Intervals} (hw : ReadsWF H iv n false) : ChainEnds (fun (j : ℕ) => iv.ends[j]!.value) (2 * n)

theorem Ratpoints.Cli.Intervals.ReadsWF.chainEnds_two_mul_add_one {H n : ℕ} {iv : Intervals} (hw : ReadsWF H iv n true) : ChainEnds (fun (j : ℕ) => iv.ends[j]!.value) (2 * n + 1)

theorem Ratpoints.Cli.ChainEnds.snoc {v w : ℕ → WithBotTop ℚ} {m : ℕ} (h : ChainEnds v m) (hvw : ∀ i < m, w i = v i) (hlast : 0 < m → w (m - 1) ≤ w m ∧ ((m - 1) % 2 = 1 → w (m - 1) < w m)) : ChainEnds w (m + 1)

theorem Ratpoints.Cli.ChainEnds.set! {ends : Array ExactEnd} {m : ℕ} {e : ExactEnd} (h : ChainEnds (fun (j : ℕ) => ends[j]!.value) m) (hm : m < ends.size) (hlink : 0 < m → ends[m - 1]!.value ≤ e.value ∧ ((m - 1) % 2 = 1 → ends[m - 1]!.value < e.value)) : ChainEnds (fun (j : ℕ) => (ends.set! m e)[j]!.value) (m + 1)

An end set after the ends of increasing and disjoint intervals l ≤ u continues them when it lies at or above the last one, strictly above an upper end.

theorem Ratpoints.Cli.inf_mem_set! {ends : Array ExactEnd} (h : ∀ (j : ℕ), ends[j]!.inf = -1 ∨ ends[j]!.inf = 0 ∨ ends[j]!.inf = 1) {e : ExactEnd} (he : e.inf = -1 ∨ e.inf = 0 ∨ e.inf = 1) (i j : ℕ) : (ends.set! i e)[j]!.inf = -1 ∨ (ends.set! i e)[j]!.inf = 0 ∨ (ends.set! i e)[j]!.inf = 1

theorem Ratpoints.Cli.intervalOf_set! {H n i k : ℕ} {dom : Array (Double × Double)} {ends : Array ExactEnd} {p : Double × Double} {e : ExactEnd} (h : ∀ j < n, IntervalOf H dom[j]! ends[2 * j]! ends[2 * j + 1]!) (hi : n ≤ i) (hk : 2 * n ≤ k) (j : ℕ) (hj : j < n) : IntervalOf H (dom.set! i p)[j]! (ends.set! k e)[2 * j]! (ends.set! k e)[2 * j + 1]!

theorem Ratpoints.Cli.readsWF_default (H : ℕ) : Intervals.ReadsWF H { } 0 false

theorem Ratpoints.Cli.Intervals.ReadsWF.lower {H : ℕ} {iv iv' : Intervals} {a : String} (hw : ReadsWF H iv iv.numInter iv.lSeen) (h : iv.lower a = Except.ok iv') : ReadsWF H iv' iv'.numInter iv'.lSeen

theorem Ratpoints.Cli.intervalOf_of_le {H : ℕ} {l d : Double} {el eu : ExactEnd} (hl : l.isNaN = false) (hd : d.isNaN = false) (h1 : doubleValue l.bits ≤ el.value) (h2 : el.value ≤ eu.value) (h3 : eu.value ≤ doubleValue d.bits) : IntervalOf H (l, d) el eu

theorem Ratpoints.Cli.doubleValue_neg_heightEnd {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) : doubleValue (heightEnd H).neg.bits = WithBotTop.coe (-(heightEnd H).toRat)

theorem Ratpoints.Cli.doubleValue_neg_heightEnd_le {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {x : ℚ} (hx : |x| ≤ ↑H) : doubleValue (heightEnd H).neg.bits ≤ WithBotTop.coe x

theorem Ratpoints.Cli.le_doubleValue_heightEnd {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {x : ℚ} (hx : |x| ≤ ↑H) : WithBotTop.coe x ≤ doubleValue (heightEnd H).bits

theorem Ratpoints.Cli.intervalOf_heightEnd_neg {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {d : Double} {e e0 : ExactEnd} (hd : d.isNaN = false) (he : e.value ≤ doubleValue d.bits) : IntervalOf H (if d.lt (heightEnd H).neg = true then Double.huge.neg else (heightEnd H).neg, d) { inf := -1, q := e0.q } e

The first interval of an upper end without a lower one, [-∞, e] of the command line, and its doubles [-h, d], or [-∞, d] when d lies below -h.

theorem Ratpoints.Cli.intervalOf_heightEnd {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {l : Double} {el e1 : ExactEnd} (hl : l.isNaN = false) (hle : doubleValue l.bits ≤ el.value) : IntervalOf H (l, if (heightEnd H).lt l = true then Double.huge else heightEnd H) el { inf := 1, q := e1.q }

The last interval of a lower end without an upper one, [el, +∞] of the command line, and its doubles [l, h], or [l, +∞] when h lies below l.

theorem Ratpoints.Cli.Intervals.ReadsWF.close {H : ℕ} {iv : Intervals} {e : ExactEnd} {u : Double} (b : Bool) (hw : ReadsWF H iv iv.numInter true) (he : e.inf = -1 ∨ e.inf = 0 ∨ e.inf = 1) (hle : iv.ends[2 * iv.numInter]!.value ≤ e.value) (hI : IntervalOf H (iv.domain[iv.numInter]!.1, u) iv.ends[2 * iv.numInter]! e) : ReadsWF H { lSeen := b, numInter := iv.numInter + 1, domain := iv.domain.set! iv.numInter (iv.domain[iv.numInter]!.1, u), ends := iv.ends.set! (2 * iv.numInter + 1) e } (iv.numInter + 1) false

Closing the pending interval of a reading with the exact upper end e and the upper double u, which hold it as far as the search goes, keeps the invariant, whatever the field lSeen of the result, which the invariant does not read: the step of both Ratpoints.Cli.Intervals.upper and Ratpoints.Cli.Intervals.complete.

theorem Ratpoints.Cli.Intervals.ReadsWF.upper_of_lSeen {H : ℕ} {iv iv' : Intervals} {a : String} (hw : ReadsWF H iv iv.numInter iv.lSeen) (hl : iv.lSeen = true) (h : iv.upper H a = Except.ok iv') : ReadsWF H iv' iv'.numInter iv'.lSeen

theorem Ratpoints.Cli.Intervals.ReadsWF.upper_of_not_lSeen {H : ℕ} {iv iv' : Intervals} {a : String} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) (hw : ReadsWF H iv iv.numInter iv.lSeen) (hl : iv.lSeen = false) (h : iv.upper H a = Except.ok iv') : ReadsWF H iv' iv'.numInter iv'.lSeen

theorem Ratpoints.Cli.Intervals.ReadsWF.upper {H : ℕ} {iv iv' : Intervals} {a : String} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) (hw : ReadsWF H iv iv.numInter iv.lSeen) (h : iv.upper H a = Except.ok iv') : ReadsWF H iv' iv'.numInter iv'.lSeen

theorem Ratpoints.Cli.Intervals.ReadsWF.complete {H : ℕ} {iv : Intervals} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) (hw : ReadsWF H iv iv.numInter iv.lSeen) : ReadsWF H (iv.complete H) (iv.complete H).numInter false

def Ratpoints.Cli.Intervals.LowerMax (iv : Intervals) (n : ℕ) (l : Bool) : Prop

The doubles of the lower ends after the first that the reading iv of the search intervals has read, n complete intervals and a pending lower end when l, are the largest doubles at most their exact ends, as outward from the double that strtod reads makes them.

Equations

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

theorem Ratpoints.Cli.lowerMax_default : { }.LowerMax 0 false

theorem Ratpoints.Cli.Intervals.LowerMax.lower {H : ℕ} {iv iv' : Intervals} {a : String} (hw : ReadsWF H iv iv.numInter iv.lSeen) (hm : iv.LowerMax iv.numInter iv.lSeen) (hlen : a.length < 2 ^ 56) (h : iv.lower a = Except.ok iv') : iv'.LowerMax iv'.numInter iv'.lSeen

theorem Ratpoints.Cli.Intervals.LowerMax.close {iv : Intervals} {e : ExactEnd} {u : Double} (b : Bool) (hs : iv.numInter < iv.domain.size) (hm : iv.LowerMax iv.numInter true) : { lSeen := b, numInter := iv.numInter + 1, domain := iv.domain.set! iv.numInter (iv.domain[iv.numInter]!.1, u), ends := iv.ends.set! (2 * iv.numInter + 1) e }.LowerMax (iv.numInter + 1) false

Closing the pending interval of a reading keeps the doubles of the lower ends the largest doubles at most their exact ends: the lower ends do not change.

theorem Ratpoints.Cli.Intervals.LowerMax.upper {H : ℕ} {iv iv' : Intervals} {a : String} (hw : ReadsWF H iv iv.numInter iv.lSeen) (hm : iv.LowerMax iv.numInter iv.lSeen) (h : iv.upper H a = Except.ok iv') : iv'.LowerMax iv'.numInter iv'.lSeen

theorem Ratpoints.Cli.Intervals.LowerMax.complete {H : ℕ} {iv : Intervals} (hw : ReadsWF H iv iv.numInter iv.lSeen) (hm : iv.LowerMax iv.numInter iv.lSeen) : (iv.complete H).LowerMax (iv.complete H).numInter false

theorem Ratpoints.Cli.checkOptions_store_intervals (s : SieveOptions × Options × Output × Intervals) (o : String) (a : Option String) : (checkOptions.store s o a).2.2.2 = s.2.2.2

theorem Ratpoints.Cli.checkOptions_preserves {H : ℕ} {P : Intervals → Prop} {Q : String → Prop} (hl : ∀ (iv : Intervals) (a : String) (iv' : Intervals), Q a → P iv → iv.lower a = Except.ok iv' → P iv') (hu : ∀ (iv : Intervals) (a : String) (iv' : Intervals), Q a → P iv → iv.upper H a = Except.ok iv' → P iv') {os : List String} {s s' : SieveOptions × Options × Output × Intervals} (hq : ∀ a ∈ os, Q a) (hs : P s.2.2.2) (h : checkOptions H s os = Except.ok s') : P s'.2.2.2

theorem Ratpoints.Cli.reads_of_input_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hi : input args = Except.ok (c, H, s, o, u)) : 1 ≤ H ∧ H < 2 ^ 63 ∧ ∃ (iv : Intervals), Intervals.ReadsWF H iv iv.numInter false ∧ o.domain = List.take iv.numInter iv.domain.toList ∧ u.ends = iv.ends

What a command line that the program accepts gives for its search intervals: the height bound is a positive long, and the reading of the intervals ends with complete intervals that keep the invariant, the search intervals of the options being their doubles and the exact ends of the settings of the output their exact ends.

theorem Ratpoints.Cli.Intervals.ReadsWF.length_take {H : ℕ} {iv : Intervals} (hw : ReadsWF H iv iv.numInter false) : (List.take iv.numInter iv.domain.toList).length = iv.numInter

theorem Ratpoints.Cli.Intervals.ReadsWF.noNaN_take {H : ℕ} {iv : Intervals} (hw : ReadsWF H iv iv.numInter false) : NoNaN (List.take iv.numInter iv.domain.toList)

theorem Ratpoints.Cli.Intervals.ReadsWF.joinsWell_take {H : ℕ} {iv : Intervals} (hw : ReadsWF H iv iv.numInter false) (hm : iv.LowerMax iv.numInter false) : JoinsWell (List.take iv.numInter iv.domain.toList)

theorem Ratpoints.Cli.Intervals.ReadsWF.intervalsWF_joinIntervals {H : ℕ} {iv : Intervals} (hw : ReadsWF H iv iv.numInter false) (hm : iv.LowerMax iv.numInter false) : IntervalsWF (domainBits (joinIntervals (List.take iv.numInter iv.domain.toList)).run)

theorem Ratpoints.Cli.inRegion_iff_of_input_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hi : input args = Except.ok (c, H, s, o, u)) (a b : ℤ) : (inRegion a b u.ends o.domain.length).run = true ↔ InExactRegion u.ends o.domain.length (↑a / ↑b)

The test of the callback, the binary search of in_region over the exact ends of the search intervals of a command line that the program accepts, which are increasing and disjoint by the checks of error 7, is the membership of a / b in one of them.

theorem Ratpoints.Cli.inIntervals_joinIntervals_of_inExactRegion {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hi : input args = Except.ok (c, H, s, o, u)) {x : ℚ} (hx : |x| ≤ ↑H) (hex : InExactRegion u.ends o.domain.length x) : InIntervals (domainValues (joinIntervals o.domain).run) x

The search intervals that the program gives the library hold the exact search region of its command line as far as the search goes, for |x| ≤ H: their ends are the doubles outward of the exact ends (Ratpoints.Cli.outward), or ∓h for a missing first lower or last upper end, which lie beyond the height bound.

theorem Ratpoints.Cli.keeps_ofOutput_iff (u : Output) (o : Options) (p : ℤ × ℤ × ℤ) : (Data.ofOutput u o).keeps p = true ↔ (u.pointsAtInfty = true ∨ p.2.2 ≠ 0) ∧ (p.2.2 = 0 ∨ o.domain = [] ∨ (inRegion p.1 p.2.2 u.ends o.domain.length).run = true)

theorem Ratpoints.Cli.intervalsWF_joinIntervals_of_input_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hlen : ∀ a ∈ args, a.length < 2 ^ 56) (hi : input args = Except.ok (c, H, s, o, u)) : IntervalsWF (domainBits (joinIntervals o.domain).run)

The search intervals that the program gives the library for a command line that it accepts, whose words have fewer than 2 ^ 56 characters, are well formed, so that the library never refuses them (error 9 is unreachable): the doubles of the lower ends after the first are the largest doubles at most the exact ends, which increase, so that join_intervals joins the intervals whose doubles meet into intervals that are increasing and strictly apart. Without the bound on the length, a word of LONG_MAX / 20 digits could make scan_end stop taking the digits of its exponent.

theorem Ratpoints.Cli.inRegion_joinIntervals_iff {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} (hi : input args = Except.ok (c, H, s, o, u)) {p : ℤ × ℤ × ℤ} (hp : IsPoint c H p) (hx : p.2.2 = 0 ∨ o.domain = [] ∨ InExactRegion u.ends o.domain.length (↑p.1 / ↑p.2.2)) : InRegion (domainValues (joinIntervals o.domain).run) o.bLow o.bHigh p ↔ InRegion [] o.bLow o.bHigh p

For a point of height at most H of a command line that the program accepts, the search region of the search on the joined intervals is that of the range of the denominators, given that x / z lies in the exact search region of the command line when there is one.

theorem Ratpoints.Cli.mem_filter_keeps_iff_of_input_eq_ok {args : List String} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {u : Output} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (hi : input args = Except.ok (c, H, s, o, u)) (hc : o.noCheck = false) (hL : findPoints c H { numPrimes := s.numPrimes, sp1 := s.sp1, sp2 := s.sp2, survivorsPerWord := s.survivorsPerWord, sp2Extra := s.sp2Extra, sp2U0 := s.sp2U0, costTable := s.costTable, adapt := s.adapt, sp3Extra := s.sp3Extra, sp3PerDenom := s.sp3PerDenom, checkCost := s.checkCost, maxForbidden := s.maxForbidden, jacobi := s.jacobi } { reverse := o.reverse, sturm := o.sturm, noCheck := o.noCheck, noY := o.noY, domain := (joinIntervals o.domain).run, bLow := o.bLow, bHigh := o.bHigh } = Except.ok L) {p : ℤ × ℤ × ℤ} : p ∈ List.filter (Data.ofOutput u o).keeps L ↔ IsPoint c H p ∧ (o.noY = true → 0 ≤ p.2.1) ∧ (u.pointsAtInfty = true ∨ p.2.2 ≠ 0) ∧ InRegion [] o.bLow o.bHigh p ∧ (p.2.2 = 0 ∨ o.domain = [] ∨ InExactRegion u.ends o.domain.length (↑p.1 / ↑p.2.2))

Assuming Sturm's theorem when the Sturm step is on (Ratpoints.SturmTheorem, which a command line with -s does not need), without -x, the points of the list of Ratpoints.findPoints on the joined search intervals of a command line that the callback of the program keeps (Ratpoints.Cli.Data.keeps), which it prints under -q (Ratpoints.Cli.run_eq_of_findPoints_eq_ok), are exactly the points of height at most H in the exact search region of the command line, those with y ≥ 0 under -y: the points at infinity unless -i, and the affine points with the denominator in the range of -dl and -du and x / z in one of the intervals of -l and -u when there are some.