The closure library, part I: calls, projections, pairing, branching

Program-layer combinators on Prog with their Eval lemmas, and the corresponding PolyTimeFun combinators (const, pair, fst, snd, ite). Two conventions keep composition free of de Bruijn bookkeeping:

• a closed program q is called on the value of variable i by let_ (var i) q (Prog.callVar): the callee sees its input at variable 0 and, being well-scoped, ignores the rest of the environment (Eval.append_of_wellScoped);
• branches re-bind the original input by copying it (PolyTimeFun.ite), rather than shifting indices.

Costs are exact at the program layer and packaged as polynomials at the function layer (planning/compression-track.md, K2).

Program layer

theorem MIPRE.Cost.Eval.cast_cost {env : Env} {p : Prog} {r : Data} {t t' : ℕ} (h : Eval env p r t) (e : t = t') : Eval env p r t'

Transport a run along an equation between costs.

theorem MIPRE.Cost.Eval.var_of_get {env : Env} {i : ℕ} {v : Data} (h : env.get i = v) : Eval env (Prog.var i) v (v.size + 1)

Reading a variable whose value is known.

def MIPRE.Cost.Prog.callVar (i : ℕ) (q : Prog) : Prog

Call the closed program q on the value of variable i.

Equations

• MIPRE.Cost.Prog.callVar i q = (MIPRE.Cost.Prog.var i).let_ q

def MIPRE.Cost.Prog.fstProg : Prog

First component of the input (variable 0).

Equations

• MIPRE.Cost.Prog.fstProg = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.var 0)

def MIPRE.Cost.Prog.sndProg : Prog

Second component of the input (variable 0).

Equations

• MIPRE.Cost.Prog.sndProg = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.var 1)

theorem MIPRE.Cost.Prog.callVar_wellScoped {n i : ℕ} (hi : i < n) {q : Prog} (hq : WellScoped 1 q) : WellScoped n (callVar i q)

theorem MIPRE.Cost.Prog.fstProg_wellScoped : WellScoped 1 fstProg

theorem MIPRE.Cost.Prog.sndProg_wellScoped : WellScoped 1 sndProg

theorem MIPRE.Cost.Prog.callVar_eval {env : Env} {i : ℕ} {q : Prog} (hq : WellScoped 1 q) {v r : Data} {t : ℕ} (hv : env.get i = v) (h : Eval [v] q r t) : Eval env (callVar i q) r (v.size + 1 + t + 1)

Calling q on variable i: copy the value, then run q (its input is variable 0; the rest of the environment is inert).

theorem MIPRE.Cost.Prog.fstProg_runs (a b : Data) : fstProg.Runs (a.cons b) a (a.size + 1 + 1)

theorem MIPRE.Cost.Prog.sndProg_runs (a b : Data) : sndProg.Runs (a.cons b) b (b.size + 1 + 1)

Function layer

noncomputable def MIPRE.Cost.PolyTimeFun.const {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (b : β) : PolyTimeFun α β

The constant function, in constant time.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.const_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (b : β) (a : α) : (const b).toFun a = b

noncomputable def MIPRE.Cost.PolyTimeFun.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun α β) (G : PolyTimeFun α γ) : PolyTimeFun α (β × γ)

Pairing.

Equations

• F.pair G = { toFun := fun (a : α) => (F.toFun a, G.toFun a), code := F.code.cons G.code, closed := ⋯, timeBound := F.timeBound + G.timeBound + 1, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.pair_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun α β) (G : PolyTimeFun α γ) (a : α) : (F.pair G).toFun a = (F.toFun a, G.toFun a)

noncomputable def MIPRE.Cost.PolyTimeFun.fst {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] : PolyTimeFun (α × β) α

First projection.

Equations

• MIPRE.Cost.PolyTimeFun.fst = { toFun := Prod.fst, code := MIPRE.Cost.Prog.fstProg, closed := MIPRE.Cost.Prog.fstProg_wellScoped, timeBound := Polynomial.X + Polynomial.C 2, computes := ⋯ }

noncomputable def MIPRE.Cost.PolyTimeFun.snd {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] : PolyTimeFun (α × β) β

Second projection.

Equations

• MIPRE.Cost.PolyTimeFun.snd = { toFun := Prod.snd, code := MIPRE.Cost.Prog.sndProg, closed := MIPRE.Cost.Prog.sndProg_wellScoped, timeBound := Polynomial.X + Polynomial.C 2, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.fst_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (p : α × β) : fst.toFun p = p.1

@[simp]

theorem MIPRE.Cost.PolyTimeFun.snd_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (p : α × β) : snd.toFun p = p.2

noncomputable def MIPRE.Cost.PolyTimeFun.ite {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (c : PolyTimeFun α Bool) (F G : PolyTimeFun α β) : PolyTimeFun α β

Branching on a boolean: ite c F G a = if c a then F a else G a. The condition is bound as variable 0; the nil (false) branch calls G on the original input (variable 1), the cons (true) branch calls F on it (variable 3, after elim bound the two nil components of encode true).

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.ite_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (c : PolyTimeFun α Bool) (F G : PolyTimeFun α β) (a : α) : (c.ite F G).toFun a = if c.toFun a = true then F.toFun a else G.toFun a