refactor(Promise): share probability_sampleList_verifier and replace restatement tests (#884)

Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean

@@ -10,7 +10,9 @@ module
 public import Complexity.Computability.Complexity.Classes.BPP
 public import Complexity.Computability.Complexity.Classes.Promise.Reduction
 public import Complexity.Computability.Complexity.Classes.RP
+public import Complexity.Computability.Complexity.Classes.SharpP
 public import Complexity.Computability.Probabilistic.PPT
+public import Complexity.Languages.Probabilistic.BitString
 public import Complexity.Languages.Probabilistic.Notation
 import Complexity.Computability.Complexity.Classes.RP.Closure
 import Complexity.Computability.Complexity.Classes.SharpP.Probability
@@ -51,6 +53,8 @@ reductions (`PromiseProblem.PolyTimeReducible.mem_PromiseBPP`,
   complement relations between `PromiseRP` and `PromiseCoRP`.
 * `Cslib.Complexity.PromiseP_subset_PromiseRP`, `Cslib.Complexity.PromiseP_subset_PromiseCoRP`,
   `Cslib.Complexity.PromiseP_subset_PromiseBPP`.
+* `Cslib.Complexity.probability_sampleList_verifier`: acceptance probability of sampling a uniform
+  random word for a seeded verifier.
 * `Cslib.Complexity.mem_PromiseBPP_iff_exists_isPPTOn`,
   `Cslib.Complexity.mem_PromiseRP_iff_exists_isPPTOn`,
   `Cslib.Complexity.mem_PromiseCoRP_iff_exists_isPPTOn`: characterizations by uniform strict PPT
@@ -132,6 +136,13 @@ theorem PromiseP_subset_PromiseCoRP : PromiseP enc ⊆ PromiseCoRP enc :=
 theorem PromiseP_subset_PromiseBPP : PromiseP enc ⊆ PromiseBPP enc :=
   (promiseClass_mono P_subset_BPP).trans promiseClass_BPP_subset_PromiseBPP
 
+/-- The program sampling a random string for a seeded verifier accepts with the accepted
+fraction of the strings. -/
+theorem probability_sampleList_verifier (V : α × List Bool → Bool) (a : α) (n : ℕ) :
+    Pr[(fun w => V (a, w)) <$> BitString.sampleList n] = (acceptCount V a n : ℝ) / 2 ^ n := by
+  simp only [ProbComp.eval_map, BitString.eval_sampleList]
+  exact uniformList_acceptCount_toReal V a n
+
 /-- **Probabilistic-program characterization of `PromiseBPP`**: a promise problem is in
 `PromiseBPP` exactly when a uniform strict PPT Boolean program accepts every yes-instance with
 probability at least `2 / 3` and rejects every no-instance with probability at least `2 / 3`. -/
@@ -146,14 +157,13 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔
       IsPPTOn.of_seeded ((ComputableInPolyTime.unary_eval p).comp
         (ComputableInPolyTime.encoding_length enc)) hV,
       fun a ha => ?_, fun a ha => ?_⟩
-    · simp only [ProbComp.eval_map, BitString.eval_sampleList]
-      rw [uniformList_acceptCount_toReal, le_div_iff₀ (by positivity)]
+    · rw [probability_sampleList_verifier, le_div_iff₀ (by positivity)]
       have h : (2 : ℝ) * 2 ^ p.eval (enc a).length ≤
           3 * (acceptCount V a (p.eval (enc a).length) : ℝ) := by
         exact_mod_cast (hQ a).1 ha
       linarith
-    · simp only [Functor.map_map, ProbComp.eval_map, BitString.eval_sampleList]
-      rw [uniformList_acceptCount_toReal (V := fun x => !V x), le_div_iff₀ (by positivity)]
+    · rw [Functor.map_map, probability_sampleList_verifier (V := fun x => !V x),
+        le_div_iff₀ (by positivity)]
       have h : (2 : ℝ) * 2 ^ p.eval (enc a).length ≤
           3 * (acceptCount (fun x => !V x) a (p.eval (enc a).length) : ℝ) := by
         simpa only [acceptCount, Bool.not_eq_true'] using
@@ -204,8 +214,7 @@ theorem mem_PromiseRP_iff_exists_isPPTOn : Q ∈ PromiseRP enc ↔
       IsPPTOn.of_seeded ((ComputableInPolyTime.unary_eval p).comp
         (ComputableInPolyTime.encoding_length enc)) hV,
       fun a ha => ?_, fun a ha hmem => ?_⟩
-    · simp only [ProbComp.eval_map, BitString.eval_sampleList]
-      rw [uniformList_acceptCount_toReal, le_div_iff₀ (by positivity)]
+    · rw [probability_sampleList_verifier, le_div_iff₀ (by positivity)]
       have h : (2 : ℝ) ^ p.eval (enc a).length ≤
           2 * (acceptCount V a (p.eval (enc a).length) : ℝ) := by
         exact_mod_cast (hQ a).1 ha

Complexity/Computability/Complexity/Classes/Promise/Randomized.lean

@@ -430,13 +430,6 @@ private theorem probability_and2 (M : α → ProbComp Bool) (a : α) :
     simp [ProbComp.eval_map, PMF.map_apply]
   rw [htrue, hfalse, mul_zero, add_zero]
 
-/-- The program sampling a random string for a seeded verifier accepts with the accepted
-fraction of the strings. -/
-private theorem probability_sampleList_verifier (V : β × List Bool → Bool) (b : β) (n : ℕ) :
-    Pr[(fun w => V (b, w)) <$> BitString.sampleList n] = (acceptCount V b n : ℝ) / 2 ^ n := by
-  simp only [ProbComp.eval_map, BitString.eval_sampleList]
-  exact uniformList_acceptCount_toReal V b n
-
 /-- **`PromiseCoRP` is closed under `RPReducible`** (library lemma): if `X` reduces to `Y` by a
 randomized one-sided reduction and `Y ∈ PromiseCoRP encB`, then `X ∈ PromiseCoRP encA`. -/
 theorem RPReducible.mem_PromiseCoRP (hXY : RPReducible encA encB X Y)

ComplexityTests/PromiseProbabilistic.lean

@@ -4,87 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
+import Complexity.Computability.Complexity.Classes.BPP.Amplification
 import Complexity.Computability.Complexity.Classes.Promise.Randomized
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 
-/-! Tests for probabilistic promise classes (`PromiseBPP`, `PromiseRP`, `PromiseCoRP`) and
-randomized one-sided promise reductions (`RPReducible`, `RPReducibleWithError`), including
-nonvacuous coin-flip solvers, soundness strictly between `2 / 3` and `1`, and the `s ≤ 0` edge
-case. -/
+/-! Tests for probabilistic promise classes (`PromiseBPP`, `PromiseRP`, `PromiseCoRP`),
+`probability_sampleList_verifier`, error amplification (`SolvesWithBoundedError.repeatMajority`) on
+a genuinely partial promise problem, and randomized one-sided promise reductions (`RPReducible`,
+`RPReducibleWithError`). -/
 
 namespace ComplexityTests.PromiseProbabilistic
 
 open Cslib Cslib.Complexity Cslib.Probability Turing.MultiTapeTM
 
-variable {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool}
-
-/-! ### Randomized reductions on promise problems -/
-
-example {X : PromiseProblem α} {Y : PromiseProblem β} :
-    PromiseProblem.RPReducible encA encB X Y ↔
-      ∃ R : α → Cslib.ProbComp β, Cslib.Probability.IsPPTOn encA encB R ∧
-        (∀ a ∈ X.yes, ∀ b ∈ (Cslib.ProbComp.eval (R a)).support, b ∈ Y.yes) ∧
-        ∀ a ∈ X.no, 2 / 3 ≤ ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.no).toReal :=
-  Iff.rfl
-
-example {X : PromiseProblem α} {Y : PromiseProblem β} :
-    PromiseProblem.RPReducible encA encB X Y ↔
-      ∃ R : α → Cslib.ProbComp β, Cslib.Probability.IsPPTOn encA encB R ∧
-        (∀ a ∈ X.yes, ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.yes).toReal = 1) ∧
-        ∀ a ∈ X.no, 2 / 3 ≤ ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.no).toReal :=
-  PromiseProblem.rpReducible_iff_toOuterMeasure_eq_one
-
-example {X : PromiseProblem α} {Y : PromiseProblem β} {s : α → ℝ} :
-    PromiseProblem.RPReducibleWithError encA encB s Xᶜ Yᶜ ↔
-      ∃ R : α → Cslib.ProbComp β, Cslib.Probability.IsPPTOn encA encB R ∧
-        (∀ a ∈ X.no, ∀ b ∈ (Cslib.ProbComp.eval (R a)).support, b ∈ Y.no) ∧
-        ∀ a ∈ X.yes, s a ≤ ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.yes).toReal :=
-  PromiseProblem.rpReducibleWithError_compl_iff
-
-example {X : PromiseProblem α} {Y : PromiseProblem β}
-    (h : PromiseProblem.PolyTimeReducible encA encB X Y) :
-    PromiseProblem.RPReducible encA encB X Y :=
-  h.rpReducible
-
-example {X : PromiseProblem α} : PromiseProblem.RPReducible encA encA X X :=
-  PromiseProblem.RPReducible.refl encA X
-
-example {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ}
-    {s₁ : α → ℝ} {s₂ : ℝ} (hs₂ : 0 ≤ s₂)
-    (hXY : PromiseProblem.RPReducibleWithError encA encB s₁ X Y)
-    (hYZ : PromiseProblem.RPReducibleWithError encB encC (fun _ => s₂) Y Z) :
-    PromiseProblem.RPReducibleWithError encA encC (fun a => s₁ a * s₂) X Z :=
-  hXY.trans hYZ hs₂
-
-example {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ}
-    {s₁ : α → ℝ} {s₂ : ℝ} (hs₂ : s₂ ≤ 1)
-    (hXY : PromiseProblem.RPReducibleWithError encA encB s₁ X Y)
-    (hYZ : PromiseProblem.RPReducibleWithError encB encC (fun _ => s₂) Y Z) :
-    PromiseProblem.RPReducibleWithError encA encC (fun a => s₁ a + s₂ - 1) X Z :=
-  hXY.trans_add hYZ hs₂
-
-example {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ}
-    {s : β → ℝ} {f : α → β} (hf : ComputableInPolyTime f encA encB)
-    (hyes : Set.MapsTo f X.yes Y.yes) (hno : Set.MapsTo f X.no Y.no)
-    (hYZ : PromiseProblem.RPReducibleWithError encB encC s Y Z) :
-    PromiseProblem.RPReducibleWithError encA encC (fun a => s (f a)) X Z :=
-  hYZ.of_computableInPolyTime hf hyes hno
-
-example {X : PromiseProblem α} {Y : PromiseProblem β}
-    (hXY : PromiseProblem.RPReducible encA encB X Y)
-    (hY : Y ∈ PromiseCoRP encB) : X ∈ PromiseCoRP encA :=
-  hXY.mem_PromiseCoRP hY
-
-example {X : PromiseProblem α} {Y : PromiseProblem β}
-    (hXY : PromiseProblem.RPReducible encA encB X Y)
-    (hY : Y ∈ PromiseBPP encB) : X ∈ PromiseBPP encA :=
-  hXY.mem_PromiseBPP hY
-
-example {X : PromiseProblem α} {Y : PromiseProblem β}
-    (hXY : PromiseProblem.RPReducible encA encB Xᶜ Yᶜ)
-    (hY : Y ∈ PromiseRP encB) : X ∈ PromiseRP encA :=
-  hXY.mem_PromiseRP_of_compl hY
-
 /-! ### Nonvacuous concrete instances -/
 
 /-- A concrete `PromiseRP` solver using a real 1-bit coin flip: on `true`,
@@ -139,4 +71,59 @@ example : PromiseProblem.RPReducibleWithError encBool encBool (fun _ => 0)
   simp only [ProbComp.eval_pure, PMF.support_pure, Set.mem_singleton_iff] at hb
   exact hb
 
+/-! ### Error amplification on a genuinely partial promise problem -/
+
+/-- A genuinely partial promise problem on bit strings (`yes = {[true]}`, `no = {[false]}`),
+leaving `[]` outside the promise. -/
+def partialSingletonBit : PromiseProblem (List Bool) where
+  yes := {[true]}
+  no := {[false]}
+  disjoint := by simp
+
+/-- The promise of `partialSingletonBit` is a proper subset of `Set.univ` (`[]` is outside the
+promise). -/
+example : partialSingletonBit.yes ∪ partialSingletonBit.no ≠ Set.univ := by
+  intro h
+  have hmem : ([] : List Bool) ∈ partialSingletonBit.yes ∪ partialSingletonBit.no :=
+    h ▸ Set.mem_univ []
+  simp [partialSingletonBit] at hmem
+
+/-- A 1-bit verifier that returns the first input bit when present and falls back to the first
+random bit on `[]`. -/
+def partialVerifier (p : List Bool × List Bool) : Bool :=
+  p.1.headD (p.2.headD false)
+
+/-- On the out-of-promise input `[]`, `partialVerifier` accepts with probability `1 / 2`, violating
+the `2 / 3` bounded-error margin on both sides. -/
+example :
+    Pr[(fun w => partialVerifier ([], w)) <$> BitString.sampleList 1] = 1 / 2 := by
+  rw [probability_sampleList_verifier]
+  have hcard : acceptCount partialVerifier [] 1 = 1 := by decide
+  rw [hcard]
+  norm_num
+
+/-- Despite accepting the out-of-promise instance `[]` with probability `1 / 2`, `partialVerifier`
+solves `partialSingletonBit` with bounded error. -/
+theorem solvesWithBoundedError_partialSingletonBit :
+    partialSingletonBit.SolvesWithBoundedError encBits 1 partialVerifier := by
+  intro a
+  refine ⟨fun ha => ?_, fun ha => ?_⟩
+  · obtain rfl : a = [true] := ha
+    generalize hk : (1 : Polynomial ℕ).eval (encBits [true]).length = k
+    rw [Polynomial.eval_one] at hk
+    subst hk
+    decide
+  · obtain rfl : a = [false] := ha
+    generalize hk : (1 : Polynomial ℕ).eval (encBits [false]).length = k
+    rw [Polynomial.eval_one] at hk
+    subst hk
+    decide
+
+/-- Majority amplification (`SolvesWithBoundedError.repeatMajority`) reduces the error on
+`partialSingletonBit` to `2 ^ (-q(n))` without requiring any margin outside the promise. -/
+example (q : Polynomial ℕ) :
+    partialSingletonBit.SolvesWithErrorExponent encBits q (12 * q * 1)
+      (repeatMajority encBits (6 * q) 1 partialVerifier) :=
+  solvesWithBoundedError_partialSingletonBit.repeatMajority q
+
 end ComplexityTests.PromiseProbabilistic