Loops over a range of indices — proof internals

The helper facts behind Complexitylib.Classes.P.Range. Concatenation over a range is a loop whose state carries the output so far, the index in unary, and the input; iterate_mem_FP_of_polyBound runs it, and the bound on its state comes from the rule alone, since a polynomial-time rule has polynomially long outputs and the loop runs at most as often as its argument is long. The rest is the one-bit marks, and the arithmetic behind computing a maximum as a count.

Contents

• listStep, listStep_iterate — the loop and what it accumulates
• entryCat — the accumulated output, indexed by the number of rounds
• bitstringEncode_of_entries — accumulating entry encodings encodes the list
• catRange_mem_FP_internal — concatenation over a range is polynomial-time
• isEmptyMark_mem_FP_internal, nonemptyMark_mem_FP — the one-bit marks
• maxProbe_mem_FP, length_maxProbe_pair — the test behind maxFn

The loop

def Complexity.listStep (E : List Bool → List Bool) (st : List Bool) : List Bool

One step: append the next entry's encoding and advance the counter. The state is pair (pair accumulated counter) input.

Equations

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

theorem Complexity.listStep_mem_FP {E : List Bool → List Bool} (hE : E ∈ FP) : listStep E ∈ FP

def Complexity.entryCat (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : List Bool

The bits the loop has accumulated after n steps.

Equations

• Complexity.entryCat E x n = List.flatMap (fun (i : ℕ) => E (Complexity.pair x (List.replicate i true))) (List.range n)

@[simp]

theorem Complexity.entryCat_zero (E : List Bool → List Bool) (x : List Bool) : entryCat E x 0 = []

theorem Complexity.entryCat_succ (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : entryCat E x (n + 1) = entryCat E x n ++ E (pair x (List.replicate n true))

theorem Complexity.catRange_eq_entryCat (E : List Bool → List Bool) (w : List Bool) : catRange E w = entryCat E (pairSnd w) (pairFst w).length

Concatenation over a range is the loop's accumulation after as many rounds as the count is long.

theorem Complexity.listStep_iterate (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : (listStep E)^[n] (pair (pair [] []) x) = pair (pair (entryCat E x n) (List.replicate n true)) x

What the loop accumulates.

theorem Complexity.length_entryCat_le (E : List Bool → List Bool) (x : List Bool) (b n : ℕ) : (∀ i < n, (E (pair x (List.replicate i true))).length ≤ b) → (entryCat E x n).length ≤ n * b

theorem Complexity.length_entryCat (E : List Bool → List Bool) (x : List Bool) (n : ℕ) : (entryCat E x n).length = ∑ i ∈ Finset.range n, (E (pair x (List.replicate i true))).length

theorem Complexity.catRange_mem_FP_internal {E : List Bool → List Bool} (hE : E ∈ FP) : catRange E ∈ FP

Concatenation over a range is polynomial-time. The loop's state after k rounds holds k outputs of E, each polynomially long in |z|, and k is at most |z|, so the states are polynomially bounded.

Encoding a list

theorem Complexity.listEncFn_eq (E : List Bool → List Bool) (z : List Bool) : listEncFn E z = false :: entryCat E (pairSnd z) (pairFst z).length ++ [true]

theorem Complexity.bitstringEncode_of_entries {α : Type} [DataEncode α] {E : List Bool → List Bool} {x : List Bool} (l : List α) (h : ∀ (i : ℕ) (hi : i < l.length), E (pair x (List.replicate i true)) = DataEncode.bitstringEncode l[i]) : DataEncode.bitstringEncode l = false :: entryCat E x l.length ++ [true]

The accumulation is the encoding. If each step writes the encoding of the corresponding entry, the loop writes the inner part of the list's own encoding.

One-bit marks

theorem Complexity.isEmptyMark_mem_FP_internal {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (z : List Bool) => isEmptyMark (f z)) ∈ FP

theorem Complexity.nonemptyMark_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (z : List Bool) => nonemptyMark (f z)) ∈ FP

theorem Complexity.length_nonemptyMark (s : List Bool) : (nonemptyMark s).length = if s = [] then 0 else 1

The maximum as a count

theorem Complexity.dropEntry_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : dropEntry f ∈ FP

theorem Complexity.maxProbe_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : maxProbe f ∈ FP

theorem Complexity.lt_maxOver_iff {f : List Bool → List Bool} {z : List Bool} {j : ℕ} (n : ℕ) : j < maxOver f z n ↔ ∃ i < n, j < (f (pair z (List.replicate i true))).length

j is below the maximum exactly when some value is longer than j.

theorem Complexity.length_maxProbe_pair (f : List Bool → List Bool) (z : List Bool) (n j : ℕ) : (maxProbe f (pair (pair (List.replicate n true) z) (List.replicate j true))).length = if j < maxOver f z n then 1 else 0

The test behind maxFn: one mark when j is below the maximum.