IP is closed under polynomial-time reductions

If A reduces to B in polynomial time and B has an interactive proof, so has A: the verifier for A computes the reduction and runs the verifier for B on its result, which is still strict oracle PPT (Cslib.Probability.IsOraclePPTOn.preprocess'), with the same provers, completeness and soundness Arora and Barak, Chapter 8.

Main results

• Cslib.Complexity.IsInteractiveProof.comp: an interactive proof along a reduction.
• Cslib.Complexity.PolyTimeReducible.mem_IP: closure of IP under reductions.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.Complexity.IsInteractiveProof.comp {Operation α β : Type} {verifier : β → Probability.WordOracleComp Operation Bool} {A : Set α} {B : Set β} {c s : ENNReal} (h : IsInteractiveProof verifier B c s) {f : α → β} (hf : ∀ (a : α), a ∈ A ↔ f a ∈ B) : IsInteractiveProof (fun (a : α) => verifier (f a)) A c s

An interactive proof for B gives one for every A that f maps into B exactly.

theorem Cslib.Complexity.PolyTimeReducible.mem_IP {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hAB : PolyTimeReducible encA encB A B) (hB : B ∈ IP encB) : A ∈ IP encA

IP is closed under polynomial-time reductions.