Programs as readers of a shared input

A program built by composition out of comp, pair, fst and snd is written point-free, and a point-free term for a formula of forty conjuncts is unreadable. This file gives the applicative reading instead: a PolyTimeFun ι α is a reader of the shared input ι, and ap₁, ap₂, ap₃ and listOf apply a program to readers. In that style a program transcribes its mathematical definition line for line, and its toFun is definitionally the function it transcribes, so the congr that names it closes by rfl.

Also here, because they are the list operations the describer's programs need and they are generic: take, tail, headD and nthD (planning/succinct-cook-levin.md, S3).

Applying a program to readers

noncomputable def MIPRE.Cost.PolyTimeFun.ap₁ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (f : PolyTimeFun ι α) : PolyTimeFun ι β

Apply a one-argument program to a reader.

Equations

• F.ap₁ f = F.comp f

@[simp]

theorem MIPRE.Cost.PolyTimeFun.ap₁_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (f : PolyTimeFun ι α) (i : ι) : (F.ap₁ f).toFun i = F.toFun (f.toFun i)

noncomputable def MIPRE.Cost.PolyTimeFun.ap₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun (α × β) γ) (f : PolyTimeFun ι α) (g : PolyTimeFun ι β) : PolyTimeFun ι γ

Apply a two-argument program to two readers.

Equations

• F.ap₂ f g = F.comp (f.pair g)

@[simp]

theorem MIPRE.Cost.PolyTimeFun.ap₂_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun (α × β) γ) (f : PolyTimeFun ι α) (g : PolyTimeFun ι β) (i : ι) : (F.ap₂ f g).toFun i = F.toFun (f.toFun i, g.toFun i)

noncomputable def MIPRE.Cost.PolyTimeFun.ap₃ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] [SizedEncoding δ] (F : PolyTimeFun (α × β × γ) δ) (f : PolyTimeFun ι α) (g : PolyTimeFun ι β) (h : PolyTimeFun ι γ) : PolyTimeFun ι δ

Apply a three-argument program to three readers.

Equations

• F.ap₃ f g h = F.comp (f.pair (g.pair h))

@[simp]

theorem MIPRE.Cost.PolyTimeFun.ap₃_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] [SizedEncoding δ] (F : PolyTimeFun (α × β × γ) δ) (f : PolyTimeFun ι α) (g : PolyTimeFun ι β) (h : PolyTimeFun ι γ) (i : ι) : (F.ap₃ f g h).toFun i = F.toFun (f.toFun i, g.toFun i, h.toFun i)

noncomputable def MIPRE.Cost.PolyTimeFun.ap₂' {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun (α × β) γ) (f : PolyTimeFun ι α) : PolyTimeFun (ι × β) γ

A two-argument program with its left argument curried away: the reader f of the shared input supplies it.

Equations

• F.ap₂' f = F.comp ((f.comp MIPRE.Cost.PolyTimeFun.fst).pair MIPRE.Cost.PolyTimeFun.snd)

@[simp]

theorem MIPRE.Cost.PolyTimeFun.ap₂'_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SizedEncoding ι] [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun (α × β) γ) (f : PolyTimeFun ι α) (p : ι × β) : (F.ap₂' f).toFun p = F.toFun (f.toFun p.1, p.2)

noncomputable def MIPRE.Cost.PolyTimeFun.listOf {ι : Type u_1} {α : Type u_2} [SizedEncoding ι] [SizedEncoding α] : List (PolyTimeFun ι α) → PolyTimeFun ι (List α)

A list of readers as a reader of the list of their values.

Equations

• MIPRE.Cost.PolyTimeFun.listOf [] = MIPRE.Cost.PolyTimeFun.const []
• MIPRE.Cost.PolyTimeFun.listOf (f :: fs) = f.cons (MIPRE.Cost.PolyTimeFun.listOf fs)

@[simp]

theorem MIPRE.Cost.PolyTimeFun.listOf_apply {ι : Type u_1} {α : Type u_2} [SizedEncoding ι] [SizedEncoding α] (fs : List (PolyTimeFun ι α)) (i : ι) : (listOf fs).toFun i = List.map (fun (f : PolyTimeFun ι α) => f.toFun i) fs

Prefixes, tails and heads

theorem MIPRE.Cost.PolyTimeFun.map_fst_zip {α : Type u_2} (l : List α) (u : Unary) : List.map Prod.fst (l.zip u) = List.take (List.length u) l

noncomputable def MIPRE.Cost.PolyTimeFun.take {α : Type u_2} [SizedEncoding α] : PolyTimeFun (List α × Unary) (List α)

Taking a prefix, the length in unary.

Equations

• MIPRE.Cost.PolyTimeFun.take = (MIPRE.Cost.PolyTimeFun.fst.map.comp MIPRE.Cost.PolyTimeFun.zip).congr (fun (p : List α × MIPRE.Cost.Unary) => List.take (List.length p.2) p.1) ⋯

@[simp]

theorem MIPRE.Cost.PolyTimeFun.take_apply {α : Type u_2} [SizedEncoding α] (p : List α × Unary) : take.toFun p = List.take (List.length p.2) p.1

noncomputable def MIPRE.Cost.PolyTimeFun.tail {α : Type u_2} [SizedEncoding α] : PolyTimeFun (List α) (List α)

The tail of a list.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.tail_apply {α : Type u_2} [SizedEncoding α] (l : List α) : tail.toFun l = l.tail

noncomputable def MIPRE.Cost.PolyTimeFun.headD {α : Type u_2} [SizedEncoding α] (d : α) : PolyTimeFun (List α) α

The head of a list, or a default.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.headD_apply {α : Type u_2} [SizedEncoding α] (d : α) (l : List α) : (headD d).toFun l = l.headD d

theorem MIPRE.Cost.PolyTimeFun.esize_tail_le {α : Type u_2} [SizedEncoding α] (l : List α) : esize l.tail ≤ esize l

Dropping a prefix, the length in unary: iterated tail.

noncomputable def MIPRE.Cost.PolyTimeFun.tailStep {α : Type u_2} [SizedEncoding α] : PolyTimeFun (List α × Unit) (List α)

Equations

• MIPRE.Cost.PolyTimeFun.tailStep = MIPRE.Cost.PolyTimeFun.tail.comp MIPRE.Cost.PolyTimeFun.fst

@[simp]

theorem MIPRE.Cost.PolyTimeFun.tailStep_apply {α : Type u_2} [SizedEncoding α] (p : List α × Unit) : tailStep.toFun p = p.1.tail

theorem MIPRE.Cost.PolyTimeFun.esize_foldl_tailStep {α : Type u_2} [SizedEncoding α] (pre : Unary) (s : List α) : esize (List.foldl tailStep.step s pre) ≤ esize s

theorem MIPRE.Cost.PolyTimeFun.tailStep_bounded {α : Type u_2} [SizedEncoding α] : tailStep.FoldBounded Polynomial.X

theorem MIPRE.Cost.PolyTimeFun.foldl_tailStep {α : Type u_2} [SizedEncoding α] (u : Unary) (l : List α) : List.foldl tailStep.step l u = List.drop (List.length u) l

noncomputable def MIPRE.Cost.PolyTimeFun.drop {α : Type u_2} [SizedEncoding α] : PolyTimeFun (List α × Unary) (List α)

Dropping a prefix, the length in unary.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.drop_apply {α : Type u_2} [SizedEncoding α] (p : List α × Unary) : drop.toFun p = List.drop (List.length p.2) p.1

noncomputable def MIPRE.Cost.PolyTimeFun.nthD {α : Type u_2} [SizedEncoding α] (d : α) : ℕ → PolyTimeFun (List α) α

The k-th entry of a list, or a default.

Equations

• MIPRE.Cost.PolyTimeFun.nthD d 0 = MIPRE.Cost.PolyTimeFun.headD d
• MIPRE.Cost.PolyTimeFun.nthD d k.succ = (MIPRE.Cost.PolyTimeFun.nthD d k).comp MIPRE.Cost.PolyTimeFun.tail

@[simp]

theorem MIPRE.Cost.PolyTimeFun.nthD_apply {α : Type u_2} [SizedEncoding α] (d : α) (k : ℕ) (l : List α) : (nthD d k).toFun l = l.getD k d