Polynomial-time lookup and tabulation on rectangular integer row tables

Executable two-dimensional tables of integers with runtime-varying dimensions are represented as lists of rows List (List ℤ) encoded under encList (encList encIntBin). This module provides shared total entry lookup (Cslib.rowEntry, defaulting out-of-bounds indices to 0), rectangular r × c table construction (Cslib.tabulateTable), rectangular shape predicates and extensionality (Cslib.IsTableShape, Cslib.eq_of_isTableShape_of_rowEntry_eq), and plain polynomial-time composition rules (Cslib.computableInPolyTime_rowEntry, Cslib.computableInPolyTime_tabulateTable) with dimensions and indices in unary.

Main definitions

• Cslib.IsTableShape: predicate asserting rows.length = r and every row of rows has length c.
• Cslib.rowEntry: total (i, j) entry lookup on List (List ℤ) returning 0 when missing.
• Cslib.tabulateTable: construct the r × c list of rows whose (i, j) entry is g i j.

Main results

• Cslib.isTableShape_tabulateTable, Cslib.rowEntry_tabulateTable, Cslib.rowEntry_tabulateTable_of_lt: shape and entry lookup of tabulateTable.
• Cslib.exists_rowEntry_eq_of_mem, Cslib.exists_rowEntry_eq, Cslib.rowEntry_rel_of_mem: correspondence between stored list elements and indexed rowEntry values.
• Cslib.eq_of_isTableShape_of_rowEntry_eq, Cslib.tabulateTable_rowEntry: extensionality and re-tabulation on (r, c)-shaped tables.
• Cslib.computableInPolyTime_rowEntry, Cslib.computableInPolyTime_tabulateTable: plain @[fun_prop] polynomial-time certificates over unary indices/dimensions and encIntBin entries.

Shape, lookup, and rectangular tabulation

def Cslib.IsTableShape (r c : ℕ) (rows : List (List ℤ)) : Prop

Shape predicate for a dense r × c integer table: r rows, each of length c.

def Cslib.rowEntry (rows : List (List ℤ)) (i j : ℕ) : ℤ

Entry (i, j) of a table stored as a list of integer rows; missing entries read as 0.

def Cslib.tabulateTable (r c : ℕ) (g : ℕ → ℕ → ℤ) : List (List ℤ)

Construct the r × c list of rows whose (i, j) entry is g i j for i < r and j < c.

@[simp]

theorem Cslib.length_tabulateTable (r c : ℕ) (g : ℕ → ℕ → ℤ) : (tabulateTable r c g).length = r

Tabulating an r × c table produces r rows.

theorem Cslib.length_of_mem_tabulateTable {r c : ℕ} {g : ℕ → ℕ → ℤ} {row : List ℤ} (hrow : row ∈ tabulateTable r c g) : row.length = c

Every row in tabulateTable r c g has length c.

theorem Cslib.isTableShape_tabulateTable (r c : ℕ) (g : ℕ → ℕ → ℤ) : IsTableShape r c (tabulateTable r c g)

Every tabulated r × c table has shape (r, c).

theorem Cslib.rowEntry_tabulateTable (r c : ℕ) (g : ℕ → ℕ → ℤ) (i j : ℕ) : rowEntry (tabulateTable r c g) i j = if i < r ∧ j < c then g i j else 0

Looking up entry (i, j) of tabulateTable r c g returns g i j when i < r and j < c, and 0 otherwise.

theorem Cslib.rowEntry_tabulateTable_of_lt {r c : ℕ} (g : ℕ → ℕ → ℤ) {i j : ℕ} (hi : i < r) (hj : j < c) : rowEntry (tabulateTable r c g) i j = g i j

In-bounds lookup on tabulateTable r c g returns g i j.

theorem Cslib.rowEntry_eq_zero_of_isTableShape {r c : ℕ} {rows : List (List ℤ)} (hrows : IsTableShape r c rows) {i j : ℕ} (h : ¬(i < r ∧ j < c)) : rowEntry rows i j = 0

Outside i < r ∧ j < c, an (r, c)-shaped table reads as 0.

theorem Cslib.exists_rowEntry_eq_of_mem {rows : List (List ℤ)} {row : List ℤ} {z : ℤ} (hrow : row ∈ rows) (hz : z ∈ row) : ∃ (i : ℕ) (j : ℕ), i < rows.length ∧ j < row.length ∧ rowEntry rows i j = z

Every stored entry of a list of rows occurs as rowEntry rows i j at valid in-bounds indices.

theorem Cslib.exists_rowEntry_eq {rows : List (List ℤ)} {row : List ℤ} {z : ℤ} (hrow : row ∈ rows) (hz : z ∈ row) : ∃ (i : ℕ) (j : ℕ), rowEntry rows i j = z

Every stored entry of a list of rows is one of its indexed entries.

theorem Cslib.rowEntry_rel_of_mem {P : ℤ → Prop} (h0 : P 0) {rows : List (List ℤ)} (h : ∀ row ∈ rows, ∀ z ∈ row, P z) (i j : ℕ) : P (rowEntry rows i j)

Any predicate holding for 0 and for every stored entry holds for every rowEntry.

theorem Cslib.eq_of_isTableShape_of_rowEntry_eq {r c : ℕ} {A B : List (List ℤ)} (hA : IsTableShape r c A) (hB : IsTableShape r c B) (h : ∀ i < r, ∀ j < c, rowEntry A i j = rowEntry B i j) : A = B

Two (r, c)-shaped tables are equal when their in-bounds entries agree.

theorem Cslib.tabulateTable_rowEntry {r c : ℕ} {rows : List (List ℤ)} (hrows : IsTableShape r c rows) : tabulateTable r c (rowEntry rows) = rows

Re-tabulating an (r, c)-shaped table from rowEntry recovers it unchanged.

Plain polynomial-time certificates

theorem Cslib.computableInPolyTime_rowEntry {α : Type} {encIn : α ↪ List Bool} {rows : α → List (List ℤ)} {i j : α → ℕ} (hrows : Turing.MultiTapeTM.ComputableInPolyTime rows encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => rowEntry (rows x) (i x) (j x)) encIn Turing.MultiTapeTM.encIntBin

Entry lookup rowEntry on a list of integer rows is computable in polynomial time.

theorem Cslib.computableInPolyTime_tabulateTable {α : Type} {encIn : α ↪ List Bool} {r c : α → ℕ} {g : α → ℕ → ℕ → ℤ} (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encUnary) (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encUnary) (hg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (α × ℕ) × ℕ) => g p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => tabulateTable (r x) (c x) (g x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Tabulating an r × c table of binary integers from unary dimensions (r, c) is computable in polynomial time.