The closure library, part II: loops

The generic reasoning principle for loop (Eval.loop_of_invariant: an invariant, a strictly decreasing measure and a uniform bound on the body's cost give a run of the loop with cost ≤ (μ + 1) · (B + 1)), and the list and unary-numeral primitives of the library proved by direct induction: reversal onto an accumulator (revOntoProg, revProg) and length in unary (lenProg). Lists are cons-chains (Data.list); unary numerals are lists of nils (Data.ofNat).

Conventions: every program is closed and takes its input in variable 0; a loop's state is the input itself or a pair assembled by let_ in front of the loop; the body stops with cons nil result and continues with cons (cons nil nil) state'. Costs are stated as bounds of the form (iterations + 1) · (S + c) where S is any number dominating the sizes involved, so that the bound is one atom for omega throughout an induction.

Lists as data

def MIPRE.Cost.Data.list : List Data → Data

Lists of data as cons-chains.

Equations

• MIPRE.Cost.Data.list = MIPRE.Cost.Data.ofList id

@[simp]

theorem MIPRE.Cost.Data.list_nil : list [] = nil

@[simp]

theorem MIPRE.Cost.Data.list_cons (a : Data) (l : List Data) : list (a :: l) = a.cons (list l)

theorem MIPRE.Cost.Data.ofList_eq_list {α : Type u_1} (f : α → Data) (l : List α) : ofList f l = list (List.map f l)

@[simp]

theorem MIPRE.Cost.Data.size_list_cons (a : Data) (l : List Data) : (list (a :: l)).size = a.size + (list l).size + 1

theorem MIPRE.Cost.Data.length_le_size_list (l : List Data) : l.length ≤ (list l).size

The loop principle

theorem MIPRE.Cost.Eval.loop_of_invariant {b : Prog} (hb : Prog.WellScoped 1 b) (env : Env) (I : Data → Prop) (μ : Data → ℕ) (Q : Data → Prop) (B : ℕ) (hbody : ∀ (s : Data), I s → (∃ (r : Data), ∃ t ≤ B, Eval [s] b (Data.nil.cons r) t ∧ Q r) ∨ ∃ (x : Data) (y : Data) (s' : Data), ∃ t ≤ B, Eval [s] b ((x.cons y).cons s') t ∧ I s' ∧ μ s' < μ s) (s : Data) : I s → ∃ (r : Data), ∃ t ≤ (μ s + 1) * (B + 1), Q r ∧ Eval (s :: env) b.loop r t

Loop with an invariant and a measure. If from every state s satisfying I the body either stops (with a result satisfying Q) or continues to a state s' satisfying I with μ s' < μ s, at cost at most B in both cases, then loop b from any state satisfying I stops with a result satisfying Q, at cost at most (μ s + 1) · (B + 1).

Reversal onto an accumulator

def MIPRE.Cost.Prog.revOntoBody : Prog

Body of revOntoProg: on state cons xs acc, stop with acc if xs is empty, otherwise move the head of xs onto acc.

Equations

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

def MIPRE.Cost.Prog.revOntoProg : Prog

revOntoProg on cons xs acc computes reverse xs ++ acc.

Equations

• MIPRE.Cost.Prog.revOntoProg = MIPRE.Cost.Prog.revOntoBody.loop

theorem MIPRE.Cost.Prog.revOntoBody_wellScoped : WellScoped 1 revOntoBody

theorem MIPRE.Cost.Prog.revOntoProg_wellScoped : WellScoped 1 revOntoProg

theorem MIPRE.Cost.Prog.revOntoBody_step (h : Data) (l acc : List Data) : Eval [(Data.list (h :: l)).cons (Data.list acc)] revOntoBody ((Data.nil.cons Data.nil).cons ((Data.list l).cons (Data.list (h :: acc)))) ((Data.list l).size + h.size + (Data.list acc).size + 11)

One iteration of revOntoBody on a non-empty list.

theorem MIPRE.Cost.Prog.revOntoBody_stop (acc : List Data) : Eval [(Data.list []).cons (Data.list acc)] revOntoBody (Data.nil.cons (Data.list acc)) ((Data.list acc).size + 5)

The stopping iteration of revOntoBody on the empty list.

theorem MIPRE.Cost.Prog.revOntoProg_runs (l acc : List Data) (env : Env) (S : ℕ) (hS : (Data.list l).size + (Data.list acc).size ≤ S) : ∃ t ≤ (l.length + 1) * (S + 12), Eval ((Data.list l).cons (Data.list acc) :: env) revOntoProg (Data.list (l.reverse ++ acc)) t

revOntoProg reverses xs onto acc, in time (|xs| + 1) · (S + 12) for any S dominating the total size of the two lists.

def MIPRE.Cost.Prog.revProg : Prog

Reversal of a list: revProg on xs computes reverse xs.

Equations

• MIPRE.Cost.Prog.revProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ MIPRE.Cost.Prog.revOntoProg

theorem MIPRE.Cost.Prog.revProg_wellScoped : WellScoped 1 revProg

theorem MIPRE.Cost.Prog.revProg_runs (l : List Data) : ∃ t ≤ (l.length + 1 + 1) * ((Data.list l).size + 1 + 12), revProg.Runs (Data.list l) (Data.list l.reverse) t

Length in unary

def MIPRE.Cost.Prog.lenBody : Prog

Body of lenProg: on state cons xs acc, stop with acc if xs is empty, otherwise drop the head of xs and prepend a nil to acc. Running it to completion prepends |xs| copies of nil to acc: with acc = nil this is the length in unary, with acc a unary numeral it is addition, with acc = [true] it is the bit string of 2 ^ |xs|.

Equations

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

theorem MIPRE.Cost.Prog.lenBody_wellScoped : WellScoped 1 lenBody

theorem MIPRE.Cost.Prog.lenBody_step (h : Data) (l acc : List Data) : Eval [(Data.list (h :: l)).cons (Data.list acc)] lenBody ((Data.nil.cons Data.nil).cons ((Data.list l).cons (Data.list (Data.nil :: acc)))) ((Data.list l).size + (Data.list acc).size + 11)

theorem MIPRE.Cost.Prog.lenBody_stop (acc : List Data) : Eval [(Data.list []).cons (Data.list acc)] lenBody (Data.nil.cons (Data.list acc)) ((Data.list acc).size + 5)

theorem MIPRE.Cost.Prog.lenLoop_runs (l acc : List Data) (env : Env) (S : ℕ) (hS : (Data.list l).size + (Data.list acc).size + 2 * l.length ≤ S) : ∃ t ≤ (l.length + 1) * (S + 13), Eval ((Data.list l).cons (Data.list acc) :: env) lenBody.loop (Data.list (List.replicate l.length Data.nil ++ acc)) t

The loop of lenBody prepends |xs| copies of nil to acc, in time (|xs| + 1) · (S + 13) for any S dominating size xs + size acc + 2 |xs|.

def MIPRE.Cost.Prog.lenProg : Prog

Length of a list in unary: lenProg on xs computes ofNat |xs|.

Equations

• MIPRE.Cost.Prog.lenProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ MIPRE.Cost.Prog.lenBody.loop

theorem MIPRE.Cost.Prog.lenProg_wellScoped : WellScoped 1 lenProg

theorem MIPRE.Cost.Data.ofNat_eq_list_replicate (n : ℕ) : ofNat n = list (List.replicate n nil)

theorem MIPRE.Cost.Prog.lenProg_runs (l : List Data) : ∃ t ≤ (l.length + 1 + 1) * ((Data.list l).size + 1 + 2 * l.length + 13), lenProg.Runs (Data.list l) (Data.ofNat l.length) t