Documentation

Ratpoints.Proof.Delivery

The delivery of a list of points #

The reference of the delivery of a search, Ratpoints.Delivery.deliver, the fold over a list of points that calls the callback for each of them while the flag of the stop is clear: its unfolding on the empty list, on a point in front and on a concatenation; a delivery whose flag is set is left as it is, whatever the list, so that the delivery of a list is that of a prefix of it once the flag is set after the prefix; with the appending callback Ratpoints.appendPoint the array of the data grows by the list and the count by its length; and in general the calls made are those of the points of a prefix of the list, before each of which the flag is clear, the whole list or the prefix up to and including the first point whose call sets the flag.

Main statements #

Implementation notes #

The file uses Lean core only, so that the contracts of the sieve in the files without Mathlib (Ratpoints.Proof.Stages, Ratpoints.Proof.Scan, Ratpoints.Proof.SiftBits, Ratpoints.Proof.Sift) can state what they deliver with it.

The unfolding #

source
@[simp]
theorem Ratpoints.Delivery.deliver_nil {σ : Type} (process : Int → Int → Int → σ → Answer σ) (r : Delivery σ) :
deliver process r [] = r
source
theorem Ratpoints.Delivery.deliver_cons {σ : Type} (process : Int → Int → Int → σ → Answer σ) (r : Delivery σ) (p : Int × Int × Int) (L : List (Int × Int × Int)) :
deliver process r (p :: L) = deliver process (if r.quit = true then r else call process r p.fst p.snd.snd p.snd.fst) L
source
theorem Ratpoints.Delivery.deliver_append {σ : Type} (process : Int → Int → Int → σ → Answer σ) (r : Delivery σ) (L₁ L₂ : List (Int × Int × Int)) :
deliver process r (L₁ ++ L₂) = deliver process (deliver process r L₁) L₂
source
theorem Ratpoints.Delivery.deliver_cons_of_quit_eq_false {σ : Type} (process : Int → Int → Int → σ → Answer σ) {r : Delivery σ} (h : r.quit = false) (p : Int × Int × Int) (L : List (Int × Int × Int)) :
deliver process r (p :: L) = deliver process (call process r p.fst p.snd.snd p.snd.fst) L
source
theorem Ratpoints.Delivery.deliver_singleton_of_quit_eq_false {σ : Type} (process : Int → Int → Int → σ → Answer σ) {r : Delivery σ} (h : r.quit = false) (p : Int × Int × Int) :
deliver process r [p] = call process r p.fst p.snd.snd p.snd.fst

The stop #

source
@[simp]
theorem Ratpoints.Delivery.deliver_of_quit {σ : Type} (process : Int → Int → Int → σ → Answer σ) {r : Delivery σ} (h : r.quit = true) (L : List (Int × Int × Int)) :
deliver process r L = r

A delivery whose flag is set is left as it is: the callback is not called again.

source
theorem Ratpoints.Delivery.deliver_append_of_quit {σ : Type} {process : Int → Int → Int → σ → Answer σ} {r : Delivery σ} {L₁ : List (Int × Int × Int)} (h : (deliver process r L₁).quit = true) (L₂ : List (Int × Int × Int)) :
deliver process r (L₁ ++ L₂) = deliver process r L₁

Once a call has set the flag, the points that follow are passed over.

source
theorem Ratpoints.Delivery.deliver_eq_of_prefix {σ : Type} {process : Int → Int → Int → σ → Answer σ} {r : Delivery σ} {M L : List (Int × Int × Int)} (h : M <+: L) (hq : (deliver process r M).quit = true) :
deliver process r L = deliver process r M

Once a call has set the flag, the delivery of a list is that of a prefix of it after which the flag is set: the points that follow are passed over.

source
theorem Ratpoints.Delivery.deliver_flatMap_eq_of_prefix {σ : Type} {process : Int → Int → Int → σ → Answer σ} {α : Type} {r : Delivery σ} {l₁ l₂ : List α} {f : α → List (Int × Int × Int)} (h : l₁ <+: l₂) (hq : (deliver process r (List.flatMap f l₁)).quit = true) :
deliver process r (List.flatMap f l₂) = deliver process r (List.flatMap f l₁)

Ratpoints.Delivery.deliver_eq_of_prefix for the concatenations of the lists f a of the elements a of a prefix l₁ of l₂.

source
theorem Ratpoints.Delivery.ite_quit_eq_deliver_append {σ : Type} {process : Int → Int → Int → σ → Answer σ} {r r₁ r₂ : Delivery σ} {L₁ L₂ : List (Int × Int × Int)} (h₁ : r₁ = deliver process r L₁) (h₂ : r₁.quit = false → r₂ = deliver process r₁ L₂) :
(if r₁.quit = true then r₁ else r₂) = deliver process r (L₁ ++ L₂)

The delivery r₁ of the points of L₁, followed, unless the callback has stopped the search, by a delivery r₂ of the points of L₂ from r₁, is the delivery of the points of L₁ ++ L₂.

The appending callback #

source
@[simp]
theorem Ratpoints.Delivery.deliver_appendPoint (arr : Array (Int × Int × Int)) (n : Int) (L : List (Int × Int × Int)) :
deliver appendPoint { info := arr, total := n, quit := false } L = { info := arr ++ L.toArray, total := n + ↑L.length, quit := false }

The calls made #

source
theorem Ratpoints.Delivery.exists_prefix_deliver_eq {σ : Type} (process : Int → Int → Int → σ → Answer σ) (r : Delivery σ) (L : List (Int × Int × Int)) :
∃ (M : List (Int × Int × Int)), M <+: L ∧ deliver process r L = deliver process r M ∧ (∀ (m : Nat), m < M.length → (deliver process r (List.take m M)).quit = false) ∧ (M ≠ L → (deliver process r M).quit = true)

The calls that the delivery of L makes are those of the points of a prefix M of L: the flag is clear before each point of M, so that each gets its call, and unless M is all of L, the flag is set after them, by the call of the last point of M, or at the start when M is empty.