Searching a block-aligned string for a block

⚠️ Unreviewed by Bolton

A search that keeps its visited set as a run of fixed-width records must be able to ask whether a record is already there. This file supplies that test as a polynomial-time function: one scan, one block per step, accumulating a flag.

The scan is written as an iteration rather than a recursion, because that is the shape Cobham.iterate_mem_FP consumes — the state is a packed pair (pair u f) rest, and one step compares u against the leading block of rest and drops it.

Main definitions

• Complexity.scanStep — one step of the scan, on the unpacked state
• Complexity.memStep — the same on the packed state
• Complexity.memFlag — the verdict of a full scan

Main results

• Complexity.memStep_iterate — the packed iteration tracks the unpacked one
• Complexity.memFlag_eq_true_iff — what the scan decides

The scan, on the unpacked state

def Complexity.anyStepPair (R : List Bool) (f : List Bool → List Bool) (s : List Bool × List Bool) : List Bool × List Bool

One step of a scan that folds a per-record test into a flag. A remainder shorter than one record is a dead end, so the state stands still.

Equations

• Complexity.anyStepPair R f s = if R.length ≤ s.2.length then (Complexity.orBit s.1 (f (List.take R.length s.2)), List.drop R.length s.2) else s

theorem Complexity.anyStepPair_pos (R : List Bool) (f : List Bool → List Bool) (s : List Bool × List Bool) (h : R.length ≤ s.2.length) : anyStepPair R f s = (orBit s.1 (f (List.take R.length s.2)), List.drop R.length s.2)

theorem Complexity.anyStepPair_neg (R : List Bool) (f : List Bool → List Bool) (s : List Bool × List Bool) (h : ¬R.length ≤ s.2.length) : anyStepPair R f s = s

theorem Complexity.anyStepPair_flag (R : List Bool) {f : List Bool → List Bool} (hf : ∀ (z : List Bool), f z = [true] ∨ f z = [false]) {s : List Bool × List Bool} (hs : s.1 = [true] ∨ s.1 = [false]) (n : ℕ) : ((anyStepPair R f)^[n] s).1 = [true] ∨ ((anyStepPair R f)^[n] s).1 = [false]

The flag component of a scan is a flag.

theorem Complexity.anyStepPair_rest_length (R : List Bool) (f : List Bool → List Bool) (s : List Bool × List Bool) (n : ℕ) : ((anyStepPair R f)^[n] s).2.length ≤ s.2.length

The remainder never grows.

theorem Complexity.blockAt_drop (R z : List Bool) (i : ℕ) : blockAt R (List.drop R.length z) i = blockAt R z (i + 1)

Dropping one record shifts the record index.

theorem Complexity.anyStepPair_flag_eq_true_iff (R : List Bool) {f : List Bool → List Bool} (hf : ∀ (z : List Bool), f z = [true] ∨ f z = [false]) (s : List Bool × List Bool) (hs : s.1 = [true] ∨ s.1 = [false]) (n : ℕ) : ((anyStepPair R f)^[n] s).1 = [true] ↔ s.1 = [true] ∨ ∃ i < n, i * R.length + R.length ≤ s.2.length ∧ f (blockAt R s.2 i) = [true]

A scan fires exactly when the test fires on one of the records.

def Complexity.scanStep (R u : List Bool) : List Bool × List Bool → List Bool × List Bool

One step of the membership scan: compare u against the leading record.

Equations

• Complexity.scanStep R u = Complexity.anyStepPair R (Complexity.Cobham.eqFlag u)

theorem Complexity.scanStep_flag (R u : List Bool) {s : List Bool × List Bool} (hs : s.1 = [true] ∨ s.1 = [false]) (n : ℕ) : ((scanStep R u)^[n] s).1 = [true] ∨ ((scanStep R u)^[n] s).1 = [false]

theorem Complexity.scanStep_rest_length (R u : List Bool) (s : List Bool × List Bool) (n : ℕ) : ((scanStep R u)^[n] s).2.length ≤ s.2.length

theorem Complexity.scanStep_flag_eq_true_iff (R u : List Bool) (s : List Bool × List Bool) (hs : s.1 = [true] ∨ s.1 = [false]) (n : ℕ) : ((scanStep R u)^[n] s).1 = [true] ↔ s.1 = [true] ∨ ∃ i < n, i * R.length + R.length ≤ s.2.length ∧ blockAt R s.2 i = u

The scan finds a record exactly when one matches.

The scan, packed

def Complexity.memPack (R u f rest : List Bool) : List Bool

The packed scan state: the ruler, then the sought block, the flag and the remaining string. Everything the step needs travels inside the state, which is what Cobham.iterate_mem_FP iterates.

Equations

• Complexity.memPack R u f rest = Complexity.pair R (Complexity.pair (Complexity.pair u f) rest)

@[simp]

theorem Complexity.memPack_length (R u f rest : List Bool) : (memPack R u f rest).length = 2 * R.length + 2 * (2 * u.length + f.length + 2) + rest.length + 4

def Complexity.memStep (z : List Bool) : List Bool

One step of the scan on the packed state.

Equations

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

theorem Complexity.memStep_pack (R u f rest : List Bool) : memStep (memPack R u f rest) = memPack R u (scanStep R u (f, rest)).1 (scanStep R u (f, rest)).2

The packed step is the unpacked step.

theorem Complexity.memStep_iterate (R u : List Bool) (s : List Bool × List Bool) (n : ℕ) : memStep^[n] (memPack R u s.1 s.2) = memPack R u ((scanStep R u)^[n] s).1 ((scanStep R u)^[n] s).2

The packed iteration is the unpacked one.

The verdict

def Complexity.memFlag (R u V : List Bool) : List Bool

Does the block u occur in the block-aligned string V?

Equations

• Complexity.memFlag R u V = Complexity.pairSnd (Complexity.pairFst (Complexity.pairSnd (Complexity.memStep^[V.length] (Complexity.memPack R u [false] V))))

theorem Complexity.memFlag_flag (R u V : List Bool) : memFlag R u V = [true] ∨ memFlag R u V = [false]

theorem Complexity.memFlag_eq_true_iff (R u V : List Bool) (hR : 0 < R.length) : memFlag R u V = [true] ↔ ∃ (i : ℕ), i * R.length + R.length ≤ V.length ∧ blockAt R V i = u

The scan decides membership.

The scan is polynomial-time

theorem Complexity.memStep_mem_FP : memStep ∈ FP

theorem Complexity.memStep_iterate_length_le (R u : List Bool) (s : List Bool × List Bool) (hf : s.1 = [true] ∨ s.1 = [false]) (n : ℕ) : (memStep^[n] (memPack R u s.1 s.2)).length ≤ (memPack R u s.1 s.2).length

The scan's state never grows.

theorem Complexity.memFlagFn_mem_FP {Rf uf Vf : List Bool → List Bool} (hR : Rf ∈ FP) (hu : uf ∈ FP) (hV : Vf ∈ FP) : (fun (z : List Bool) => memFlag (Rf z) (uf z) (Vf z)) ∈ FP

The membership scan is polynomial-time.