The canonical index of a tableau variable

idxOf e G T v is the index of the variable v in the described 3SAT formula: the answer index j < 4T for a cell of one of the two free tapes inside the answer block — tape 5 for j < 2T and tape 6 otherwise, position r / 2 + 3 for r = j mod 2T, the value 1 for r odd and the blank for r even — and the structured index (encodeVar) for every other variable. So the first 4T variables of the formula are exactly the two answer blocks, which is what item 1 of thm:succinct-sat needs, and decodeVar_fieldsOf_idxOf says that decoding the canonical index returns the variable. decodeVar_ans is the other half: every index below 4T decodes to the answer variable it stands for (planning/succinct-cook-levin.md, S3).

Reading an index built from a number

theorem MIPRE.TM.CookLevin.Desc.getD_bitsOfNat {w : ℕ} (n : ℕ) {i : ℕ} (hi : i < w) : (SAT.bitsOfNat w n).getD i false = n.testBit i

theorem MIPRE.TM.CookLevin.Desc.bitField_bitsOfNat_zero (w n k : ℕ) (hk : k ≤ w) : bitField (SAT.bitsOfNat w n) 0 k = n % 2 ^ k

The answer variables

def MIPRE.TM.CookLevin.Desc.rOf (T j : ℕ) : ℕ

The offset of an answer index inside its block.

Equations

• MIPRE.TM.CookLevin.Desc.rOf T j = if j < 2 * T then j else j - 2 * T

def MIPRE.TM.CookLevin.Desc.tapeIdx (T j : ℕ) : ℕ

The tape code of an answer index: 5 for the first block, 6 for the second.

Equations

• MIPRE.TM.CookLevin.Desc.tapeIdx T j = if j < 2 * T then 5 else 6

def MIPRE.TM.CookLevin.Desc.valOf (T j : ℕ) : CellVal Interp.Sym

The cell value of an answer index: 1 for an odd offset, the blank for an even one.

Equations

• MIPRE.TM.CookLevin.Desc.valOf T j = if MIPRE.TM.CookLevin.Desc.rOf T j % 2 = 1 then MIPRE.TM.CookLevin.CellVal.sym MIPRE.TM.Interp.Sym.one else MIPRE.TM.CookLevin.CellVal.blank

theorem MIPRE.TM.CookLevin.Desc.tapeIdx_lt (T j : ℕ) : tapeIdx T j < 7

theorem MIPRE.TM.CookLevin.Desc.rOf_lt (T j : ℕ) (hj : j < 4 * T) : rOf T j < 2 * T

theorem MIPRE.TM.CookLevin.Desc.four_T_le_flag (e G T : ℕ) (hT : T ≤ Sof e) : 4 * T ≤ 2 ^ flagOff e G

4T fits below the flag bit.

theorem MIPRE.TM.CookLevin.Desc.flag_lt_m (e G : ℕ) : flagOff e G < mOf e G

theorem MIPRE.TM.CookLevin.Desc.decodeVar_ans (e G T : ℕ) (hT : T ≤ Sof e) {j : ℕ} (hj : j < 4 * T) : ∃ (jt : Fin 7) (p : Pos (Sof e)), ↑jt = tapeIdx T j ∧ ↑p = rOf T j / 2 + 3 ∧ decodeVar e G (fieldsOf e G T (SAT.bitsOfNat (mOf e G) j)) = some (TabVar.cell 0 (Sum.inl jt) p (valOf T j))

Every index below 4T decodes to the answer variable it stands for.

The canonical index

def MIPRE.TM.CookLevin.Desc.IsAnsCell (e T : ℕ) (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym) : Prop

The cell is an answer cell: at time 0 on a free tape, inside the answer block, holding 1 or the blank.

Equations

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

@[instance_reducible]

instance MIPRE.TM.CookLevin.Desc.instDecidableIsAnsCell (e T : ℕ) (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym) : Decidable (IsAnsCell e T t d p v)

Equations

• MIPRE.TM.CookLevin.Desc.instDecidableIsAnsCell e T t d p v = id inferInstance

def MIPRE.TM.CookLevin.Desc.ansIdx (e T : ℕ) (d : Tape 7 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym) : ℕ

The answer index of an answer cell.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.idxOf (e G T : ℕ) : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G → ℕ

The canonical index of a tableau variable: the answer index for an answer cell, the structured index (encodeVar) otherwise.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.idxOf e G T (MIPRE.TM.CookLevin.TabVar.head t d p) = MIPRE.Cost.bitsVal (MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.head t d p))
• MIPRE.TM.CookLevin.Desc.idxOf e G T (MIPRE.TM.CookLevin.TabVar.state t q) = MIPRE.Cost.bitsVal (MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.state t q))
• MIPRE.TM.CookLevin.Desc.idxOf e G T (MIPRE.TM.CookLevin.TabVar.emitOne t) = MIPRE.Cost.bitsVal (MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.emitOne t))
• MIPRE.TM.CookLevin.Desc.idxOf e G T (MIPRE.TM.CookLevin.TabVar.emitBad t) = MIPRE.Cost.bitsVal (MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.emitBad t))
• MIPRE.TM.CookLevin.Desc.idxOf e G T (MIPRE.TM.CookLevin.TabVar.emitted t) = MIPRE.Cost.bitsVal (MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.emitted t))
• MIPRE.TM.CookLevin.Desc.idxOf e G T (MIPRE.TM.CookLevin.TabVar.aux t js g) = MIPRE.Cost.bitsVal (MIPRE.TM.CookLevin.Desc.encodeVar e G (MIPRE.TM.CookLevin.TabVar.aux t js g))

theorem MIPRE.TM.CookLevin.Desc.bitsVal_encodeVar_lt (e G : ℕ) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) : Cost.bitsVal (encodeVar e G v) < 2 ^ mOf e G

theorem MIPRE.TM.CookLevin.Desc.ansIdx_lt (e T : ℕ) (hT : T ≤ Sof e) {t : Fin (Sof e + 1)} {d : Tape 7 6} {p : Pos (Sof e)} {v : CellVal Interp.Sym} (h : IsAnsCell e T t d p v) : ansIdx e T d p v < 4 * T

theorem MIPRE.TM.CookLevin.Desc.idxOf_lt (e G T : ℕ) (hT : T ≤ Sof e) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) : idxOf e G T v < 2 ^ mOf e G

theorem MIPRE.TM.CookLevin.Desc.decodeVar_fieldsOf_bitsVal (e G T : ℕ) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) : decodeVar e G (fieldsOf e G T (SAT.bitsOfNat (mOf e G) (Cost.bitsVal (encodeVar e G v)))) = some v

theorem MIPRE.TM.CookLevin.Desc.decodeVar_fieldsOf_idxOf (e G T : ℕ) (hT : T ≤ Sof e) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) : decodeVar e G (fieldsOf e G T (SAT.bitsOfNat (mOf e G) (idxOf e G T v))) = some v

Decoding the canonical index returns the variable.

theorem MIPRE.TM.CookLevin.Desc.idxOf_ans (e G T : ℕ) (hT : T ≤ Sof e) {j : ℕ} (hj : j < 4 * T) {jt : Fin 7} {p : Pos (Sof e)} (hjt : ↑jt = tapeIdx T j) (hp : ↑p = rOf T j / 2 + 3) : idxOf e G T (TabVar.cell 0 (Sum.inl jt) p (valOf T j)) = j

The canonical index of the answer variable of j is j.