Decisions that depend on a bounded amount of data

A constraint of a constraint graph looks at two symbols and a little local data, and says yes or no. The rule may be described by something noncomputable — an alphabet embedding chosen by Classical.choice, say — but it still runs in polynomial time, because it is a table lookup on a bounded key.

The lookup lives in Complexitylib.Classes.P.FinsetDomain, which keeps the old names keySet, mem_keySet and mem_FP_of_bounded_key, and mem_P_of_bounded_key in Complexitylib.Classes.P.DecisionFn. This module re-exports both and keeps the enumeration of bit vectors that the PCP-to-SAT reduction reads.

Main definitions

• Complexity.allVecs — the bit vectors of a given length

Main results

• Complexity.mem_allVecs_iff — allVecs n is exactly the vectors of length n

Enumerating bit vectors

def Complexity.allVecs : ℕ → List (List Bool)

Every bit vector of a given length.

Equations

• Complexity.allVecs 0 = [[]]
• Complexity.allVecs n.succ = List.flatMap (fun (v : List Bool) => [false :: v, true :: v]) (Complexity.allVecs n)

theorem Complexity.mem_allVecs_iff (n : ℕ) (b : List Bool) : b ∈ allVecs n ↔ b.length = n