The layout arithmetic as programs

The widths and offsets of the index layout (Layout.lean) as programs. Two conventions make them cheap:

• widths and offsets are unary. W e, mOf e G, the field offsets: all are affine in e with small coefficients, so in unary they are append and iterated append, and no arithmetic program is needed. e itself must be unary in any case — the formulas are of size polynomial in e, so a binary e would make the output exponential in the input.
• a constant of a field is a resize of a bit string. resize w bs keeps the low w bits of bs, padding with false, and resize_eq_nbits identifies it with nbits w k for any bs whose bits are those of k. So nbits w (2 * T) is a resize of false :: T.bits and nbits w (T + 3) one of incBits (incBits (incBits T.bits)), with no multiplication or addition on numbers (planning/succinct-cook-levin.md, S3).

Unary arithmetic

noncomputable def MIPRE.TM.CookLevin.Desc.addU : Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary

Unary addition.

Equations

• MIPRE.TM.CookLevin.Desc.addU = MIPRE.Cost.PolyTimeFun.append

@[simp]

theorem MIPRE.TM.CookLevin.Desc.addU_apply (p : Cost.Unary × Cost.Unary) : addU.toFun p = p.1 ++ p.2

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_addU (p : Cost.Unary × Cost.Unary) : List.length (addU.toFun p) = List.length p.1 + List.length p.2

noncomputable def MIPRE.TM.CookLevin.Desc.nsmulU : ℕ → Cost.PolyTimeFun Cost.Unary Cost.Unary

Unary multiplication by a constant.

Equations

• MIPRE.TM.CookLevin.Desc.nsmulU 0 = MIPRE.Cost.PolyTimeFun.const []
• MIPRE.TM.CookLevin.Desc.nsmulU k.succ = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.TM.CookLevin.Desc.nsmulU k) (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_nsmulU (k : ℕ) (u : Cost.Unary) : List.length ((nsmulU k).toFun u) = k * List.length u

Resizing a bit string

def MIPRE.TM.CookLevin.Desc.resize (w : ℕ) (bs : Cost.BitStr) : Cost.BitStr

The low w bits of a bit string, padded with false to the width w.

Equations

• MIPRE.TM.CookLevin.Desc.resize w bs = List.take w (bs ++ List.replicate w false)

theorem MIPRE.TM.CookLevin.Desc.length_resize (w : ℕ) (bs : Cost.BitStr) : List.length (resize w bs) = w

theorem MIPRE.TM.CookLevin.Desc.getD_append_replicate (bs : Cost.BitStr) (w i : ℕ) : List.getD (bs ++ List.replicate w false) i false = List.getD bs i false

theorem MIPRE.TM.CookLevin.Desc.getD_resize {w : ℕ} (bs : Cost.BitStr) {i : ℕ} (hi : i < w) : List.getD (resize w bs) i false = List.getD bs i false

theorem MIPRE.TM.CookLevin.Desc.resize_eq_nbits (w : ℕ) (bs : Cost.BitStr) (k : ℕ) (h : ∀ (i : ℕ), List.getD bs i false = k.testBit i) : resize w bs = nbits w k

A constant of a width is a resize: if the bits of bs are those of k, then the low w bits of bs are the w-bit constant k.

The bit strings of the numbers the describer needs

theorem MIPRE.TM.CookLevin.Desc.getD_bits (k i : ℕ) : k.bits.getD i false = k.testBit i

theorem MIPRE.TM.CookLevin.Desc.getD_false_cons (bs : Cost.BitStr) (k : ℕ) (h : ∀ (i : ℕ), List.getD bs i false = k.testBit i) (i : ℕ) : (false :: bs).getD i false = (2 * k).testBit i

Powers of two

Resizing, as a program

noncomputable def MIPRE.TM.CookLevin.Desc.resizeP : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr

resize, the width in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.resizeP_apply (p : Cost.Unary × Cost.BitStr) : resizeP.toFun p = resize (List.length p.1) p.2

noncomputable def MIPRE.TM.CookLevin.Desc.dblP : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Doubling a bit string: a false in front.

Equations

• MIPRE.TM.CookLevin.Desc.dblP = (MIPRE.Cost.PolyTimeFun.const false).cons (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.BitStr)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dblP_apply (bs : Cost.BitStr) : dblP.toFun bs = false :: bs

noncomputable def MIPRE.TM.CookLevin.Desc.pow2P : Cost.PolyTimeFun Cost.Unary ℕ

2 ^ e, from e in unary: its bit string is e zeros and a one.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.pow2P_apply (u : Cost.Unary) : pow2P.toFun u = 2 ^ List.length u

noncomputable def MIPRE.TM.CookLevin.Desc.incN : ℕ → Cost.PolyTimeFun ℕ ℕ

Adding a constant to a number.

Equations

• MIPRE.TM.CookLevin.Desc.incN 0 = MIPRE.Cost.PolyTimeFun.id ℕ
• MIPRE.TM.CookLevin.Desc.incN k.succ = MIPRE.Cost.PolyTimeFun.inc.comp (MIPRE.TM.CookLevin.Desc.incN k)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.incN_apply (k n : ℕ) : (incN k).toFun n = n + k

Readers of the layout

noncomputable def MIPRE.TM.CookLevin.Desc.nbitsR {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (bs : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι Cost.BitStr

The constant k on w bits, read off a width in unary and the bits of k.

Equations

• MIPRE.TM.CookLevin.Desc.nbitsR w bs = MIPRE.TM.CookLevin.Desc.resizeP.ap₂ w bs

theorem MIPRE.TM.CookLevin.Desc.nbitsR_apply {ι : Type u_1} [Cost.SizedEncoding ι] {w : Cost.PolyTimeFun ι Cost.Unary} {bs : Cost.PolyTimeFun ι Cost.BitStr} {i : ι} (k : ℕ) (h : ∀ (j : ℕ), List.getD (bs.toFun i) j false = k.testBit j) : (nbitsR w bs).toFun i = nbits (List.length (w.toFun i)) k

noncomputable def MIPRE.TM.CookLevin.Desc.cstR {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (bs : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι (List SAT.Fml)

The formulas of the constant k on w bits.

Equations

• MIPRE.TM.CookLevin.Desc.cstR w bs = MIPRE.SAT.constBitsP.ap₁ (MIPRE.TM.CookLevin.Desc.nbitsR w bs)

theorem MIPRE.TM.CookLevin.Desc.cstR_apply {ι : Type u_1} [Cost.SizedEncoding ι] {w : Cost.PolyTimeFun ι Cost.Unary} {bs : Cost.PolyTimeFun ι Cost.BitStr} {i : ι} (k : ℕ) (h : ∀ (j : ℕ), List.getD (bs.toFun i) j false = k.testBit j) : (cstR w bs).toFun i = cst (List.length (w.toFun i)) k

theorem MIPRE.TM.CookLevin.Desc.nbitsR_num {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (kR : Cost.PolyTimeFun ι ℕ) (i : ι) : (nbitsR w (Cost.PolyTimeFun.natBits.ap₁ kR)).toFun i = nbits (List.length (w.toFun i)) (kR.toFun i)

The constant read off a width in unary and a reader of the number itself.

noncomputable def MIPRE.TM.CookLevin.Desc.bitsR {ι : Type u_1} [Cost.SizedEncoding ι] (k : ℕ) : Cost.PolyTimeFun ι Cost.BitStr

The bits of a numeral, as a reader.

Equations

• MIPRE.TM.CookLevin.Desc.bitsR k = MIPRE.Cost.PolyTimeFun.const k.bits

theorem MIPRE.TM.CookLevin.Desc.bitsR_spec {ι : Type u_1} [Cost.SizedEncoding ι] (k : ℕ) (i : ι) (j : ℕ) : List.getD ((bitsR k).toFun i) j false = k.testBit j

The widths and offsets

noncomputable def MIPRE.TM.CookLevin.Desc.WU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

W e, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.WU eu = MIPRE.TM.CookLevin.Desc.addU.ap₂ eu (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 4))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_WU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((WU eu).toFun i) = W (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.threeU {ι : Type u_1} [Cost.SizedEncoding ι] : Cost.PolyTimeFun ι Cost.Unary

3, 4 and Qb and Gb Gc, in unary: the widths that do not depend on e.

Equations

• MIPRE.TM.CookLevin.Desc.threeU = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 3)

noncomputable def MIPRE.TM.CookLevin.Desc.fourU {ι : Type u_1} [Cost.SizedEncoding ι] : Cost.PolyTimeFun ι Cost.Unary

Equations

• MIPRE.TM.CookLevin.Desc.fourU = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 4)

noncomputable def MIPRE.TM.CookLevin.Desc.QbU {ι : Type u_1} [Cost.SizedEncoding ι] : Cost.PolyTimeFun ι Cost.Unary

Equations

• MIPRE.TM.CookLevin.Desc.QbU = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary MIPRE.TM.CookLevin.Desc.Qb)

noncomputable def MIPRE.TM.CookLevin.Desc.GbU {ι : Type u_1} [Cost.SizedEncoding ι] : Cost.PolyTimeFun ι Cost.Unary

Equations

• MIPRE.TM.CookLevin.Desc.GbU = MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary (MIPRE.TM.CookLevin.Desc.Gb MIPRE.TM.CookLevin.Desc.Gc))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_threeU {ι : Type u_1} [Cost.SizedEncoding ι] (i : ι) : List.length (threeU.toFun i) = 3

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_fourU {ι : Type u_1} [Cost.SizedEncoding ι] (i : ι) : List.length (fourU.toFun i) = 4

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_QbU {ι : Type u_1} [Cost.SizedEncoding ι] (i : ι) : List.length (QbU.toFun i) = Qb

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_GbU {ι : Type u_1} [Cost.SizedEncoding ι] (i : ι) : List.length (GbU.toFun i) = Gb Gc

noncomputable def MIPRE.TM.CookLevin.Desc.mU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

mOf e Gc, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_mU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((mU eu).toFun i) = mOf (List.length (eu.toFun i)) Gc

noncomputable def MIPRE.TM.CookLevin.Desc.flagOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

flagOff e Gc, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_flagOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((flagOffU eu).toFun i) = flagOff (List.length (eu.toFun i)) Gc

noncomputable def MIPRE.TM.CookLevin.Desc.gOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

gOff e, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_gOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((gOffU eu).toFun i) = gOff (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.dOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

dOff e, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.dOffU eu = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 3)) (MIPRE.TM.CookLevin.Desc.WU eu)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_dOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((dOffU eu).toFun i) = dOff (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.pOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

pOff e, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.pOffU eu = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 7)) (MIPRE.TM.CookLevin.Desc.WU eu)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_pOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((pOffU eu).toFun i) = pOff (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.vOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

vOff e, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.vOffU eu = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 7)) ((MIPRE.TM.CookLevin.Desc.nsmulU 2).ap₁ (MIPRE.TM.CookLevin.Desc.WU eu))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_vOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((vOffU eu).toFun i) = vOff (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.qOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

qOff e, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.qOffU eu = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 10)) ((MIPRE.TM.CookLevin.Desc.nsmulU 2).ap₁ (MIPRE.TM.CookLevin.Desc.WU eu))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_qOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((qOffU eu).toFun i) = qOff (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.jsOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (d : ℕ) : Cost.PolyTimeFun ι Cost.Unary

jsOff e d, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_jsOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (d : ℕ) (i : ι) : List.length ((jsOffU eu d).toFun i) = jsOff (List.length (eu.toFun i)) d

muxList, as a program

noncomputable def MIPRE.TM.CookLevin.Desc.muxListP : Cost.PolyTimeFun (SAT.Fml × List SAT.Fml × List SAT.Fml) (List SAT.Fml)

muxList.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.muxListP_apply (p : SAT.Fml × List SAT.Fml × List SAT.Fml) : muxListP.toFun p = muxList p.1 p.2.1 p.2.2