From 80b67eb3150ec2977547a5a26932dd6e46fed932 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 02:11:27 +0000 Subject: [PATCH 1/3] refactor(ArthurMerlin): factor MA/AM amplification through BPP per-instance error bounds (#949) --- .../Circuit/Boolean/PolynomialTime.lean | 1 + .../Complexity/Classes/ArthurMerlin.lean | 69 +++++- .../Classes/ArthurMerlin/Amplification.lean | 205 ++++++------------ .../Complexity/Classes/ArthurMerlin/PH.lean | 6 +- .../Classes/ArthurMerlin/SetLowerBound.lean | 1 + .../Computability/Complexity/Classes/BPP.lean | 77 ++++++- .../Complexity/Classes/BPP/Amplification.lean | 168 +++++++------- .../Complexity/Classes/BPP/Reduction.lean | 7 +- .../Computability/Complexity/Classes/IP.lean | 7 +- .../Computability/Complexity/Classes/PP.lean | 6 +- .../Classes/Promise/Probabilistic.lean | 2 + .../Classes/Promise/Randomized.lean | 4 +- .../Computability/Complexity/Classes/RP.lean | 1 + .../Computability/Complexity/Classes/SBP.lean | 8 +- .../Complexity/Classes/Time.lean | 2 + .../Complexity/Classes/Toda.lean | 1 + .../Complexity/Classes/Toda/Hierarchy.lean | 3 +- ComplexityTests/ArthurMerlin.lean | 16 +- ComplexityTests/InteractiveProofs.lean | 2 +- ComplexityTests/NonVacuity.lean | 4 +- ComplexityTests/ResourceClasses4.lean | 4 +- ComplexityTests/SipserLautemann.lean | 2 + 22 files changed, 348 insertions(+), 248 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean b/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean index 07a231358b..ba5b4a224e 100644 --- a/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean +++ b/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean @@ -179,6 +179,7 @@ theorem BPP_subset_PPolyOn : Complexity.BPP enc ⊆ PPolyOn enc := by (polynomiallyBounded_complexity_framedSlice hL' (by fun_prop)) (encodes enc) (encodesMember enc A) fun n x ⟨a, ha⟩ => by have h := hdec a + dsimp only [Complexity.BoundedErrorAt, Complexity.outcomeCount] at h rw [ha, List.length_ofFn] at h by_cases haA : a ∈ A · rw [(encodesMember_eq_true_iff ha).2 haA] diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean index 2ca0957f3d..4a61b1a962 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean @@ -53,10 +53,15 @@ the second level of the polynomial hierarchy in ## Main definitions * `Cslib.Complexity.IsMerlinArthurVerifier`, `Cslib.Complexity.MA`. +* `Cslib.Complexity.arthurMerlinAcceptCount`, `Cslib.Complexity.arthurMerlinRejectCount`, + `Cslib.Complexity.arthurMerlinSlice`: per-instance Arthur–Merlin coin counts and reply-existence + verifier. * `Cslib.Complexity.IsArthurMerlinVerifier`, `Cslib.Complexity.AM`. ## Main results +* `Cslib.Complexity.isArthurMerlinVerifier_iff_decidesWithBoundedError`: an Arthur–Merlin verifier + is a bounded-error decider when composed with existential quantification over Merlin's reply. * `Cslib.Complexity.NP_subset_MA`, `Cslib.Complexity.BPP_subset_MA`. * `Cslib.Complexity.PolyTimeReducible.mem_MA`, `Cslib.Complexity.PolyTimeReducible.mem_AM`: closure under polynomial-time many-one reductions. @@ -85,12 +90,10 @@ makes at least two thirds of the random strings `r` accepted, `V (a, y ++ r) = t non-member every proof leaves at least two thirds of the random strings rejected. -/ def IsMerlinArthurVerifier (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop := - ∀ a, (a ∈ A → ∃ y : Fin (q.eval (enc a).length) → Bool, 2 * 2 ^ p.eval (enc a).length ≤ - 3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn y ++ List.ofFn r) = true).card) ∧ - (a ∉ A → ∀ y : Fin (q.eval (enc a).length) → Bool, 2 * 2 ^ p.eval (enc a).length ≤ - 3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn y ++ List.ofFn r) = false).card) + ∀ a, (a ∈ A → ∃ y : Fin (q.eval (enc a).length) → Bool, + BoundedErrorAt enc p (fun z => V (z.1, List.ofFn y ++ z.2)) a true) ∧ + (a ∉ A → ∀ y : Fin (q.eval (enc a).length) → Bool, + BoundedErrorAt enc p (fun z => V (z.1, List.ofFn y ++ z.2)) a false) /-- The problems with polynomial-time Merlin–Arthur verifiers, with polynomially long proofs and random strings, with respect to the encoding `enc` of instances [Babai][Babai1985]. -/ @@ -105,6 +108,38 @@ theorem mem_MA : A ∈ MA enc ↔ ∃ (q p : Polynomial ℕ) (V : α × List Boo /-! ### Arthur–Merlin -/ +/-- The number of random strings `r` of length `m` for which some reply `y` of length `n` is +accepted by `V` on `a`. -/ +@[reducible] +def arthurMerlinAcceptCount (V : α × List Bool → Bool) (a : α) (m n : ℕ) : ℕ := + (univ.filter fun r : Fin m → Bool => + ∃ y : Fin n → Bool, V (a, List.ofFn r ++ List.ofFn y) = true).card + +/-- The number of random strings `r` of length `m` for which every reply `y` of length `n` is +rejected by `V` on `a`. -/ +@[reducible] +def arthurMerlinRejectCount (V : α × List Bool → Bool) (a : α) (m n : ℕ) : ℕ := + (univ.filter fun r : Fin m → Bool => + ∀ y : Fin n → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card + +/-- Whether some reply `y` of length `q(|x.1|)` is accepted by `V` on `(x.1, x.2 ++ y)`. -/ +def arthurMerlinSlice (enc : α ↪ List Bool) (q : Polynomial ℕ) (V : α × List Bool → Bool) + (x : α × List Bool) : Bool := + decide (∃ y : Fin (q.eval (enc x.1).length) → Bool, V (x.1, x.2 ++ List.ofFn y) = true) + +theorem arthurMerlinAcceptCount_eq_outcomeCount (enc : α ↪ List Bool) (q : Polynomial ℕ) + (V : α × List Bool → Bool) (a : α) (m : ℕ) : + arthurMerlinAcceptCount V a m (q.eval (enc a).length) = + outcomeCount (arthurMerlinSlice enc q V) a m true := by + simp only [arthurMerlinAcceptCount, outcomeCount, arthurMerlinSlice, decide_eq_true_iff] + +theorem arthurMerlinRejectCount_eq_outcomeCount (enc : α ↪ List Bool) (q : Polynomial ℕ) + (V : α × List Bool → Bool) (a : α) (m : ℕ) : + arthurMerlinRejectCount V a m (q.eval (enc a).length) = + outcomeCount (arthurMerlinSlice enc q V) a m false := by + simp only [arthurMerlinRejectCount, outcomeCount, arthurMerlinSlice, decide_eq_false_iff_not, + not_exists, Bool.not_eq_true] + /-- `V` is an Arthur–Merlin verifier for `A`, with random strings of length `p` and replies of length `q`, both evaluated at the length of the encoded instance: on a member `a` at least two thirds of the random strings `r` have a reply `y` with `V (a, r ++ y) = true`; on a non-member at @@ -112,11 +147,20 @@ least two thirds of them have none. -/ def IsArthurMerlinVerifier (enc : α ↪ List Bool) (p q : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop := ∀ a, (a ∈ A → 2 * 2 ^ p.eval (enc a).length ≤ - 3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - ∃ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = true).card) ∧ + 3 * arthurMerlinAcceptCount V a (p.eval (enc a).length) (q.eval (enc a).length)) ∧ (a ∉ A → 2 * 2 ^ p.eval (enc a).length ≤ - 3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - ∀ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card) + 3 * arthurMerlinRejectCount V a (p.eval (enc a).length) (q.eval (enc a).length)) + +/-- An Arthur–Merlin verifier is a bounded-error decider when composed with existential +quantification over Merlin's reply. -/ +theorem isArthurMerlinVerifier_iff_decidesWithBoundedError {p q : Polynomial ℕ} + {V : α × List Bool → Bool} : + IsArthurMerlinVerifier enc p q V A ↔ + DecidesWithBoundedError enc p (arthurMerlinSlice enc q V) A := by + simp only [IsArthurMerlinVerifier, DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, + BoundedErrorAt, arthurMerlinAcceptCount_eq_outcomeCount, + arthurMerlinRejectCount_eq_outcomeCount] + rfl /-- The problems with polynomial-time Arthur–Merlin verifiers, with polynomially long random strings and replies, with respect to the encoding `enc` of instances @@ -147,9 +191,11 @@ theorem NP_subset_MA : NP enc ⊆ MA enc := by · obtain ⟨w, hw, hVw⟩ := (hA a).1 ha refine ⟨BitString.ofList _ w, two_mul_two_pow_le_card_filter_of_eq_zero (Polynomial.eval_zero) _ fun r => ?_⟩ + dsimp only rw [BitString.ofFn_ofList hw, List.eq_nil_of_length_eq_zero (by simp : (List.ofFn r).length = 0), List.append_nil, hVw] · refine two_mul_two_pow_le_card_filter_of_eq_zero (Polynomial.eval_zero) _ fun r => ?_ + dsimp only rw [List.eq_nil_of_length_eq_zero (by simp : (List.ofFn r).length = 0), List.append_nil] by_contra hVy exact ha ((hA a).2 ⟨_, List.length_ofFn, by simpa using hVy⟩) @@ -218,6 +264,7 @@ theorem PolyTimeReducible.mem_MA {encB : β ↪ List Bool} {B : Set β} obtain ⟨q, p, V, hV, hVB⟩ := hB obtain ⟨Q, P, V', hV', hQe, hPe, hsplit⟩ := exists_truncated_verifier hf.tidy q p hV.tidy refine ⟨Q, P, V', .of_tidy hV', fun a => ?_⟩ + dsimp only [BoundedErrorAt, outcomeCount] simp only [hsplit] constructor · intro ha @@ -257,7 +304,7 @@ theorem PolyTimeReducible.mem_AM {encB : β ↪ List Bool} {B : Set β} V (f a, (List.ofFn r).take (p.eval (encB (f a)).length) ++ List.ofFn y) = false := BitString.forall_take_ofFn_iff (hQe a) (g := fun w => V (f a, (List.ofFn r).take (p.eval (encB (f a)).length) ++ w) = false) - simp only [hsplit, hex, hall] + simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, hsplit, hex, hall] exact ⟨fun ha => two_mul_two_pow_le_card_filter_take (hPe a) (fun w => ∃ y : Fin (q.eval (encB (f a)).length) → Bool, V (f a, w ++ List.ofFn y) = true) ((hVB (f a)).1 ((hAB a).1 ha)), diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean index 25e099b91a..feb5c22d23 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.Classes.ArthurMerlin +public import Complexity.Computability.Complexity.Classes.BPP.Amplification public import Complexity.Computability.Complexity.Classes.RepeatedTrials public import Complexity.Computability.Complexity.Classes.SBP public import Complexity.Foundations.Data.BitString.WordCount @@ -97,12 +98,10 @@ member some proof is rejected on at most a `2 ^ (-e(n))` fraction of the random non-member every proof is accepted on at most such a fraction. -/ def IsMerlinArthurVerifierWithErrorExponent (enc : α ↪ List Bool) (e q p : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop := - ∀ a, (a ∈ A → ∃ y : Fin (q.eval (enc a).length) → Bool, 2 ^ e.eval (enc a).length * - (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn y ++ List.ofFn r) = false).card ≤ 2 ^ p.eval (enc a).length) ∧ - (a ∉ A → ∀ y : Fin (q.eval (enc a).length) → Bool, 2 ^ e.eval (enc a).length * - (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn y ++ List.ofFn r) = true).card ≤ 2 ^ p.eval (enc a).length) + ∀ a, (a ∈ A → ∃ y : Fin (q.eval (enc a).length) → Bool, + ErrorExponentAt enc e p (fun z => V (z.1, List.ofFn y ++ z.2)) a true) ∧ + (a ∉ A → ∀ y : Fin (q.eval (enc a).length) → Bool, + ErrorExponentAt enc e p (fun z => V (z.1, List.ofFn y ++ z.2)) a false) /-- The strict majority of `2 r(n)` runs of a Merlin–Arthur verifier `V` on one proof, where `n` is the length of the encoded instance: the string is a proof of `q(n)` bits followed by `2 r(n)` @@ -123,16 +122,14 @@ theorem computableInPolyTime_merlinArthurRepeat {V : α × List Bool → Bool} unfold merlinArthurRepeat repeatMajority repeatVotes fun_prop -/-- On a proof followed by `2 r(n)` rows of `p(n)` bits, the majority vote compares the number of -rows accepted with the proof with `r(n)`. -/ -private theorem merlinArthurRepeat_ofFn_append_ofFn {q r p : Polynomial ℕ} +/-- On a proof of length `q(n)` followed by a random string `w`, `merlinArthurRepeat` is +`repeatMajority` with that proof fixed. -/ +private theorem merlinArthurRepeat_ofFn_append {q r p : Polynomial ℕ} {V : α × List Bool → Bool} - (a : α) (y : Fin (q.eval (enc a).length) → Bool) - (x : BitString (2 * r.eval (enc a).length * p.eval (enc a).length)) : - merlinArthurRepeat enc q r p V (a, List.ofFn y ++ List.ofFn x) = decide (r.eval (enc a).length < - #{i | V (a, List.ofFn y ++ List.ofFn (BitString.block x i)) = true}) := by + (a : α) (y : Fin (q.eval (enc a).length) → Bool) (w : List Bool) : + merlinArthurRepeat enc q r p V (a, List.ofFn y ++ w) = + repeatMajority enc r p (fun z => V (z.1, List.ofFn y ++ z.2)) (a, w) := by rw [merlinArthurRepeat, List.take_left' List.length_ofFn, List.drop_left' List.length_ofFn] - exact repeatMajority_ofFn (V := fun z => V (z.1, List.ofFn y ++ z.2)) a x /-- **Error reduction for `MA`** [Babai][Babai1985]. The strict majority of `12 e(n)` runs of a Merlin–Arthur verifier with one proof, on independent blocks of random bits, errs on at most a @@ -140,50 +137,18 @@ Merlin–Arthur verifier with one proof, on independent blocks of random bits, e theorem IsMerlinArthurVerifier.repeatMajority {q p : Polynomial ℕ} {V : α × List Bool → Bool} (h : IsMerlinArthurVerifier enc q p V A) (e : Polynomial ℕ) : IsMerlinArthurVerifierWithErrorExponent enc e q (12 * e * p) - (merlinArthurRepeat enc q (6 * e) p V) A := by - intro a - have hlen : (12 * e * p).eval (enc a).length = - 2 * (6 * e).eval (enc a).length * p.eval (enc a).length := by - simp only [Polynomial.eval_mul, Polynomial.eval_ofNat] - ring - have hR : (6 * e).eval (enc a).length = 6 * e.eval (enc a).length := by simp - rw [hlen] - constructor - · -- on a member, the good proof is rejected only when at most `R` runs accept - intro ha - obtain ⟨y, hy⟩ := (h a).1 ha - refine ⟨y, (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans - (BitString.two_pow_mul_card_filter_card_filter_block_le hR - (fun s => V (a, List.ofFn y ++ List.ofFn s) = true) hy)⟩ - rw [mem_filter, merlinArthurRepeat_ofFn_append_ofFn, decide_eq_false_iff_not, not_lt] at hx - exact mem_filter.2 ⟨mem_univ _, hx.2⟩ - · -- on a non-member, every proof is accepted only when at most `R` runs reject - intro ha y - refine (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans - (BitString.two_pow_mul_card_filter_card_filter_block_le hR - (fun s => V (a, List.ofFn y ++ List.ofFn s) = false) ((h a).2 ha y)) - rw [mem_filter, merlinArthurRepeat_ofFn_append_ofFn, decide_eq_true_iff] at hx - have hsum := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * - (6 * e).eval (enc a).length)))) - fun i => V (a, List.ofFn y ++ List.ofFn (BitString.block x i)) = true - simp only [Bool.not_eq_true, card_univ, Fintype.card_fin] at hsum - refine mem_filter.2 ⟨mem_univ _, ?_⟩ - omega + (merlinArthurRepeat enc q (6 * e) p V) A := + fun a => ⟨fun ha => let ⟨y, hy⟩ := (h a).1 ha + ⟨y, (hy.repeatMajority e).congr fun _ => (merlinArthurRepeat_ofFn_append a y _).symm⟩, + fun ha y => (((h a).2 ha y).repeatMajority e).congr fun _ => + (merlinArthurRepeat_ofFn_append a y _).symm⟩ /-- Error at most `2 ^ (-e(n)) ≤ 1 / 4` is error at most `1 / 3`. -/ theorem IsMerlinArthurVerifierWithErrorExponent.isMerlinArthurVerifier {e q p : Polynomial ℕ} {V : α × List Bool → Bool} (h : IsMerlinArthurVerifierWithErrorExponent enc e q p V A) - (he : ∀ n, 2 ≤ e.eval n) : IsMerlinArthurVerifier enc q p V A := fun a => by - have h4 : 4 ≤ 2 ^ e.eval (enc a).length := - (Nat.pow_le_pow_right (by norm_num) (he _) : 2 ^ 2 ≤ _) - constructor - · intro ha - obtain ⟨y, hy⟩ := (h a).1 ha - refine ⟨y, BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le _ ?_⟩ - simpa only [Bool.not_eq_true] using (Nat.mul_le_mul_right _ h4).trans hy - · intro ha y - refine BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le _ ?_ - simpa only [Bool.not_eq_false] using (Nat.mul_le_mul_right _ h4).trans ((h a).2 ha y) + (he : ∀ n, 2 ≤ e.eval n) : IsMerlinArthurVerifier enc q p V A := + fun a => ⟨fun ha => let ⟨y, hy⟩ := (h a).1 ha; ⟨y, hy.boundedErrorAt (he _)⟩, + fun ha y => ((h a).2 ha y).boundedErrorAt (he _)⟩ /-- **Error reduction for `MA`** [Babai][Babai1985]: a problem is in `MA` exactly when, for some polynomial proof length `q` and every polynomial `e`, it has a polynomial-time Merlin–Arthur @@ -192,17 +157,11 @@ before the error, so the error can be made smaller than `2 ^ (-q(n))`. -/ theorem mem_MA_iff_exists_forall_errorExponent : A ∈ MA enc ↔ ∃ q : Polynomial ℕ, ∀ e : Polynomial ℕ, ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), ComputableInPolyTime V (encPair enc encBits) encBool ∧ - IsMerlinArthurVerifierWithErrorExponent enc e q p V A := by - have this : A ∈ MA enc ↔ ∃ q : Polynomial ℕ, ∀ e : Polynomial ℕ, ∃ (p : Polynomial ℕ) - (V : α × List Bool → Bool), ComputableTidilyInPolyTime V (encPair enc encBits) encBool ∧ - IsMerlinArthurVerifierWithErrorExponent enc e q p V A := by - rw [mem_MA] - refine ⟨fun ⟨q, p, V, hV, h⟩ => ⟨q, fun e => ⟨12 * e * p, _, - (computableInPolyTime_merlinArthurRepeat hV _ _ _).tidy, h.repeatMajority e⟩⟩, - fun ⟨q, h⟩ => ?_⟩ - obtain ⟨p, V, hV, h⟩ := h 2 - exact ⟨q, p, V, (.of_tidy hV), h.isMerlinArthurVerifier fun _ => by simp⟩ - simpa only [computableInPolyTime_iff_computableTidilyInPolyTime] using this + IsMerlinArthurVerifierWithErrorExponent enc e q p V A := + ⟨fun ⟨q, p, V, hV, h⟩ => ⟨q, fun e => ⟨12 * e * p, _, + computableInPolyTime_merlinArthurRepeat hV _ _ _, h.repeatMajority e⟩⟩, + fun ⟨q, h⟩ => let ⟨p, V, hV, h⟩ := h 2 + ⟨q, p, V, hV, h.isMerlinArthurVerifier fun _ => by simp⟩⟩ /-! ### Error reduction for `AM` -/ @@ -213,14 +172,23 @@ non-member at most such a fraction have one. -/ def IsArthurMerlinVerifierWithErrorExponent (enc : α ↪ List Bool) (e p q : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop := ∀ a, (a ∈ A → 2 ^ e.eval (enc a).length * - (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - ∀ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card ≤ + arthurMerlinRejectCount V a (p.eval (enc a).length) (q.eval (enc a).length) ≤ 2 ^ p.eval (enc a).length) ∧ (a ∉ A → 2 ^ e.eval (enc a).length * - (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - ∃ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = true).card ≤ + arthurMerlinAcceptCount V a (p.eval (enc a).length) (q.eval (enc a).length) ≤ 2 ^ p.eval (enc a).length) +/-- An Arthur–Merlin verifier has error exponent `e` iff its reply-existence slice decides with +error exponent `e`. -/ +theorem isArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent + {e p q : Polynomial ℕ} {V : α × List Bool → Bool} : + IsArthurMerlinVerifierWithErrorExponent enc e p q V A ↔ + DecidesWithErrorExponent enc e p (arthurMerlinSlice enc q V) A := by + simp only [IsArthurMerlinVerifierWithErrorExponent, DecidesWithErrorExponent, + PromiseProblem.SolvesWithErrorExponent, ErrorExponentAt, Bool.not_true, Bool.not_false, + arthurMerlinAcceptCount_eq_outcomeCount, arthurMerlinRejectCount_eq_outcomeCount] + rfl + /-- The strict majority of `2 r(n)` parallel runs of an Arthur–Merlin verifier `V`, where `n` is the length of the encoded instance: the string consists of `2 r(n)` random rows of `p(n)` bits followed by `2 r(n)` replies of `q(n)` bits (`Cslib.BitString.listRow`), and `V` runs on each row followed @@ -284,6 +252,23 @@ theorem exists_arthurMerlinRepeat_ofFn_append_ofFn_iff {r p q : Polynomial ℕ} simp only [z, hi, ↓reduceDIte] exact hi.choose_spec +private theorem arthurMerlinSlice_arthurMerlinRepeat {e p q : Polynomial ℕ} + {V : α × List Bool → Bool} (a : α) + (x : Fin ((12 * e * p).eval (enc a).length) → Bool) : + repeatMajority enc (6 * e) p (arthurMerlinSlice enc q V) (a, List.ofFn x) = + arthurMerlinSlice enc (12 * e * q) (arthurMerlinRepeat enc (6 * e) p q V) + (a, List.ofFn x) := by + have hlen (s : Polynomial ℕ) : (12 * e * s).eval (enc a).length = + 2 * (6 * e).eval (enc a).length * s.eval (enc a).length := by + simp only [Polynomial.eval_mul, Polynomial.eval_ofNat] + ring + revert x + rw [hlen p] + intro x + rw [repeatMajority_ofFn, arthurMerlinSlice, hlen q] + simp only [arthurMerlinSlice, decide_eq_true_iff, + exists_arthurMerlinRepeat_ofFn_append_ofFn_iff] + /-- **Error reduction for `AM`** [Babai][Babai1985]. The strict majority of `12 e(n)` parallel runs of an Arthur–Merlin verifier, on independent blocks of random bits answered independently, errs on at most a `2 ^ (-e(n))` fraction of the random strings. -/ @@ -291,61 +276,18 @@ theorem IsArthurMerlinVerifier.repeatMajority {p q : Polynomial ℕ} {V : α × (h : IsArthurMerlinVerifier enc p q V A) (e : Polynomial ℕ) : IsArthurMerlinVerifierWithErrorExponent enc e (12 * e * p) (12 * e * q) (arthurMerlinRepeat enc (6 * e) p q V) A := by - intro a - have hlen (s : Polynomial ℕ) : (12 * e * s).eval (enc a).length = - 2 * (6 * e).eval (enc a).length * s.eval (enc a).length := by - simp only [Polynomial.eval_mul, Polynomial.eval_ofNat] - ring - have hR : (6 * e).eval (enc a).length = 6 * e.eval (enc a).length := by simp - rw [hlen p, hlen q] - -- the amplified acceptance condition is a majority vote of the original one - have hacc (x : BitString (2 * (6 * e).eval (enc a).length * p.eval (enc a).length)) : - (∃ y : BitString (2 * (6 * e).eval (enc a).length * q.eval (enc a).length), - arthurMerlinRepeat enc (6 * e) p q V (a, List.ofFn x ++ List.ofFn y) = true) ↔ - (6 * e).eval (enc a).length < #{i | ∃ z : Fin (q.eval (enc a).length) → Bool, - V (a, List.ofFn (BitString.block x i) ++ List.ofFn z) = true} := - exists_arthurMerlinRepeat_ofFn_append_ofFn_iff a x - constructor - · -- on a member, no reply is accepted only when at most `R` rows have an accepted reply - intro ha - refine (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans - (BitString.two_pow_mul_card_filter_card_filter_block_le hR - (fun s => ∃ z : Fin (q.eval (enc a).length) → Bool, - V (a, List.ofFn s ++ List.ofFn z) = true) ((h a).1 ha)) - have hx := (mem_filter.1 hx).2 - refine mem_filter.2 ⟨mem_univ _, not_lt.1 fun hlt => ?_⟩ - obtain ⟨y, hy⟩ := (hacc x).2 hlt - rw [hx y] at hy - exact Bool.false_ne_true hy - · -- on a non-member, some reply is accepted only when at most `R` rows have none - intro ha - refine (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans - (BitString.two_pow_mul_card_filter_card_filter_block_le hR - (fun s => ∀ z : Fin (q.eval (enc a).length) → Bool, - V (a, List.ofFn s ++ List.ofFn z) = false) ((h a).2 ha)) - have hx := (hacc x).1 (mem_filter.1 hx).2 - have hsum := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * - (6 * e).eval (enc a).length)))) - fun i => ∃ z : Fin (q.eval (enc a).length) → Bool, - V (a, List.ofFn (BitString.block x i) ++ List.ofFn z) = true - simp only [not_exists, Bool.not_eq_true, card_univ, Fintype.card_fin] at hsum - refine mem_filter.2 ⟨mem_univ _, ?_⟩ - omega + rw [isArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent] + have h' := (isArthurMerlinVerifier_iff_decidesWithBoundedError.1 h).repeatMajority e + exact fun a => ⟨fun ha => ((h' a).1 ha).congr (arthurMerlinSlice_arthurMerlinRepeat a), + fun ha => ((h' a).2 ha).congr (arthurMerlinSlice_arthurMerlinRepeat a)⟩ /-- Error at most `2 ^ (-e(n)) ≤ 1 / 4` is error at most `1 / 3`. -/ theorem IsArthurMerlinVerifierWithErrorExponent.isArthurMerlinVerifier {e p q : Polynomial ℕ} {V : α × List Bool → Bool} (h : IsArthurMerlinVerifierWithErrorExponent enc e p q V A) - (he : ∀ n, 2 ≤ e.eval n) : IsArthurMerlinVerifier enc p q V A := fun a => by - have h4 : 4 ≤ 2 ^ e.eval (enc a).length := - (Nat.pow_le_pow_right (by norm_num) (he _) : 2 ^ 2 ≤ _) - constructor - · intro ha - refine BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le _ ?_ - simpa only [not_exists, Bool.not_eq_true] using (Nat.mul_le_mul_right _ h4).trans ((h a).1 ha) - · intro ha - refine BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le _ ?_ - simpa only [not_forall, Bool.not_eq_false] using - (Nat.mul_le_mul_right _ h4).trans ((h a).2 ha) + (he : ∀ n, 2 ≤ e.eval n) : IsArthurMerlinVerifier enc p q V A := + isArthurMerlinVerifier_iff_decidesWithBoundedError.2 + ((isArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent.1 + h).solvesWithBoundedError he) /-- **Error reduction for `AM`** [Babai][Babai1985]: a problem is in `AM` exactly when, for every polynomial `e`, it has a polynomial-time Arthur–Merlin verifier with error at most @@ -353,16 +295,11 @@ polynomial `e`, it has a polynomial-time Arthur–Merlin verifier with error at theorem mem_AM_iff_forall_errorExponent : A ∈ AM enc ↔ ∀ e : Polynomial ℕ, ∃ (p q : Polynomial ℕ) (V : α × List Bool → Bool), ComputableInPolyTime V (encPair enc encBits) encBool ∧ - IsArthurMerlinVerifierWithErrorExponent enc e p q V A := by - have this : A ∈ AM enc ↔ ∀ e : Polynomial ℕ, ∃ (p q : Polynomial ℕ) (V : α × List Bool → Bool), - ComputableTidilyInPolyTime V (encPair enc encBits) encBool ∧ - IsArthurMerlinVerifierWithErrorExponent enc e p q V A := by - rw [mem_AM] - refine ⟨fun ⟨p, q, V, hV, h⟩ e => ⟨12 * e * p, 12 * e * q, _, - (computableInPolyTime_arthurMerlinRepeat hV _ _ _).tidy, h.repeatMajority e⟩, fun h => ?_⟩ - obtain ⟨p, q, V, hV, h⟩ := h 2 - exact ⟨p, q, V, (.of_tidy hV), h.isArthurMerlinVerifier fun _ => by simp⟩ - simpa only [computableInPolyTime_iff_computableTidilyInPolyTime] using this + IsArthurMerlinVerifierWithErrorExponent enc e p q V A := + ⟨fun ⟨p, q, V, hV, h⟩ e => ⟨12 * e * p, 12 * e * q, _, + computableInPolyTime_arthurMerlinRepeat hV _ _ _, h.repeatMajority e⟩, + fun h => let ⟨p, q, V, hV, h⟩ := h 2 + ⟨p, q, V, hV, h.isArthurMerlinVerifier fun _ => by simp⟩⟩ /-! ### `MA ⊆ AM` -/ @@ -410,7 +347,7 @@ theorem MA_subset_AM : MA enc ⊆ AM enc := by (List.ofFn r ++ List.ofFn y).take (P.eval (enc a).length) = List.ofFn y ++ List.ofFn r := by rw [List.drop_left' List.length_ofFn, List.take_left' List.length_ofFn] - simp only [hswap] + simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, hswap] have h4 : 4 ≤ 2 ^ (q + 2).eval (enc a).length := by simp only [Polynomial.eval_add, Polynomial.eval_ofNat, pow_add] exact Nat.le_mul_of_pos_left _ (by positivity) @@ -500,6 +437,7 @@ theorem MA_subset_SBP : MA enc ⊆ SBP enc := by · -- the good proof alone is accepted with three quarters of the random strings intro ha obtain ⟨y, hy⟩ := (h' a).1 ha + dsimp only [ErrorExponentAt, outcomeCount, Bool.not_true] at hy rw [Polynomial.eval_add, Polynomial.eval_ofNat] at hy exact three_mul_two_pow_le_four_mul_sum W a y hy · -- all proofs together are accepted with at most a quarter of the random strings @@ -508,7 +446,8 @@ theorem MA_subset_SBP : MA enc ⊆ SBP enc := by (f := fun u : Fin (q.eval (enc a).length) → Bool => acceptCount (fun x => W (x.1, List.ofFn u ++ x.2)) a (P.eval (enc a).length)) fun u => ?_ - simpa only [acceptCount, Polynomial.eval_add, Polynomial.eval_ofNat] using (h' a).2 ha u + simpa only [ErrorExponentAt, outcomeCount, Bool.not_false, acceptCount, Polynomial.eval_add, + Polynomial.eval_ofNat] using (h' a).2 ha u /-! ### Existential quantification -/ @@ -617,7 +556,7 @@ theorem mem_AM_of_exists {B : Set (α × List Bool)} (hB : B ∈ AM (encPair enc computableInPolyTime_existsAMVerifier hVB (pB.comp L) p, fun a => ?_⟩ -- the verifier reads the word and runs the verifier of the pairs rw [Polynomial.eval_add] - simp only [existsAMVerifier_ofFn_append] + simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, existsAMVerifier_ofFn_append] -- the error bounds of the pairs, at the length of the encoded instance have herr (w : BitString (p.eval (enc a).length)) := by have h := hB' (a, List.ofFn w) diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean index 224c3aff53..3b881d3f53 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean @@ -145,7 +145,8 @@ theorem isAlternatingVerifier_sigmaTwoVerifier {e q k p : Polynomial ℕ} {W : obtain ⟨y, hy⟩ := (h a).1 ha have hS : 2 ^ e.eval (enc a).length * #(univ.filter fun r : BitString (p.eval (enc a).length) => W (a, List.ofFn y ++ List.ofFn r) = true)ᶜ ≤ 2 ^ p.eval (enc a).length := by - simpa only [compl_filter, Bool.not_eq_true] using hy + simpa only [compl_filter, Bool.not_eq_true, ErrorExponentAt, outcomeCount, Bool.not_true] + using hy obtain ⟨u, hu⟩ := BitString.exists_forall_exists_add_mem_of_two_pow_mul_card_compl_le _ hS (hcover _) refine ⟨List.ofFn y ++ List.ofFn (BitString.blocksEquiv.symm u), by simp, fun w hw => ?_⟩ @@ -238,7 +239,8 @@ theorem isAlternatingVerifier_piTwoVerifier {e k p q : Polynomial ℕ} {W : α have hS : 2 ^ e.eval (enc a).length * #(univ.filter fun r : BitString (p.eval (enc a).length) => ∃ y : BitString (q.eval (enc a).length), W (a, List.ofFn r ++ List.ofFn y) = true)ᶜ ≤ 2 ^ p.eval (enc a).length := by - simpa only [compl_filter, not_exists, Bool.not_eq_true] using (h a).1 ha + simpa only [compl_filter, not_exists, Bool.not_eq_true, arthurMerlinRejectCount] using + (h a).1 ha obtain ⟨r, hr⟩ := BitString.exists_forall_add_notMem_of_two_pow_mul_card_le _ hS (hshifts _) (BitString.block (BitString.ofList (k.eval (enc a).length * p.eval (enc a).length) w)) have hY (i : Fin (k.eval (enc a).length)) : ∃ y : BitString (q.eval (enc a).length), diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean index e3c37d4ea2..6b0f9d1a33 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean @@ -321,6 +321,7 @@ theorem mem_AM_of_card_certifiedSet {N c : Polynomial ℕ} {R : α × List Bool (5 * N.eval (enc a).length + T.eval (enc a).length) + m.eval (enc a).length := by simp have hQ : (5 * N + T + 5 * c).eval (enc a).length = 5 * N.eval (enc a).length + T.eval (enc a).length + 5 * c.eval (enc a).length := by simp + dsimp only [arthurMerlinAcceptCount, arthurMerlinRejectCount] rw [hP, hQ] simp only [forall_verifier_eq_false_iff, exists_verifier_iff] set n := (enc a).length diff --git a/Complexity/Computability/Complexity/Classes/BPP.lean b/Complexity/Computability/Complexity/Classes/BPP.lean index ff59d83055..c5b51b110f 100644 --- a/Complexity/Computability/Complexity/Classes/BPP.lean +++ b/Complexity/Computability/Complexity/Classes/BPP.lean @@ -44,6 +44,10 @@ The probability is written as a count over the random strings, which are functio ## Main definitions +* `Cslib.Complexity.outcomeCount`: the number of strings of a given length on which a verifier + gives a specified Boolean answer. +* `Cslib.Complexity.BoundedErrorAt`: the per-instance bounded-error condition for a specified + Boolean answer. * `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError`: the bounded-error condition on a promise problem. * `Cslib.Complexity.DecidesWithBoundedError`: its specialization to a decision problem. @@ -75,6 +79,63 @@ open Turing.MultiTapeTM variable {α : Type} +/-- The number of strings `r` of length `n` with `V (a, r) = b`. -/ +@[reducible] +def outcomeCount (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : ℕ := + (Finset.univ.filter fun r : Fin n → Bool => V (a, List.ofFn r) = b).card + +/-- Verifiers that agree on an instance and all strings of length `n` have the same outcome counts +at length `n`. -/ +theorem outcomeCount_congr {V W : α × List Bool → Bool} {a : α} {n : ℕ} {b : Bool} + (h : ∀ r : Fin n → Bool, V (a, List.ofFn r) = W (a, List.ofFn r)) : + outcomeCount V a n b = outcomeCount W a n b := + congrArg Finset.card (Finset.filter_congr fun r _ => by rw [h r]) + +/-- Negating the verifier negates the counted outcome. -/ +theorem outcomeCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : + outcomeCount (fun x => !V x) a n b = outcomeCount V a n (!b) := + congrArg Finset.card (Finset.filter_congr fun _ _ => Bool.not_eq_eq_eq_not) + +/-- The strings of length `n` on which `V` gives `b` and those on which it gives `!b` partition all +`2 ^ n` strings. -/ +theorem outcomeCount_add_outcomeCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : + outcomeCount V a n b + outcomeCount V a n (!b) = 2 ^ n := by + have h := Finset.card_filter_add_card_filter_not (s := Finset.univ) + fun r : Fin n → Bool => V (a, List.ofFn r) = b + have hnot : (Finset.univ.filter fun r : Fin n → Bool => ¬V (a, List.ofFn r) = b) = + Finset.univ.filter fun r : Fin n → Bool => V (a, List.ofFn r) = !b := + Finset.filter_congr fun _ _ => by cases b <;> simp + simpa only [outcomeCount, hnot, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, + Fintype.card_fin] using h + +/-- The strings of length `n` that `V` accepts together with `a` and those it rejects partition all +`2 ^ n` strings. -/ +theorem outcomeCount_true_add_outcomeCount_false (V : α × List Bool → Bool) (a : α) (n : ℕ) : + outcomeCount V a n true + outcomeCount V a n false = 2 ^ n := + outcomeCount_add_outcomeCount_not V a n true + +/-- `V` gives the answer `b` with bounded error on the instance `a`, using random strings whose +length is `p` evaluated at the length of the encoded instance: at least two thirds of the random +strings `r` of length `p (enc a).length` give `V (a, r) = b`. -/ +@[reducible] +def BoundedErrorAt (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) + (a : α) (b : Bool) : Prop := + 2 * 2 ^ p.eval (enc a).length ≤ 3 * outcomeCount V a (p.eval (enc a).length) b + +/-- Bounded error at an instance depends only on the verifier's values on strings of length +`p(|a|)`. -/ +theorem BoundedErrorAt.congr {enc : α ↪ List Bool} {p : Polynomial ℕ} + {V W : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) + (hVW : ∀ r : Fin (p.eval (enc a).length) → Bool, V (a, List.ofFn r) = W (a, List.ofFn r)) : + BoundedErrorAt enc p W a b := by + rwa [BoundedErrorAt, ← outcomeCount_congr hVW] + +/-- Negating the verifier negates the bounded-error answer at `a`. -/ +theorem BoundedErrorAt.not {enc : α ↪ List Bool} {p : Polynomial ℕ} + {V : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) : + BoundedErrorAt enc p (fun x => !V x) a (!b) := by + rwa [BoundedErrorAt, outcomeCount_not, Bool.not_not] + namespace PromiseProblem /-- `V` solves the promise problem `Q` with bounded error, using random strings whose length is `p` @@ -84,18 +145,14 @@ random strings are accepted, and for every no-instance at least two thirds are r instances outside the promise. -/ def SolvesWithBoundedError (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (Q : PromiseProblem α) : Prop := - ∀ a, (a ∈ Q.yes → 2 * 2 ^ p.eval (enc a).length ≤ - 3 * (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn r) = true).card) ∧ - (a ∈ Q.no → 2 * 2 ^ p.eval (enc a).length ≤ - 3 * (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn r) = false).card) + ∀ a, (a ∈ Q.yes → BoundedErrorAt enc p V a true) ∧ + (a ∈ Q.no → BoundedErrorAt enc p V a false) /-- Negating the verifier solves the complement promise problem with bounded error. -/ theorem SolvesWithBoundedError.compl {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {Q : PromiseProblem α} (h : Q.SolvesWithBoundedError enc p V) : - Qᶜ.SolvesWithBoundedError enc p (fun x => !V x) := fun a => by - simpa using (h a).symm + Qᶜ.SolvesWithBoundedError enc p (fun x => !V x) := fun a => + ⟨fun ha => ((h a).2 ha).not, fun ha => ((h a).1 ha).not⟩ end PromiseProblem @@ -172,8 +229,8 @@ theorem P_subset_BPP : P enc ⊆ BPP enc := by rintro A ⟨f, hf, hA⟩ refine ⟨0, fun x => f x.1, hf.comp (.fst enc encBits), fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ - · simp [(hA a).mp ha] + · simp [BoundedErrorAt, outcomeCount, (hA a).mp ha] · have : f a = false := by simpa [hA a] using ha - simp [this] + simp [BoundedErrorAt, outcomeCount, this] end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean index 71027703ae..870a1fd2ae 100644 --- a/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean @@ -41,15 +41,19 @@ polynomial time with error at most `2 ^ (-q(n))` for every polynomial `q` ## Main definitions +* `Cslib.Complexity.ErrorExponentAt`: the per-instance condition that a verifier errs from a + specified Boolean answer on at most a `2 ^ (-q(n))` fraction of random strings. * `Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent`: error at most `2 ^ (-q(n))`. * `Cslib.Complexity.DecidesWithErrorExponent`: its specialization to a decision problem. * `Cslib.Complexity.BPP.booleanSubalgebra`: `BPP` as a Boolean subalgebra of `Set α`. ## Main results -* `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.repeatMajority`: `12 q(n)` majority +* `Cslib.Complexity.BoundedErrorAt.repeatMajority`, + `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.repeatMajority`: `12 q(n)` majority votes reduce the error to `2 ^ (-q(n))`. -* `Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent.solvesWithBoundedError`: error at most +* `Cslib.Complexity.ErrorExponentAt.boundedErrorAt`, + `Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent.solvesWithBoundedError`: error at most `2 ^ (-q(n)) ≤ 1 / 4` is bounded error. * `Cslib.Complexity.mem_PromiseBPP_iff_forall_solvesWithErrorExponent`, `Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent`: error reduction for `PromiseBPP` @@ -70,6 +74,62 @@ open Finset Turing.MultiTapeTM variable {α : Type} +/-- `V` gives the answer `b` with error at most `2 ^ (-q(n))` on the instance `a`, using random +strings whose length is `p` evaluated at the length `n` of the encoded instance: the random strings +`r` of length `p n` with `V (a, r) = !b` make up at most a `2 ^ (-q n)` fraction. -/ +@[reducible] +def ErrorExponentAt (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) + (a : α) (b : Bool) : Prop := + 2 ^ q.eval (enc a).length * outcomeCount V a (p.eval (enc a).length) (!b) ≤ + 2 ^ p.eval (enc a).length + +/-- An error-exponent bound at an instance depends only on the verifier's values on strings of +length `p(|a|)`. -/ +theorem ErrorExponentAt.congr {enc : α ↪ List Bool} {q p : Polynomial ℕ} + {V W : α × List Bool → Bool} {a : α} {b : Bool} (h : ErrorExponentAt enc q p V a b) + (hVW : ∀ r : Fin (p.eval (enc a).length) → Bool, V (a, List.ofFn r) = W (a, List.ofFn r)) : + ErrorExponentAt enc q p W a b := by + rwa [ErrorExponentAt, ← outcomeCount_congr hVW] + +/-- **Per-instance error reduction for bounded error**: the strict majority of `12 q(n)` runs of a +verifier on independent blocks of random bits errs from `b` on at most a `2 ^ (-q(n))` fraction of +the random strings whenever a single run produces `b` on at least two thirds of them. -/ +theorem BoundedErrorAt.repeatMajority {enc : α ↪ List Bool} {p : Polynomial ℕ} + {V : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) + (q : Polynomial ℕ) : + ErrorExponentAt enc q (12 * q * p) (Complexity.repeatMajority enc (6 * q) p V) a b := by + unfold ErrorExponentAt outcomeCount + have hlen : (12 * q * p).eval (enc a).length = + 2 * (6 * q).eval (enc a).length * p.eval (enc a).length := by + simp only [Polynomial.eval_mul, Polynomial.eval_ofNat] + ring + have hR : (6 * q).eval (enc a).length = 6 * q.eval (enc a).length := by simp + rw [hlen] + refine (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans + (BitString.two_pow_mul_card_filter_card_filter_block_le hR + (fun s => V (a, List.ofFn s) = b) h) + rw [mem_filter, repeatMajority_ofFn] at hx + cases b + · rw [Bool.not_false, decide_eq_true_iff] at hx + have hsum := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * + (6 * q).eval (enc a).length)))) + fun i => V (a, List.ofFn (BitString.block x i)) = true + simp only [Bool.not_eq_true, card_univ, Fintype.card_fin] at hsum + refine mem_filter.2 ⟨mem_univ _, ?_⟩ + omega + · rw [Bool.not_true, decide_eq_false_iff_not, not_lt] at hx + exact mem_filter.2 ⟨mem_univ _, hx.2⟩ + +/-- Error at most `2 ^ (-q(n)) ≤ 1 / 4` on an instance is bounded error on that instance. -/ +theorem ErrorExponentAt.boundedErrorAt {enc : α ↪ List Bool} {q p : Polynomial ℕ} + {V : α × List Bool → Bool} {a : α} {b : Bool} (h : ErrorExponentAt enc q p V a b) + (hq : 2 ≤ q.eval (enc a).length) : BoundedErrorAt enc p V a b := by + have hsum := outcomeCount_add_outcomeCount_not V a (p.eval (enc a).length) b + have h4 : 2 ^ 2 ≤ 2 ^ q.eval (enc a).length := Nat.pow_le_pow_right (by norm_num) hq + have hle := (Nat.mul_le_mul_right _ h4).trans h + unfold BoundedErrorAt + omega + namespace PromiseProblem /-- `V` solves the promise problem `Q` with error at most `2 ^ (-q(n))`, using random strings whose @@ -78,12 +138,8 @@ rejected random strings, and for every no-instance the accepted ones, make up at `2 ^ (-q(n))` fraction. Nothing is required on instances outside the promise. -/ def SolvesWithErrorExponent (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (Q : PromiseProblem α) : Prop := - ∀ a, (a ∈ Q.yes → 2 ^ q.eval (enc a).length * - (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn r) = false).card ≤ 2 ^ p.eval (enc a).length) ∧ - (a ∈ Q.no → 2 ^ q.eval (enc a).length * - (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => - V (a, List.ofFn r) = true).card ≤ 2 ^ p.eval (enc a).length) + ∀ a, (a ∈ Q.yes → ErrorExponentAt enc q p V a true) ∧ + (a ∈ Q.no → ErrorExponentAt enc q p V a false) variable {enc : α ↪ List Bool} {Q : PromiseProblem α} @@ -93,50 +149,15 @@ promise problems. The strict majority of `12 q(n)` runs of a bounded-error solve blocks of random bits, errs on at most a `2 ^ (-q(n))` fraction of the random strings. -/ theorem SolvesWithBoundedError.repeatMajority {p : Polynomial ℕ} {V : α × List Bool → Bool} (h : Q.SolvesWithBoundedError enc p V) (q : Polynomial ℕ) : - Q.SolvesWithErrorExponent enc q (12 * q * p) (Complexity.repeatMajority enc (6 * q) p V) := by - intro a - have hlen : (12 * q * p).eval (enc a).length = - 2 * (6 * q).eval (enc a).length * p.eval (enc a).length := by - simp only [Polynomial.eval_mul, Polynomial.eval_ofNat] - ring - have hR : (6 * q).eval (enc a).length = 6 * q.eval (enc a).length := by simp - rw [hlen] - constructor - · -- on a yes-instance, the majority rejects only when at most `R` runs accept - intro ha - refine (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans - (BitString.two_pow_mul_card_filter_card_filter_block_le hR - (fun s => V (a, List.ofFn s) = true) ((h a).1 ha)) - rw [mem_filter, repeatMajority_ofFn, decide_eq_false_iff_not, not_lt] at hx - exact mem_filter.2 ⟨mem_univ _, hx.2⟩ - · -- on a no-instance, the majority accepts only when at most `R` runs reject - intro ha - refine (Nat.mul_le_mul_left _ (card_le_card fun x hx => ?_)).trans - (BitString.two_pow_mul_card_filter_card_filter_block_le hR - (fun s => V (a, List.ofFn s) = false) ((h a).2 ha)) - rw [mem_filter, repeatMajority_ofFn, decide_eq_true_iff] at hx - have hsum := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * - (6 * q).eval (enc a).length)))) - fun i => V (a, List.ofFn (BitString.block x i)) = true - simp only [Bool.not_eq_true, card_univ, Fintype.card_fin] at hsum - refine mem_filter.2 ⟨mem_univ _, ?_⟩ - omega + Q.SolvesWithErrorExponent enc q (12 * q * p) (Complexity.repeatMajority enc (6 * q) p V) := + fun a => ⟨fun ha => ((h a).1 ha).repeatMajority q, fun ha => ((h a).2 ha).repeatMajority q⟩ /-- Error at most `2 ^ (-q(n)) ≤ 1 / 4` is bounded error. -/ theorem SolvesWithErrorExponent.solvesWithBoundedError {q p : Polynomial ℕ} {V : α × List Bool → Bool} (h : Q.SolvesWithErrorExponent enc q p V) - (hq : ∀ n, 2 ≤ q.eval n) : Q.SolvesWithBoundedError enc p V := fun a => by - have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length) - have h4 : 2 ^ 2 ≤ 2 ^ q.eval (enc a).length := Nat.pow_le_pow_right (by norm_num) (hq _) - rw [← acceptCount] - constructor - · intro ha - have := (Nat.mul_le_mul_right _ h4).trans ((h a).1 ha) - omega - · intro ha - have := (Nat.mul_le_mul_right _ h4).trans ((h a).2 ha) - rw [← acceptCount] at this - omega + (hq : ∀ n, 2 ≤ q.eval n) : Q.SolvesWithBoundedError enc p V := + fun a => ⟨fun ha => ((h a).1 ha).boundedErrorAt (hq _), + fun ha => ((h a).2 ha).boundedErrorAt (hq _)⟩ end PromiseProblem @@ -182,44 +203,45 @@ theorem inter_mem_BPP {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : obtain ⟨p₂, V₂, hV₂, h₂⟩ := mem_BPP_iff_forall_decidesWithErrorExponent.1 hB 3 refine mem_BPP.2 ⟨p₁ + p₂, andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂, by fun_prop, fun a => ?_⟩ - have hs₁ := acceptCount_add_card_filter_eq_false (V := V₁) (a := a) - (n := p₁.eval (enc a).length) - have hs₂ := acceptCount_add_card_filter_eq_false (V := V₂) (a := a) - (n := p₂.eval (enc a).length) - have hs := acceptCount_add_card_filter_eq_false - (V := andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) (a := a) - (n := (p₁ + p₂).eval (enc a).length) - have hc : acceptCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a - ((p₁ + p₂).eval (enc a).length) = - acceptCount V₁ a (p₁.eval (enc a).length) * acceptCount V₂ a (p₂.eval (enc a).length) := by - rw [Polynomial.eval_add, acceptCount_andVerifier] + have hs₁ := outcomeCount_true_add_outcomeCount_false V₁ a (p₁.eval (enc a).length) + have hs₂ := outcomeCount_true_add_outcomeCount_false V₂ a (p₂.eval (enc a).length) + have hs := outcomeCount_true_add_outcomeCount_false + (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a ((p₁ + p₂).eval (enc a).length) + have hc : outcomeCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a + ((p₁ + p₂).eval (enc a).length) true = + outcomeCount V₁ a (p₁.eval (enc a).length) true * + outcomeCount V₂ a (p₂.eval (enc a).length) true := by + rw [Polynomial.eval_add] + exact acceptCount_andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂ a (p₂.eval (enc a).length) constructor · intro ha have e₁ := (h₁ a).1 ha.1 have e₂ := (h₂ a).1 ha.2 - simp only [Polynomial.eval_ofNat] at e₁ e₂ - have f₁ : 7 * 2 ^ p₁.eval (enc a).length ≤ 8 * acceptCount V₁ a (p₁.eval (enc a).length) := by - omega - have f₂ : 7 * 2 ^ p₂.eval (enc a).length ≤ 8 * acceptCount V₂ a (p₂.eval (enc a).length) := by - omega - rw [← acceptCount, hc, Polynomial.eval_add, pow_add] + simp only [ErrorExponentAt, Bool.not_true, Polynomial.eval_ofNat] at e₁ e₂ + have f₁ : 7 * 2 ^ p₁.eval (enc a).length ≤ + 8 * outcomeCount V₁ a (p₁.eval (enc a).length) true := by omega + have f₂ : 7 * 2 ^ p₂.eval (enc a).length ≤ + 8 * outcomeCount V₂ a (p₂.eval (enc a).length) true := by omega + unfold BoundedErrorAt + rw [hc, Polynomial.eval_add, pow_add] nlinarith [Nat.mul_le_mul f₁ f₂] · intro ha - have hacc : 8 * acceptCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a - ((p₁ + p₂).eval (enc a).length) ≤ 2 ^ (p₁ + p₂).eval (enc a).length := by + have hacc : 8 * outcomeCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a + ((p₁ + p₂).eval (enc a).length) true ≤ 2 ^ (p₁ + p₂).eval (enc a).length := by rw [hc, Polynomial.eval_add, pow_add] by_cases ha₁ : a ∈ A · have ha₂ : a ∉ B := fun hb => ha ⟨ha₁, hb⟩ have e₂ := (h₂ a).2 ha₂ - simp only [Polynomial.eval_ofNat] at e₂ - rw [← acceptCount] at e₂ - have hb₁ := acceptCount_le_two_pow (V := V₁) (a := a) (n := p₁.eval (enc a).length) + simp only [ErrorExponentAt, Bool.not_false, Polynomial.eval_ofNat] at e₂ + have hb₁ : outcomeCount V₁ a (p₁.eval (enc a).length) true ≤ + 2 ^ p₁.eval (enc a).length := by omega nlinarith [Nat.mul_le_mul hb₁ e₂] · have e₁ := (h₁ a).2 ha₁ - simp only [Polynomial.eval_ofNat] at e₁ - rw [← acceptCount] at e₁ - have hb₂ := acceptCount_le_two_pow (V := V₂) (a := a) (n := p₂.eval (enc a).length) + simp only [ErrorExponentAt, Bool.not_false, Polynomial.eval_ofNat] at e₁ + have hb₂ : outcomeCount V₂ a (p₂.eval (enc a).length) true ≤ + 2 ^ p₂.eval (enc a).length := by omega nlinarith [Nat.mul_le_mul e₁ hb₂] + unfold BoundedErrorAt omega /-- `BPP` as a Boolean subalgebra of `Set α`. -/ diff --git a/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean b/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean index 4a1dd81569..5d6da544a7 100644 --- a/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean +++ b/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean @@ -62,6 +62,8 @@ theorem PolyTimeReducible.mem_BPP (h : PolyTimeReducible enc encB A B) (hB : B (hW.comp ((hg.comp (.fst enc encBits)).prod (.snd enc encBits))) (.const true)), fun a => ?_⟩ obtain ⟨j, hj⟩ := Nat.exists_eq_add_of_le (hle a) + dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt, + outcomeCount] rw [hj] set k := q.eval (encB (g a)).length set V := andVerifier (fun a => q.eval (encB (g a)).length) (fun x => W (g x.1, x.2)) @@ -85,7 +87,10 @@ theorem PolyTimeReducible.mem_BPP (h : PolyTimeReducible enc encB A B) (hB : B · have h : 2 * 2 ^ k ≤ 3 * acceptCount W (g a) k := (hWB (g a)).1 ((hAB a).1 ha) have := Nat.mul_le_mul_right (2 ^ j) h linarith - · have := Nat.mul_le_mul_right (2 ^ j) ((hWB (g a)).2 fun hgB => ha ((hAB a).2 hgB)) + · have h : 2 * 2 ^ k ≤ + 3 * (Finset.univ.filter fun r : Fin k → Bool => W (g a, List.ofFn r) = false).card := + (hWB (g a)).2 fun hgB => ha ((hAB a).2 hgB) + have := Nat.mul_le_mul_right (2 ^ j) h linarith end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/IP.lean b/Complexity/Computability/Complexity/Classes/IP.lean index ec46dcf264..6ce6e4a498 100644 --- a/Complexity/Computability/Complexity/Classes/IP.lean +++ b/Complexity/Computability/Complexity/Classes/IP.lean @@ -296,13 +296,12 @@ theorem BPP_subset_IP (enc : α ↪ List Bool) : BPP enc ⊆ IP enc := by refine ⟨_, isOraclePPTOn_bppVerifier (p := p) hV.tidy, fun a ha => ⟨Prover.const [], ?_⟩, fun a ha P => ?_⟩ <;> rw [acceptProb_bppVerifier] · have h := (hA a).1 ha + unfold BoundedErrorAt outcomeCount at h exact_mod_cast natCast_div_le_natCast_div (a := 2) (b := 3) (d := 2 ^ p.eval (enc a).length) three_ne_zero (pow_pos two_pos _).ne' (by omega) · have h := (hA a).2 ha - have hsum := Finset.card_filter_add_card_filter_not (s := Finset.univ) - (fun r : Fin (p.eval (enc a).length) → Bool => V (a, List.ofFn r) = true) - simp only [Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, - Fintype.card_fin] at hsum + have hsum := outcomeCount_true_add_outcomeCount_false V a (p.eval (enc a).length) + unfold BoundedErrorAt outcomeCount at h hsum exact_mod_cast natCast_div_le_natCast_div (c := 1) (d := 3) (b := 2 ^ p.eval (enc a).length) (pow_pos two_pos _).ne' three_ne_zero (by omega) diff --git a/Complexity/Computability/Complexity/Classes/PP.lean b/Complexity/Computability/Complexity/Classes/PP.lean index c1b06ae0d3..c24a2cacc8 100644 --- a/Complexity/Computability/Complexity/Classes/PP.lean +++ b/Complexity/Computability/Complexity/Classes/PP.lean @@ -77,16 +77,18 @@ strings accepts the members of its problem, and only them, on more than half. -/ theorem DecidesWithBoundedError.decidesByMajority {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (h : DecidesWithBoundedError enc p V A) : DecidesByMajority enc p V A := by intro a - have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length) + have hsum := outcomeCount_true_add_outcomeCount_false V a (p.eval (enc a).length) have hpos := Nat.one_le_two_pow (n := p.eval (enc a).length) + change a ∈ A ↔ 2 ^ p.eval (enc a).length < 2 * outcomeCount V a (p.eval (enc a).length) true constructor · intro ha have := (h a).1 ha - rw [← acceptCount] at this + unfold BoundedErrorAt at this omega · intro hlt by_contra ha have := (h a).2 ha + unfold BoundedErrorAt at this omega /-- **`BPP ⊆ PP`.** -/ diff --git a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean index 67adc0add1..5991d20f3a 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean @@ -175,6 +175,7 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔ fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ · have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (enc a).length = c * ((enc a).length + 1) ^ d := by simp + dsimp only [BoundedErrorAt, outcomeCount] rw [hp] have hprob := hyes a ha rw [hlaw a, uniformList_acceptCount_toReal (V := fun x => evalM x.1 x.2), @@ -185,6 +186,7 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔ exact_mod_cast h3 · have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (enc a).length = c * ((enc a).length + 1) ^ d := by simp + dsimp only [BoundedErrorAt, outcomeCount] rw [hp] have hprob := hno a ha have hmap : ProbComp.eval (Bool.not <$> M a) = diff --git a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean index e57e860172..cfaefc71af 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean @@ -495,14 +495,14 @@ theorem RPReducible.mem_PromiseBPP (hXY : RPReducible encA encB X Y) have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := b) (n := p.eval (encB b).length) have h := (hYV b).1 hb - simp only [Polynomial.eval_ofNat] at h + simp only [ErrorExponentAt, outcomeCount, Bool.not_true, Polynomial.eval_ofNat] at h have h' : (7 : ℝ) * 2 ^ p.eval (encB b).length ≤ 8 * acceptCount V b (p.eval (encB b).length) := by exact_mod_cast (by omega) linarith have hMno (b : β) (hb : b ∈ Y.no) : Pr[M b] ≤ 1 / 8 := by rw [probability_sampleList_verifier, div_le_iff₀ (by positivity)] have h := (hYV b).2 hb - simp only [Polynomial.eval_ofNat] at h + simp only [ErrorExponentAt, outcomeCount, Bool.not_false, Polynomial.eval_ofNat] at h rw [← acceptCount] at h have h' : (8 : ℝ) * acceptCount V b (p.eval (encB b).length) ≤ 2 ^ p.eval (encB b).length := by exact_mod_cast h diff --git a/Complexity/Computability/Complexity/Classes/RP.lean b/Complexity/Computability/Complexity/Classes/RP.lean index 0284ccf388..432f40cae3 100644 --- a/Complexity/Computability/Complexity/Classes/RP.lean +++ b/Complexity/Computability/Complexity/Classes/RP.lean @@ -271,6 +271,7 @@ theorem solvesWithOneSidedError (h : Q.SolvesWithOneSidedErrorExponent enc q p V theorem solvesWithErrorExponent (h : Q.SolvesWithOneSidedErrorExponent enc q p V) : Q.SolvesWithErrorExponent enc q p V := fun a => by refine ⟨(h a).1, fun ha => ?_⟩ + simp only [ErrorExponentAt, outcomeCount, Bool.not_false] rw [Finset.filter_false_of_mem fun r _ => by simp [(h a).2 ha r]] simp diff --git a/Complexity/Computability/Complexity/Classes/SBP.lean b/Complexity/Computability/Complexity/Classes/SBP.lean index 28d3b18122..701406962d 100644 --- a/Complexity/Computability/Complexity/Classes/SBP.lean +++ b/Complexity/Computability/Complexity/Classes/SBP.lean @@ -114,14 +114,15 @@ theorem BPP_subset_SBP : BPP enc ⊆ SBP enc := by (n := p.eval (enc a).length) have hp : 0 < 2 ^ p.eval (enc a).length := by positivity have h := hA a - simp only [Polynomial.eval_ofNat] at h + simp only [ErrorExponentAt, Bool.not_true, Bool.not_false, Polynomial.eval_ofNat] at h change (a ∈ A → _ ≤ 3 * acceptCount V a (p.eval (enc a).length)) ∧ _ constructor <;> intro ha · have := h.1 ha + unfold outcomeCount at this lia · have := h.2 ha change 2 * (3 * acceptCount V a (p.eval (enc a).length)) < _ - rw [← acceptCount] at this + change _ * acceptCount V a (p.eval (enc a).length) ≤ _ at this lia /-- The integer gap `2f - k + 1` is positive exactly on members, including zero thresholds. -/ @@ -217,7 +218,8 @@ theorem inter_mem_SBP_of_mem_BPP (hA : A ∈ SBP enc) (hB : B ∈ BPP enc) : have hD : 0 < 2 ^ q.eval (enc a).length := by positivity have hp1 : 1 ≤ 2 ^ p.eval (enc a).length := Nat.one_le_pow _ _ (by decide) have h := hB a - simp only [Polynomial.eval_add, Polynomial.eval_ofNat, pow_add] at h + simp only [ErrorExponentAt, Bool.not_true, Bool.not_false, outcomeCount, + Polynomial.eval_add, Polynomial.eval_ofNat, pow_add] at h change (a ∈ A ∩ B → 3 * (k a * 2 ^ q.eval (enc a).length) ≤ 4 * (f a * c a)) ∧ (a ∉ A ∩ B → 2 * (4 * (f a * c a)) < 3 * (k a * 2 ^ q.eval (enc a).length)) constructor diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean index 1952b4624c..e824152b22 100644 --- a/Complexity/Computability/Complexity/Classes/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Time.lean @@ -459,6 +459,8 @@ theorem mem_BPP_iff_exists_mem_BPTIME {α : Type} {enc : α ↪ List Bool} {A : have hprob := (hA a).2 rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, two_thirds_le_div_iff] at hprob + dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt, + outcomeCount] rw [heval] constructor · intro (ha : a ∈ A) diff --git a/Complexity/Computability/Complexity/Classes/Toda.lean b/Complexity/Computability/Complexity/Classes/Toda.lean index bb1385c1ec..811ca0eab6 100644 --- a/Complexity/Computability/Complexity/Classes/Toda.lean +++ b/Complexity/Computability/Complexity/Classes/Toda.lean @@ -83,6 +83,7 @@ theorem exists_SharpP_testBit_of_mem_BPOp_ParityP {L : Set α} rw [length_encPair, hZp, Polynomial.eval_comp] simp [hr] obtain ⟨hyes, hno⟩ := hdec a + dsimp only [BoundedErrorAt, outcomeCount] at hyes hno simp only [decide_eq_true_eq, decide_eq_false_iff_not, hL', hZlen _ List.length_ofFn] at hyes hno simp only diff --git a/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean b/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean index f53ec5e865..977b3b0c8a 100644 --- a/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean +++ b/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean @@ -539,7 +539,8 @@ theorem PH_subset_BPOp_ParityP : PH enc ⊆ BPOp enc (ParityP (encPair enc encBi (s := (univ : Finset (Fin (ρ.eval (enc a).length) → Bool))) (fun r => Odd (acceptCount (fun x => W (x.1, List.ofFn r ++ x.2)) a (ζ.eval (enc a).length))) simp only [card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_fin] at hsplit - simp only [hL', Set.mem_ofPred_eq, decide_eq_true_eq, decide_eq_false_iff_not] + simp only [BoundedErrorAt, outcomeCount, hL', Set.mem_ofPred_eq, decide_eq_true_eq, + decide_eq_false_iff_not] rw [← hLV a] at ha constructor · intro (haL : a ∈ L) diff --git a/ComplexityTests/ArthurMerlin.lean b/ComplexityTests/ArthurMerlin.lean index 2c121316f2..351529c2b7 100644 --- a/ComplexityTests/ArthurMerlin.lean +++ b/ComplexityTests/ArthurMerlin.lean @@ -37,9 +37,11 @@ private theorem head_mem_MA_direct : {w : List Bool | w.headD false = true} ∈ decide refine ⟨1, 1, fun x => x.1.headD false, by fun_prop, fun w => ⟨fun hw => ?_, fun hw y => ?_⟩⟩ · refine ⟨fun _ => true, ?_⟩ + dsimp only [BoundedErrorAt, outcomeCount] rw [Finset.filter_true_of_mem fun r _ => by simpa using hw] exact hcard w - · rw [Finset.filter_true_of_mem fun r _ => by simpa using hw] + · dsimp only [BoundedErrorAt, outcomeCount] + rw [Finset.filter_true_of_mem fun r _ => by simpa using hw] exact hcard w example : {w : List Bool | w.headD false = true} ∈ AM encBits := MA_subset_AM head_mem_MA_direct @@ -105,4 +107,16 @@ example (h : PolyTimeReducible encCNF (encPair encGraph encGraph) SAT GraphIsomo PH_eq_SigmaP_two_of_npComplete_GraphIsomorphism ⟨GraphIsomorphism.mem_NP, CookLevin.SAT_npHard.trans h⟩ +/-- `IsArthurMerlinVerifier` and `IsArthurMerlinVerifierWithErrorExponent` reduce to `BPP`'s +bounded-error and error-exponent predicates on `arthurMerlinSlice`. -/ +example {p q : Polynomial ℕ} {V : List Bool × List Bool → Bool} {A : Set (List Bool)} : + IsArthurMerlinVerifier encBits p q V A ↔ + DecidesWithBoundedError encBits p (arthurMerlinSlice encBits q V) A := + isArthurMerlinVerifier_iff_decidesWithBoundedError + +example {e p q : Polynomial ℕ} {V : List Bool × List Bool → Bool} {A : Set (List Bool)} : + IsArthurMerlinVerifierWithErrorExponent encBits e p q V A ↔ + DecidesWithErrorExponent encBits e p (arthurMerlinSlice encBits q V) A := + isArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent + end ComplexityTests.ArthurMerlin diff --git a/ComplexityTests/InteractiveProofs.lean b/ComplexityTests/InteractiveProofs.lean index 0c8330298b..8eb0b49910 100644 --- a/ComplexityTests/InteractiveProofs.lean +++ b/ComplexityTests/InteractiveProofs.lean @@ -126,7 +126,7 @@ example (a : List Bool) : example : (∅ : Set (List Bool)) ∈ IP encBits := BPP_subset_IP _ ⟨0, fun _ => false, .const false, fun _ => ⟨fun h => h.elim, fun _ => by - simp only [Polynomial.eval_zero, pow_zero, mul_one] + simp only [BoundedErrorAt, outcomeCount, Polynomial.eval_zero, pow_zero, mul_one] exact le_trans (by norm_num : 2 ≤ 3 * 1) (Nat.mul_le_mul_left 3 (Finset.card_pos.2 ⟨fun _ => false, Finset.mem_filter.2 ⟨Finset.mem_univ _, trivial⟩⟩))⟩⟩ diff --git a/ComplexityTests/NonVacuity.lean b/ComplexityTests/NonVacuity.lean index 16163ce70b..b6a32ae66a 100644 --- a/ComplexityTests/NonVacuity.lean +++ b/ComplexityTests/NonVacuity.lean @@ -92,7 +92,7 @@ example : (Set.univ : Set (List Bool)) ∈ NP encBits := example : (∅ : Set (List Bool)) ∈ BPP encBits := ⟨0, fun _ => false, .const false, fun _ => ⟨fun h => h.elim, fun _ => by - simp only [Polynomial.eval_zero, pow_zero, mul_one] + simp only [BoundedErrorAt, outcomeCount, Polynomial.eval_zero, pow_zero, mul_one] exact le_trans (by norm_num : 2 ≤ 3 * 1) (Nat.mul_le_mul_left 3 (Finset.card_pos.2 ⟨fun _ => false, Finset.mem_filter.2 ⟨Finset.mem_univ _, trivial⟩⟩))⟩⟩ @@ -109,7 +109,7 @@ example : (⊤ : Language Bool) ∈ PPoly := example : (⊥ : Language Bool) ∈ PPoly := mem_PPolyOn_encBits_iff.1 (BPP_subset_PPolyOn ⟨0, fun _ => false, .const false, fun _ => ⟨fun h => h.elim, fun _ => by - simp only [Polynomial.eval_zero, pow_zero, mul_one] + simp only [BoundedErrorAt, outcomeCount, Polynomial.eval_zero, pow_zero, mul_one] exact le_trans (by norm_num : 2 ≤ 3 * 1) (Nat.mul_le_mul_left 3 (Finset.card_pos.2 ⟨fun _ => false, Finset.mem_filter.2 ⟨Finset.mem_univ _, trivial⟩⟩))⟩⟩) diff --git a/ComplexityTests/ResourceClasses4.lean b/ComplexityTests/ResourceClasses4.lean index d4ef0ccbdd..bc1dd9c8ff 100644 --- a/ComplexityTests/ResourceClasses4.lean +++ b/ComplexityTests/ResourceClasses4.lean @@ -80,10 +80,10 @@ theorem decidesWithBoundedError_orAnd : DecidesWithBoundedError encBits 2 orAnd decide rcases ha : a.headD false · refine ⟨fun h => absurd (ha.symm.trans h) Bool.false_ne_true, fun _ => ?_⟩ - simp only [orAnd, ha, Bool.false_eq_true, ↓reduceIte] + simp only [BoundedErrorAt, outcomeCount, orAnd, ha, Bool.false_eq_true, ↓reduceIte] exact hand _ (Polynomial.eval_ofNat 2 _) · refine ⟨fun _ => ?_, fun h => absurd ha h⟩ - simp only [orAnd, ha, ↓reduceIte] + simp only [BoundedErrorAt, outcomeCount, orAnd, ha, ↓reduceIte] exact hor _ (Polynomial.eval_ofNat 2 _) /-- Majority votes of `12 q(n)` runs of `orAnd` decide `startsTrue` with error at most diff --git a/ComplexityTests/SipserLautemann.lean b/ComplexityTests/SipserLautemann.lean index 7fa50a1791..657e22280a 100644 --- a/ComplexityTests/SipserLautemann.lean +++ b/ComplexityTests/SipserLautemann.lean @@ -80,6 +80,8 @@ theorem noisyHeadVerifier_decides : DecidesWithBoundedError encBits (Polynomial.C 2) noisyHeadVerifier {x : List Bool | x.headD false = true} := by intro a + dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt, + outcomeCount] generalize hm : (Polynomial.C 2).eval (encBits a).length = m have hm2 : m = 2 := by rw [← hm, Polynomial.eval_C] subst hm2 From 22d5cc563cecfef992c2ae5a95e30b46128ce174 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 03:35:59 +0000 Subject: [PATCH 2/3] refactor(ArthurMerlin): drop outcomeCount/AM count aliases and address review (#949) --- .../Circuit/Boolean/PolynomialTime.lean | 2 +- .../Complexity/Classes/ArthurMerlin.lean | 49 ++++---------- .../Classes/ArthurMerlin/Amplification.lean | 19 +++--- .../Complexity/Classes/ArthurMerlin/PH.lean | 5 +- .../Classes/ArthurMerlin/SetLowerBound.lean | 1 - .../Computability/Complexity/Classes/BPP.lean | 65 ++++++------------- .../Complexity/Classes/BPP/Amplification.lean | 62 +++++++++++------- .../Complexity/Classes/BPP/Reduction.lean | 3 +- .../Computability/Complexity/Classes/IP.lean | 9 ++- .../Computability/Complexity/Classes/PP.lean | 4 +- .../Classes/Promise/Probabilistic.lean | 4 +- .../Classes/Promise/Randomized.lean | 4 +- .../Computability/Complexity/Classes/RP.lean | 2 +- .../Computability/Complexity/Classes/SBP.lean | 5 +- .../Complexity/Classes/Time.lean | 3 +- .../Complexity/Classes/Toda.lean | 2 +- .../Complexity/Classes/Toda/Hierarchy.lean | 2 +- ComplexityTests/ArthurMerlin.lean | 4 +- ComplexityTests/InteractiveProofs.lean | 2 +- ComplexityTests/NonVacuity.lean | 4 +- ComplexityTests/ResourceClasses4.lean | 4 +- ComplexityTests/SipserLautemann.lean | 3 +- 22 files changed, 111 insertions(+), 147 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean b/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean index ba5b4a224e..4fb996a2ac 100644 --- a/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean +++ b/Complexity/Computability/Circuit/Boolean/PolynomialTime.lean @@ -179,7 +179,7 @@ theorem BPP_subset_PPolyOn : Complexity.BPP enc ⊆ PPolyOn enc := by (polynomiallyBounded_complexity_framedSlice hL' (by fun_prop)) (encodes enc) (encodesMember enc A) fun n x ⟨a, ha⟩ => by have h := hdec a - dsimp only [Complexity.BoundedErrorAt, Complexity.outcomeCount] at h + dsimp only [Complexity.BoundedErrorAt] at h rw [ha, List.length_ofFn] at h by_cases haA : a ∈ A · rw [(encodesMember_eq_true_iff ha).2 haA] diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean index 4a61b1a962..7b4888b195 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin.lean @@ -53,9 +53,7 @@ the second level of the polynomial hierarchy in ## Main definitions * `Cslib.Complexity.IsMerlinArthurVerifier`, `Cslib.Complexity.MA`. -* `Cslib.Complexity.arthurMerlinAcceptCount`, `Cslib.Complexity.arthurMerlinRejectCount`, - `Cslib.Complexity.arthurMerlinSlice`: per-instance Arthur–Merlin coin counts and reply-existence - verifier. +* `Cslib.Complexity.arthurMerlinSlice`: reply-existence counting slice of an Arthur–Merlin verifier. * `Cslib.Complexity.IsArthurMerlinVerifier`, `Cslib.Complexity.AM`. ## Main results @@ -108,38 +106,13 @@ theorem mem_MA : A ∈ MA enc ↔ ∃ (q p : Polynomial ℕ) (V : α × List Boo /-! ### Arthur–Merlin -/ -/-- The number of random strings `r` of length `m` for which some reply `y` of length `n` is -accepted by `V` on `a`. -/ -@[reducible] -def arthurMerlinAcceptCount (V : α × List Bool → Bool) (a : α) (m n : ℕ) : ℕ := - (univ.filter fun r : Fin m → Bool => - ∃ y : Fin n → Bool, V (a, List.ofFn r ++ List.ofFn y) = true).card - -/-- The number of random strings `r` of length `m` for which every reply `y` of length `n` is -rejected by `V` on `a`. -/ -@[reducible] -def arthurMerlinRejectCount (V : α × List Bool → Bool) (a : α) (m n : ℕ) : ℕ := - (univ.filter fun r : Fin m → Bool => - ∀ y : Fin n → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card - -/-- Whether some reply `y` of length `q(|x.1|)` is accepted by `V` on `(x.1, x.2 ++ y)`. -/ +/-- Whether some reply `y` of length `q(|x.1|)` is accepted by `V` on `(x.1, x.2 ++ y)`. +This is a counting device rather than a polynomial-time verifier: it quantifies over all +`2 ^ q(|x.1|)` replies, and `DecidesWithBoundedError` carries no computability requirement. -/ def arthurMerlinSlice (enc : α ↪ List Bool) (q : Polynomial ℕ) (V : α × List Bool → Bool) (x : α × List Bool) : Bool := decide (∃ y : Fin (q.eval (enc x.1).length) → Bool, V (x.1, x.2 ++ List.ofFn y) = true) -theorem arthurMerlinAcceptCount_eq_outcomeCount (enc : α ↪ List Bool) (q : Polynomial ℕ) - (V : α × List Bool → Bool) (a : α) (m : ℕ) : - arthurMerlinAcceptCount V a m (q.eval (enc a).length) = - outcomeCount (arthurMerlinSlice enc q V) a m true := by - simp only [arthurMerlinAcceptCount, outcomeCount, arthurMerlinSlice, decide_eq_true_iff] - -theorem arthurMerlinRejectCount_eq_outcomeCount (enc : α ↪ List Bool) (q : Polynomial ℕ) - (V : α × List Bool → Bool) (a : α) (m : ℕ) : - arthurMerlinRejectCount V a m (q.eval (enc a).length) = - outcomeCount (arthurMerlinSlice enc q V) a m false := by - simp only [arthurMerlinRejectCount, outcomeCount, arthurMerlinSlice, decide_eq_false_iff_not, - not_exists, Bool.not_eq_true] - /-- `V` is an Arthur–Merlin verifier for `A`, with random strings of length `p` and replies of length `q`, both evaluated at the length of the encoded instance: on a member `a` at least two thirds of the random strings `r` have a reply `y` with `V (a, r ++ y) = true`; on a non-member at @@ -147,9 +120,11 @@ least two thirds of them have none. -/ def IsArthurMerlinVerifier (enc : α ↪ List Bool) (p q : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop := ∀ a, (a ∈ A → 2 * 2 ^ p.eval (enc a).length ≤ - 3 * arthurMerlinAcceptCount V a (p.eval (enc a).length) (q.eval (enc a).length)) ∧ + 3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + ∃ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = true).card) ∧ (a ∉ A → 2 * 2 ^ p.eval (enc a).length ≤ - 3 * arthurMerlinRejectCount V a (p.eval (enc a).length) (q.eval (enc a).length)) + 3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + ∀ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card) /-- An Arthur–Merlin verifier is a bounded-error decider when composed with existential quantification over Merlin's reply. -/ @@ -158,8 +133,8 @@ theorem isArthurMerlinVerifier_iff_decidesWithBoundedError {p q : Polynomial ℕ IsArthurMerlinVerifier enc p q V A ↔ DecidesWithBoundedError enc p (arthurMerlinSlice enc q V) A := by simp only [IsArthurMerlinVerifier, DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, - BoundedErrorAt, arthurMerlinAcceptCount_eq_outcomeCount, - arthurMerlinRejectCount_eq_outcomeCount] + BoundedErrorAt, arthurMerlinSlice, decide_eq_true_iff, decide_eq_false_iff_not, not_exists, + Bool.not_eq_true] rfl /-- The problems with polynomial-time Arthur–Merlin verifiers, with polynomially long random @@ -264,7 +239,7 @@ theorem PolyTimeReducible.mem_MA {encB : β ↪ List Bool} {B : Set β} obtain ⟨q, p, V, hV, hVB⟩ := hB obtain ⟨Q, P, V', hV', hQe, hPe, hsplit⟩ := exists_truncated_verifier hf.tidy q p hV.tidy refine ⟨Q, P, V', .of_tidy hV', fun a => ?_⟩ - dsimp only [BoundedErrorAt, outcomeCount] + dsimp only [BoundedErrorAt] simp only [hsplit] constructor · intro ha @@ -304,7 +279,7 @@ theorem PolyTimeReducible.mem_AM {encB : β ↪ List Bool} {B : Set β} V (f a, (List.ofFn r).take (p.eval (encB (f a)).length) ++ List.ofFn y) = false := BitString.forall_take_ofFn_iff (hQe a) (g := fun w => V (f a, (List.ofFn r).take (p.eval (encB (f a)).length) ++ w) = false) - simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, hsplit, hex, hall] + simp only [hsplit, hex, hall] exact ⟨fun ha => two_mul_two_pow_le_card_filter_take (hPe a) (fun w => ∃ y : Fin (q.eval (encB (f a)).length) → Bool, V (f a, w ++ List.ofFn y) = true) ((hVB (f a)).1 ((hAB a).1 ha)), diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean index feb5c22d23..5afcdd42cd 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean @@ -64,7 +64,8 @@ is closed under polynomially bounded existential quantification (`MAM = AM`, * `Cslib.Complexity.IsMerlinArthurVerifier.repeatMajority`, `Cslib.Complexity.mem_MA_iff_exists_forall_errorExponent`: error reduction for `MA`, with the proof length fixed before the error. -* `Cslib.Complexity.IsArthurMerlinVerifier.repeatMajority`, +* `Cslib.Complexity.isArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent`, + `Cslib.Complexity.IsArthurMerlinVerifier.repeatMajority`, `Cslib.Complexity.mem_AM_iff_forall_errorExponent`: error reduction for `AM`. * `Cslib.Complexity.MA_subset_AM`, `Cslib.Complexity.NP_subset_AM`, `Cslib.Complexity.BPP_subset_AM`. @@ -172,10 +173,12 @@ non-member at most such a fraction have one. -/ def IsArthurMerlinVerifierWithErrorExponent (enc : α ↪ List Bool) (e p q : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop := ∀ a, (a ∈ A → 2 ^ e.eval (enc a).length * - arthurMerlinRejectCount V a (p.eval (enc a).length) (q.eval (enc a).length) ≤ + (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + ∀ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card ≤ 2 ^ p.eval (enc a).length) ∧ (a ∉ A → 2 ^ e.eval (enc a).length * - arthurMerlinAcceptCount V a (p.eval (enc a).length) (q.eval (enc a).length) ≤ + (univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + ∃ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = true).card ≤ 2 ^ p.eval (enc a).length) /-- An Arthur–Merlin verifier has error exponent `e` iff its reply-existence slice decides with @@ -186,7 +189,7 @@ theorem isArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent DecidesWithErrorExponent enc e p (arthurMerlinSlice enc q V) A := by simp only [IsArthurMerlinVerifierWithErrorExponent, DecidesWithErrorExponent, PromiseProblem.SolvesWithErrorExponent, ErrorExponentAt, Bool.not_true, Bool.not_false, - arthurMerlinAcceptCount_eq_outcomeCount, arthurMerlinRejectCount_eq_outcomeCount] + arthurMerlinSlice, decide_eq_true_iff, decide_eq_false_iff_not, not_exists, Bool.not_eq_true] rfl /-- The strict majority of `2 r(n)` parallel runs of an Arthur–Merlin verifier `V`, where `n` is the @@ -347,7 +350,7 @@ theorem MA_subset_AM : MA enc ⊆ AM enc := by (List.ofFn r ++ List.ofFn y).take (P.eval (enc a).length) = List.ofFn y ++ List.ofFn r := by rw [List.drop_left' List.length_ofFn, List.take_left' List.length_ofFn] - simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, hswap] + simp only [hswap] have h4 : 4 ≤ 2 ^ (q + 2).eval (enc a).length := by simp only [Polynomial.eval_add, Polynomial.eval_ofNat, pow_add] exact Nat.le_mul_of_pos_left _ (by positivity) @@ -437,7 +440,7 @@ theorem MA_subset_SBP : MA enc ⊆ SBP enc := by · -- the good proof alone is accepted with three quarters of the random strings intro ha obtain ⟨y, hy⟩ := (h' a).1 ha - dsimp only [ErrorExponentAt, outcomeCount, Bool.not_true] at hy + dsimp only [ErrorExponentAt, Bool.not_true] at hy rw [Polynomial.eval_add, Polynomial.eval_ofNat] at hy exact three_mul_two_pow_le_four_mul_sum W a y hy · -- all proofs together are accepted with at most a quarter of the random strings @@ -446,7 +449,7 @@ theorem MA_subset_SBP : MA enc ⊆ SBP enc := by (f := fun u : Fin (q.eval (enc a).length) → Bool => acceptCount (fun x => W (x.1, List.ofFn u ++ x.2)) a (P.eval (enc a).length)) fun u => ?_ - simpa only [ErrorExponentAt, outcomeCount, Bool.not_false, acceptCount, Polynomial.eval_add, + simpa only [ErrorExponentAt, Bool.not_false, acceptCount, Polynomial.eval_add, Polynomial.eval_ofNat] using (h' a).2 ha u /-! ### Existential quantification -/ @@ -556,7 +559,7 @@ theorem mem_AM_of_exists {B : Set (α × List Bool)} (hB : B ∈ AM (encPair enc computableInPolyTime_existsAMVerifier hVB (pB.comp L) p, fun a => ?_⟩ -- the verifier reads the word and runs the verifier of the pairs rw [Polynomial.eval_add] - simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, existsAMVerifier_ofFn_append] + simp only [existsAMVerifier_ofFn_append] -- the error bounds of the pairs, at the length of the encoded instance have herr (w : BitString (p.eval (enc a).length)) := by have h := hB' (a, List.ofFn w) diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean index 3b881d3f53..41c051dbc4 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean @@ -145,7 +145,7 @@ theorem isAlternatingVerifier_sigmaTwoVerifier {e q k p : Polynomial ℕ} {W : obtain ⟨y, hy⟩ := (h a).1 ha have hS : 2 ^ e.eval (enc a).length * #(univ.filter fun r : BitString (p.eval (enc a).length) => W (a, List.ofFn y ++ List.ofFn r) = true)ᶜ ≤ 2 ^ p.eval (enc a).length := by - simpa only [compl_filter, Bool.not_eq_true, ErrorExponentAt, outcomeCount, Bool.not_true] + simpa only [compl_filter, Bool.not_eq_true, ErrorExponentAt, Bool.not_true] using hy obtain ⟨u, hu⟩ := BitString.exists_forall_exists_add_mem_of_two_pow_mul_card_compl_le _ hS (hcover _) @@ -239,8 +239,7 @@ theorem isAlternatingVerifier_piTwoVerifier {e k p q : Polynomial ℕ} {W : α have hS : 2 ^ e.eval (enc a).length * #(univ.filter fun r : BitString (p.eval (enc a).length) => ∃ y : BitString (q.eval (enc a).length), W (a, List.ofFn r ++ List.ofFn y) = true)ᶜ ≤ 2 ^ p.eval (enc a).length := by - simpa only [compl_filter, not_exists, Bool.not_eq_true, arthurMerlinRejectCount] using - (h a).1 ha + simpa only [compl_filter, not_exists, Bool.not_eq_true] using (h a).1 ha obtain ⟨r, hr⟩ := BitString.exists_forall_add_notMem_of_two_pow_mul_card_le _ hS (hshifts _) (BitString.block (BitString.ofList (k.eval (enc a).length * p.eval (enc a).length) w)) have hY (i : Fin (k.eval (enc a).length)) : ∃ y : BitString (q.eval (enc a).length), diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean index 6b0f9d1a33..e3c37d4ea2 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean @@ -321,7 +321,6 @@ theorem mem_AM_of_card_certifiedSet {N c : Polynomial ℕ} {R : α × List Bool (5 * N.eval (enc a).length + T.eval (enc a).length) + m.eval (enc a).length := by simp have hQ : (5 * N + T + 5 * c).eval (enc a).length = 5 * N.eval (enc a).length + T.eval (enc a).length + 5 * c.eval (enc a).length := by simp - dsimp only [arthurMerlinAcceptCount, arthurMerlinRejectCount] rw [hP, hQ] simp only [forall_verifier_eq_false_iff, exists_verifier_iff] set n := (enc a).length diff --git a/Complexity/Computability/Complexity/Classes/BPP.lean b/Complexity/Computability/Complexity/Classes/BPP.lean index c5b51b110f..892b6bd9f9 100644 --- a/Complexity/Computability/Complexity/Classes/BPP.lean +++ b/Complexity/Computability/Complexity/Classes/BPP.lean @@ -44,8 +44,6 @@ The probability is written as a count over the random strings, which are functio ## Main definitions -* `Cslib.Complexity.outcomeCount`: the number of strings of a given length on which a verifier - gives a specified Boolean answer. * `Cslib.Complexity.BoundedErrorAt`: the per-instance bounded-error condition for a specified Boolean answer. * `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError`: the bounded-error condition on a @@ -55,6 +53,8 @@ The probability is written as a count over the random strings, which are functio ## Main results +* `Cslib.Complexity.BoundedErrorAt.congr`, `Cslib.Complexity.BoundedErrorAt.not`: extensionality + and negation for per-instance bounded error. * `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.compl`, `Cslib.Complexity.DecidesWithBoundedError.compl`: negating the verifier solves the complement with bounded error. @@ -79,48 +79,14 @@ open Turing.MultiTapeTM variable {α : Type} -/-- The number of strings `r` of length `n` with `V (a, r) = b`. -/ -@[reducible] -def outcomeCount (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : ℕ := - (Finset.univ.filter fun r : Fin n → Bool => V (a, List.ofFn r) = b).card - -/-- Verifiers that agree on an instance and all strings of length `n` have the same outcome counts -at length `n`. -/ -theorem outcomeCount_congr {V W : α × List Bool → Bool} {a : α} {n : ℕ} {b : Bool} - (h : ∀ r : Fin n → Bool, V (a, List.ofFn r) = W (a, List.ofFn r)) : - outcomeCount V a n b = outcomeCount W a n b := - congrArg Finset.card (Finset.filter_congr fun r _ => by rw [h r]) - -/-- Negating the verifier negates the counted outcome. -/ -theorem outcomeCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : - outcomeCount (fun x => !V x) a n b = outcomeCount V a n (!b) := - congrArg Finset.card (Finset.filter_congr fun _ _ => Bool.not_eq_eq_eq_not) - -/-- The strings of length `n` on which `V` gives `b` and those on which it gives `!b` partition all -`2 ^ n` strings. -/ -theorem outcomeCount_add_outcomeCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : - outcomeCount V a n b + outcomeCount V a n (!b) = 2 ^ n := by - have h := Finset.card_filter_add_card_filter_not (s := Finset.univ) - fun r : Fin n → Bool => V (a, List.ofFn r) = b - have hnot : (Finset.univ.filter fun r : Fin n → Bool => ¬V (a, List.ofFn r) = b) = - Finset.univ.filter fun r : Fin n → Bool => V (a, List.ofFn r) = !b := - Finset.filter_congr fun _ _ => by cases b <;> simp - simpa only [outcomeCount, hnot, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, - Fintype.card_fin] using h - -/-- The strings of length `n` that `V` accepts together with `a` and those it rejects partition all -`2 ^ n` strings. -/ -theorem outcomeCount_true_add_outcomeCount_false (V : α × List Bool → Bool) (a : α) (n : ℕ) : - outcomeCount V a n true + outcomeCount V a n false = 2 ^ n := - outcomeCount_add_outcomeCount_not V a n true - /-- `V` gives the answer `b` with bounded error on the instance `a`, using random strings whose length is `p` evaluated at the length of the encoded instance: at least two thirds of the random strings `r` of length `p (enc a).length` give `V (a, r) = b`. -/ -@[reducible] -def BoundedErrorAt (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) +abbrev BoundedErrorAt (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) (b : Bool) : Prop := - 2 * 2 ^ p.eval (enc a).length ≤ 3 * outcomeCount V a (p.eval (enc a).length) b + 2 * 2 ^ p.eval (enc a).length ≤ + 3 * (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + V (a, List.ofFn r) = b).card /-- Bounded error at an instance depends only on the verifier's values on strings of length `p(|a|)`. -/ @@ -128,13 +94,24 @@ theorem BoundedErrorAt.congr {enc : α ↪ List Bool} {p : Polynomial ℕ} {V W : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) (hVW : ∀ r : Fin (p.eval (enc a).length) → Bool, V (a, List.ofFn r) = W (a, List.ofFn r)) : BoundedErrorAt enc p W a b := by - rwa [BoundedErrorAt, ← outcomeCount_congr hVW] + have hcard : (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + V (a, List.ofFn r) = b).card = + (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + W (a, List.ofFn r) = b).card := + congrArg Finset.card (Finset.filter_congr fun r _ => by rw [hVW r]) + rwa [BoundedErrorAt, ← hcard] /-- Negating the verifier negates the bounded-error answer at `a`. -/ theorem BoundedErrorAt.not {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) : BoundedErrorAt enc p (fun x => !V x) a (!b) := by - rwa [BoundedErrorAt, outcomeCount_not, Bool.not_not] + have hcard : (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + (!V (a, List.ofFn r)) = !b).card = + (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + V (a, List.ofFn r) = b).card := + congrArg Finset.card + (Finset.filter_congr fun _ _ => by rw [Bool.not_eq_eq_eq_not, Bool.not_not]) + rwa [BoundedErrorAt, hcard] namespace PromiseProblem @@ -229,8 +206,8 @@ theorem P_subset_BPP : P enc ⊆ BPP enc := by rintro A ⟨f, hf, hA⟩ refine ⟨0, fun x => f x.1, hf.comp (.fst enc encBits), fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ - · simp [BoundedErrorAt, outcomeCount, (hA a).mp ha] + · simp [BoundedErrorAt, (hA a).mp ha] · have : f a = false := by simpa [hA a] using ha - simp [BoundedErrorAt, outcomeCount, this] + simp [BoundedErrorAt, this] end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean index 870a1fd2ae..7134bb1e17 100644 --- a/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/BPP/Amplification.lean @@ -49,6 +49,7 @@ polynomial time with error at most `2 ^ (-q(n))` for every polynomial `q` ## Main results +* `Cslib.Complexity.ErrorExponentAt.congr`: extensionality for per-instance error-exponent bounds. * `Cslib.Complexity.BoundedErrorAt.repeatMajority`, `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.repeatMajority`: `12 q(n)` majority votes reduce the error to `2 ^ (-q(n))`. @@ -77,10 +78,11 @@ variable {α : Type} /-- `V` gives the answer `b` with error at most `2 ^ (-q(n))` on the instance `a`, using random strings whose length is `p` evaluated at the length `n` of the encoded instance: the random strings `r` of length `p n` with `V (a, r) = !b` make up at most a `2 ^ (-q n)` fraction. -/ -@[reducible] -def ErrorExponentAt (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) +abbrev ErrorExponentAt (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) (b : Bool) : Prop := - 2 ^ q.eval (enc a).length * outcomeCount V a (p.eval (enc a).length) (!b) ≤ + 2 ^ q.eval (enc a).length * + (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + V (a, List.ofFn r) = !b).card ≤ 2 ^ p.eval (enc a).length /-- An error-exponent bound at an instance depends only on the verifier's values on strings of @@ -89,7 +91,12 @@ theorem ErrorExponentAt.congr {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V W : α × List Bool → Bool} {a : α} {b : Bool} (h : ErrorExponentAt enc q p V a b) (hVW : ∀ r : Fin (p.eval (enc a).length) → Bool, V (a, List.ofFn r) = W (a, List.ofFn r)) : ErrorExponentAt enc q p W a b := by - rwa [ErrorExponentAt, ← outcomeCount_congr hVW] + have hcard : (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + V (a, List.ofFn r) = !b).card = + (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => + W (a, List.ofFn r) = !b).card := + congrArg Finset.card (Finset.filter_congr fun r _ => by rw [hVW r]) + rwa [ErrorExponentAt, ← hcard] /-- **Per-instance error reduction for bounded error**: the strict majority of `12 q(n)` runs of a verifier on independent blocks of random bits errs from `b` on at most a `2 ^ (-q(n))` fraction of @@ -98,7 +105,7 @@ theorem BoundedErrorAt.repeatMajority {enc : α ↪ List Bool} {p : Polynomial {V : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) (q : Polynomial ℕ) : ErrorExponentAt enc q (12 * q * p) (Complexity.repeatMajority enc (6 * q) p V) a b := by - unfold ErrorExponentAt outcomeCount + unfold ErrorExponentAt have hlen : (12 * q * p).eval (enc a).length = 2 * (6 * q).eval (enc a).length * p.eval (enc a).length := by simp only [Polynomial.eval_mul, Polynomial.eval_ofNat] @@ -124,11 +131,13 @@ theorem BoundedErrorAt.repeatMajority {enc : α ↪ List Bool} {p : Polynomial theorem ErrorExponentAt.boundedErrorAt {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {b : Bool} (h : ErrorExponentAt enc q p V a b) (hq : 2 ≤ q.eval (enc a).length) : BoundedErrorAt enc p V a b := by - have hsum := outcomeCount_add_outcomeCount_not V a (p.eval (enc a).length) b - have h4 : 2 ^ 2 ≤ 2 ^ q.eval (enc a).length := Nat.pow_le_pow_right (by norm_num) hq - have hle := (Nat.mul_le_mul_right _ h4).trans h - unfold BoundedErrorAt - omega + refine BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le + (fun r => V (a, List.ofFn r) = b) ?_ + have hnot : (univ.filter fun r : BitString (p.eval (enc a).length) => ¬V (a, List.ofFn r) = b) = + univ.filter fun r : BitString (p.eval (enc a).length) => V (a, List.ofFn r) = !b := + filter_congr fun _ _ => by cases b <;> simp + rw [hnot] + exact (Nat.mul_le_mul_right _ (Nat.pow_le_pow_right (by norm_num) hq)).trans h namespace PromiseProblem @@ -203,14 +212,15 @@ theorem inter_mem_BPP {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : obtain ⟨p₂, V₂, hV₂, h₂⟩ := mem_BPP_iff_forall_decidesWithErrorExponent.1 hB 3 refine mem_BPP.2 ⟨p₁ + p₂, andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂, by fun_prop, fun a => ?_⟩ - have hs₁ := outcomeCount_true_add_outcomeCount_false V₁ a (p₁.eval (enc a).length) - have hs₂ := outcomeCount_true_add_outcomeCount_false V₂ a (p₂.eval (enc a).length) - have hs := outcomeCount_true_add_outcomeCount_false - (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a ((p₁ + p₂).eval (enc a).length) - have hc : outcomeCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a - ((p₁ + p₂).eval (enc a).length) true = - outcomeCount V₁ a (p₁.eval (enc a).length) true * - outcomeCount V₂ a (p₂.eval (enc a).length) true := by + have hs₁ := acceptCount_add_card_filter_eq_false (V := V₁) (a := a) (n := p₁.eval (enc a).length) + have hs₂ := acceptCount_add_card_filter_eq_false (V := V₂) (a := a) (n := p₂.eval (enc a).length) + have hs := acceptCount_add_card_filter_eq_false + (V := andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) (a := a) + (n := (p₁ + p₂).eval (enc a).length) + have hc : acceptCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a + ((p₁ + p₂).eval (enc a).length) = + acceptCount V₁ a (p₁.eval (enc a).length) * + acceptCount V₂ a (p₂.eval (enc a).length) := by rw [Polynomial.eval_add] exact acceptCount_andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂ a (p₂.eval (enc a).length) constructor @@ -219,26 +229,28 @@ theorem inter_mem_BPP {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : have e₂ := (h₂ a).1 ha.2 simp only [ErrorExponentAt, Bool.not_true, Polynomial.eval_ofNat] at e₁ e₂ have f₁ : 7 * 2 ^ p₁.eval (enc a).length ≤ - 8 * outcomeCount V₁ a (p₁.eval (enc a).length) true := by omega + 8 * acceptCount V₁ a (p₁.eval (enc a).length) := by omega have f₂ : 7 * 2 ^ p₂.eval (enc a).length ≤ - 8 * outcomeCount V₂ a (p₂.eval (enc a).length) true := by omega + 8 * acceptCount V₂ a (p₂.eval (enc a).length) := by omega unfold BoundedErrorAt - rw [hc, Polynomial.eval_add, pow_add] + rw [← acceptCount, hc, Polynomial.eval_add, pow_add] nlinarith [Nat.mul_le_mul f₁ f₂] · intro ha - have hacc : 8 * outcomeCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a - ((p₁ + p₂).eval (enc a).length) true ≤ 2 ^ (p₁ + p₂).eval (enc a).length := by + have hacc : 8 * acceptCount (andVerifier (fun a => p₁.eval (enc a).length) V₁ V₂) a + ((p₁ + p₂).eval (enc a).length) ≤ 2 ^ (p₁ + p₂).eval (enc a).length := by rw [hc, Polynomial.eval_add, pow_add] by_cases ha₁ : a ∈ A · have ha₂ : a ∉ B := fun hb => ha ⟨ha₁, hb⟩ have e₂ := (h₂ a).2 ha₂ simp only [ErrorExponentAt, Bool.not_false, Polynomial.eval_ofNat] at e₂ - have hb₁ : outcomeCount V₁ a (p₁.eval (enc a).length) true ≤ + rw [← acceptCount] at e₂ + have hb₁ : acceptCount V₁ a (p₁.eval (enc a).length) ≤ 2 ^ p₁.eval (enc a).length := by omega nlinarith [Nat.mul_le_mul hb₁ e₂] · have e₁ := (h₁ a).2 ha₁ simp only [ErrorExponentAt, Bool.not_false, Polynomial.eval_ofNat] at e₁ - have hb₂ : outcomeCount V₂ a (p₂.eval (enc a).length) true ≤ + rw [← acceptCount] at e₁ + have hb₂ : acceptCount V₂ a (p₂.eval (enc a).length) ≤ 2 ^ p₂.eval (enc a).length := by omega nlinarith [Nat.mul_le_mul e₁ hb₂] unfold BoundedErrorAt diff --git a/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean b/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean index 5d6da544a7..c367bee4de 100644 --- a/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean +++ b/Complexity/Computability/Complexity/Classes/BPP/Reduction.lean @@ -62,8 +62,7 @@ theorem PolyTimeReducible.mem_BPP (h : PolyTimeReducible enc encB A B) (hB : B (hW.comp ((hg.comp (.fst enc encBits)).prod (.snd enc encBits))) (.const true)), fun a => ?_⟩ obtain ⟨j, hj⟩ := Nat.exists_eq_add_of_le (hle a) - dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt, - outcomeCount] + dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt] rw [hj] set k := q.eval (encB (g a)).length set V := andVerifier (fun a => q.eval (encB (g a)).length) (fun x => W (g x.1, x.2)) diff --git a/Complexity/Computability/Complexity/Classes/IP.lean b/Complexity/Computability/Complexity/Classes/IP.lean index 6ce6e4a498..2b5105f4f4 100644 --- a/Complexity/Computability/Complexity/Classes/IP.lean +++ b/Complexity/Computability/Complexity/Classes/IP.lean @@ -296,12 +296,15 @@ theorem BPP_subset_IP (enc : α ↪ List Bool) : BPP enc ⊆ IP enc := by refine ⟨_, isOraclePPTOn_bppVerifier (p := p) hV.tidy, fun a ha => ⟨Prover.const [], ?_⟩, fun a ha P => ?_⟩ <;> rw [acceptProb_bppVerifier] · have h := (hA a).1 ha - unfold BoundedErrorAt outcomeCount at h + unfold BoundedErrorAt at h exact_mod_cast natCast_div_le_natCast_div (a := 2) (b := 3) (d := 2 ^ p.eval (enc a).length) three_ne_zero (pow_pos two_pos _).ne' (by omega) · have h := (hA a).2 ha - have hsum := outcomeCount_true_add_outcomeCount_false V a (p.eval (enc a).length) - unfold BoundedErrorAt outcomeCount at h hsum + unfold BoundedErrorAt at h + have hsum := Finset.card_filter_add_card_filter_not (s := Finset.univ) + (fun r : Fin (p.eval (enc a).length) → Bool => V (a, List.ofFn r) = true) + simp only [Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, + Fintype.card_fin] at hsum exact_mod_cast natCast_div_le_natCast_div (c := 1) (d := 3) (b := 2 ^ p.eval (enc a).length) (pow_pos two_pos _).ne' three_ne_zero (by omega) diff --git a/Complexity/Computability/Complexity/Classes/PP.lean b/Complexity/Computability/Complexity/Classes/PP.lean index c24a2cacc8..37f7c119af 100644 --- a/Complexity/Computability/Complexity/Classes/PP.lean +++ b/Complexity/Computability/Complexity/Classes/PP.lean @@ -77,13 +77,13 @@ strings accepts the members of its problem, and only them, on more than half. -/ theorem DecidesWithBoundedError.decidesByMajority {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (h : DecidesWithBoundedError enc p V A) : DecidesByMajority enc p V A := by intro a - have hsum := outcomeCount_true_add_outcomeCount_false V a (p.eval (enc a).length) + have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length) have hpos := Nat.one_le_two_pow (n := p.eval (enc a).length) - change a ∈ A ↔ 2 ^ p.eval (enc a).length < 2 * outcomeCount V a (p.eval (enc a).length) true constructor · intro ha have := (h a).1 ha unfold BoundedErrorAt at this + rw [← acceptCount] at this omega · intro hlt by_contra ha diff --git a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean index 5991d20f3a..197776d463 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean @@ -175,7 +175,7 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔ fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ · have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (enc a).length = c * ((enc a).length + 1) ^ d := by simp - dsimp only [BoundedErrorAt, outcomeCount] + dsimp only [BoundedErrorAt] rw [hp] have hprob := hyes a ha rw [hlaw a, uniformList_acceptCount_toReal (V := fun x => evalM x.1 x.2), @@ -186,7 +186,7 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔ exact_mod_cast h3 · have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (enc a).length = c * ((enc a).length + 1) ^ d := by simp - dsimp only [BoundedErrorAt, outcomeCount] + dsimp only [BoundedErrorAt] rw [hp] have hprob := hno a ha have hmap : ProbComp.eval (Bool.not <$> M a) = diff --git a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean index cfaefc71af..39ac9bcd65 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean @@ -495,14 +495,14 @@ theorem RPReducible.mem_PromiseBPP (hXY : RPReducible encA encB X Y) have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := b) (n := p.eval (encB b).length) have h := (hYV b).1 hb - simp only [ErrorExponentAt, outcomeCount, Bool.not_true, Polynomial.eval_ofNat] at h + simp only [ErrorExponentAt, Bool.not_true, Polynomial.eval_ofNat] at h have h' : (7 : ℝ) * 2 ^ p.eval (encB b).length ≤ 8 * acceptCount V b (p.eval (encB b).length) := by exact_mod_cast (by omega) linarith have hMno (b : β) (hb : b ∈ Y.no) : Pr[M b] ≤ 1 / 8 := by rw [probability_sampleList_verifier, div_le_iff₀ (by positivity)] have h := (hYV b).2 hb - simp only [ErrorExponentAt, outcomeCount, Bool.not_false, Polynomial.eval_ofNat] at h + simp only [ErrorExponentAt, Bool.not_false, Polynomial.eval_ofNat] at h rw [← acceptCount] at h have h' : (8 : ℝ) * acceptCount V b (p.eval (encB b).length) ≤ 2 ^ p.eval (encB b).length := by exact_mod_cast h diff --git a/Complexity/Computability/Complexity/Classes/RP.lean b/Complexity/Computability/Complexity/Classes/RP.lean index 432f40cae3..7996c5ded4 100644 --- a/Complexity/Computability/Complexity/Classes/RP.lean +++ b/Complexity/Computability/Complexity/Classes/RP.lean @@ -271,7 +271,7 @@ theorem solvesWithOneSidedError (h : Q.SolvesWithOneSidedErrorExponent enc q p V theorem solvesWithErrorExponent (h : Q.SolvesWithOneSidedErrorExponent enc q p V) : Q.SolvesWithErrorExponent enc q p V := fun a => by refine ⟨(h a).1, fun ha => ?_⟩ - simp only [ErrorExponentAt, outcomeCount, Bool.not_false] + simp only [ErrorExponentAt, Bool.not_false] rw [Finset.filter_false_of_mem fun r _ => by simp [(h a).2 ha r]] simp diff --git a/Complexity/Computability/Complexity/Classes/SBP.lean b/Complexity/Computability/Complexity/Classes/SBP.lean index 701406962d..68c4ee3419 100644 --- a/Complexity/Computability/Complexity/Classes/SBP.lean +++ b/Complexity/Computability/Complexity/Classes/SBP.lean @@ -118,11 +118,10 @@ theorem BPP_subset_SBP : BPP enc ⊆ SBP enc := by change (a ∈ A → _ ≤ 3 * acceptCount V a (p.eval (enc a).length)) ∧ _ constructor <;> intro ha · have := h.1 ha - unfold outcomeCount at this lia · have := h.2 ha change 2 * (3 * acceptCount V a (p.eval (enc a).length)) < _ - change _ * acceptCount V a (p.eval (enc a).length) ≤ _ at this + rw [← acceptCount] at this lia /-- The integer gap `2f - k + 1` is positive exactly on members, including zero thresholds. -/ @@ -218,7 +217,7 @@ theorem inter_mem_SBP_of_mem_BPP (hA : A ∈ SBP enc) (hB : B ∈ BPP enc) : have hD : 0 < 2 ^ q.eval (enc a).length := by positivity have hp1 : 1 ≤ 2 ^ p.eval (enc a).length := Nat.one_le_pow _ _ (by decide) have h := hB a - simp only [ErrorExponentAt, Bool.not_true, Bool.not_false, outcomeCount, + simp only [ErrorExponentAt, Bool.not_true, Bool.not_false, Polynomial.eval_add, Polynomial.eval_ofNat, pow_add] at h change (a ∈ A ∩ B → 3 * (k a * 2 ^ q.eval (enc a).length) ≤ 4 * (f a * c a)) ∧ (a ∉ A ∩ B → 2 * (4 * (f a * c a)) < 3 * (k a * 2 ^ q.eval (enc a).length)) diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean index e824152b22..2b2c876b30 100644 --- a/Complexity/Computability/Complexity/Classes/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Time.lean @@ -459,8 +459,7 @@ theorem mem_BPP_iff_exists_mem_BPTIME {α : Type} {enc : α ↪ List Bool} {A : have hprob := (hA a).2 rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, two_thirds_le_div_iff] at hprob - dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt, - outcomeCount] + dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt] rw [heval] constructor · intro (ha : a ∈ A) diff --git a/Complexity/Computability/Complexity/Classes/Toda.lean b/Complexity/Computability/Complexity/Classes/Toda.lean index 811ca0eab6..756befa14e 100644 --- a/Complexity/Computability/Complexity/Classes/Toda.lean +++ b/Complexity/Computability/Complexity/Classes/Toda.lean @@ -83,7 +83,7 @@ theorem exists_SharpP_testBit_of_mem_BPOp_ParityP {L : Set α} rw [length_encPair, hZp, Polynomial.eval_comp] simp [hr] obtain ⟨hyes, hno⟩ := hdec a - dsimp only [BoundedErrorAt, outcomeCount] at hyes hno + dsimp only [BoundedErrorAt] at hyes hno simp only [decide_eq_true_eq, decide_eq_false_iff_not, hL', hZlen _ List.length_ofFn] at hyes hno simp only diff --git a/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean b/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean index 977b3b0c8a..7e50ed0a2a 100644 --- a/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean +++ b/Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean @@ -539,7 +539,7 @@ theorem PH_subset_BPOp_ParityP : PH enc ⊆ BPOp enc (ParityP (encPair enc encBi (s := (univ : Finset (Fin (ρ.eval (enc a).length) → Bool))) (fun r => Odd (acceptCount (fun x => W (x.1, List.ofFn r ++ x.2)) a (ζ.eval (enc a).length))) simp only [card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_fin] at hsplit - simp only [BoundedErrorAt, outcomeCount, hL', Set.mem_ofPred_eq, decide_eq_true_eq, + simp only [BoundedErrorAt, hL', Set.mem_ofPred_eq, decide_eq_true_eq, decide_eq_false_iff_not] rw [← hLV a] at ha constructor diff --git a/ComplexityTests/ArthurMerlin.lean b/ComplexityTests/ArthurMerlin.lean index 351529c2b7..90f7416602 100644 --- a/ComplexityTests/ArthurMerlin.lean +++ b/ComplexityTests/ArthurMerlin.lean @@ -37,10 +37,10 @@ private theorem head_mem_MA_direct : {w : List Bool | w.headD false = true} ∈ decide refine ⟨1, 1, fun x => x.1.headD false, by fun_prop, fun w => ⟨fun hw => ?_, fun hw y => ?_⟩⟩ · refine ⟨fun _ => true, ?_⟩ - dsimp only [BoundedErrorAt, outcomeCount] + dsimp only [BoundedErrorAt] rw [Finset.filter_true_of_mem fun r _ => by simpa using hw] exact hcard w - · dsimp only [BoundedErrorAt, outcomeCount] + · dsimp only [BoundedErrorAt] rw [Finset.filter_true_of_mem fun r _ => by simpa using hw] exact hcard w diff --git a/ComplexityTests/InteractiveProofs.lean b/ComplexityTests/InteractiveProofs.lean index 8eb0b49910..609e52616b 100644 --- a/ComplexityTests/InteractiveProofs.lean +++ b/ComplexityTests/InteractiveProofs.lean @@ -126,7 +126,7 @@ example (a : List Bool) : example : (∅ : Set (List Bool)) ∈ IP encBits := BPP_subset_IP _ ⟨0, fun _ => false, .const false, fun _ => ⟨fun h => h.elim, fun _ => by - simp only [BoundedErrorAt, outcomeCount, Polynomial.eval_zero, pow_zero, mul_one] + simp only [BoundedErrorAt, Polynomial.eval_zero, pow_zero, mul_one] exact le_trans (by norm_num : 2 ≤ 3 * 1) (Nat.mul_le_mul_left 3 (Finset.card_pos.2 ⟨fun _ => false, Finset.mem_filter.2 ⟨Finset.mem_univ _, trivial⟩⟩))⟩⟩ diff --git a/ComplexityTests/NonVacuity.lean b/ComplexityTests/NonVacuity.lean index b6a32ae66a..1027a8d648 100644 --- a/ComplexityTests/NonVacuity.lean +++ b/ComplexityTests/NonVacuity.lean @@ -92,7 +92,7 @@ example : (Set.univ : Set (List Bool)) ∈ NP encBits := example : (∅ : Set (List Bool)) ∈ BPP encBits := ⟨0, fun _ => false, .const false, fun _ => ⟨fun h => h.elim, fun _ => by - simp only [BoundedErrorAt, outcomeCount, Polynomial.eval_zero, pow_zero, mul_one] + simp only [BoundedErrorAt, Polynomial.eval_zero, pow_zero, mul_one] exact le_trans (by norm_num : 2 ≤ 3 * 1) (Nat.mul_le_mul_left 3 (Finset.card_pos.2 ⟨fun _ => false, Finset.mem_filter.2 ⟨Finset.mem_univ _, trivial⟩⟩))⟩⟩ @@ -109,7 +109,7 @@ example : (⊤ : Language Bool) ∈ PPoly := example : (⊥ : Language Bool) ∈ PPoly := mem_PPolyOn_encBits_iff.1 (BPP_subset_PPolyOn ⟨0, fun _ => false, .const false, fun _ => ⟨fun h => h.elim, fun _ => by - simp only [BoundedErrorAt, outcomeCount, Polynomial.eval_zero, pow_zero, mul_one] + simp only [BoundedErrorAt, Polynomial.eval_zero, pow_zero, mul_one] exact le_trans (by norm_num : 2 ≤ 3 * 1) (Nat.mul_le_mul_left 3 (Finset.card_pos.2 ⟨fun _ => false, Finset.mem_filter.2 ⟨Finset.mem_univ _, trivial⟩⟩))⟩⟩) diff --git a/ComplexityTests/ResourceClasses4.lean b/ComplexityTests/ResourceClasses4.lean index bc1dd9c8ff..7a60c786da 100644 --- a/ComplexityTests/ResourceClasses4.lean +++ b/ComplexityTests/ResourceClasses4.lean @@ -80,10 +80,10 @@ theorem decidesWithBoundedError_orAnd : DecidesWithBoundedError encBits 2 orAnd decide rcases ha : a.headD false · refine ⟨fun h => absurd (ha.symm.trans h) Bool.false_ne_true, fun _ => ?_⟩ - simp only [BoundedErrorAt, outcomeCount, orAnd, ha, Bool.false_eq_true, ↓reduceIte] + simp only [BoundedErrorAt, orAnd, ha, Bool.false_eq_true, ↓reduceIte] exact hand _ (Polynomial.eval_ofNat 2 _) · refine ⟨fun _ => ?_, fun h => absurd ha h⟩ - simp only [BoundedErrorAt, outcomeCount, orAnd, ha, ↓reduceIte] + simp only [BoundedErrorAt, orAnd, ha, ↓reduceIte] exact hor _ (Polynomial.eval_ofNat 2 _) /-- Majority votes of `12 q(n)` runs of `orAnd` decide `startsTrue` with error at most diff --git a/ComplexityTests/SipserLautemann.lean b/ComplexityTests/SipserLautemann.lean index 657e22280a..bf6cc27410 100644 --- a/ComplexityTests/SipserLautemann.lean +++ b/ComplexityTests/SipserLautemann.lean @@ -80,8 +80,7 @@ theorem noisyHeadVerifier_decides : DecidesWithBoundedError encBits (Polynomial.C 2) noisyHeadVerifier {x : List Bool | x.headD false = true} := by intro a - dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt, - outcomeCount] + dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt] generalize hm : (Polynomial.C 2).eval (encBits a).length = m have hm2 : m = 2 := by rw [← hm, Polynomial.eval_C] subst hm2 From 123a6f04456fac826acf9461dcdae5cf0942cb05 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 04:30:12 +0000 Subject: [PATCH 3/3] test(PromiseProbabilistic): unfold BoundedErrorAt before generalize after rebase (#1400) --- ComplexityTests/PromiseProbabilistic.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ComplexityTests/PromiseProbabilistic.lean b/ComplexityTests/PromiseProbabilistic.lean index e69aecdfcc..7633aba8e3 100644 --- a/ComplexityTests/PromiseProbabilistic.lean +++ b/ComplexityTests/PromiseProbabilistic.lean @@ -109,11 +109,13 @@ theorem solvesWithBoundedError_partialSingletonBit : intro a refine ⟨fun ha => ?_, fun ha => ?_⟩ · obtain rfl : a = [true] := ha + dsimp only [BoundedErrorAt] generalize hk : (1 : Polynomial ℕ).eval (encBits [true]).length = k rw [Polynomial.eval_one] at hk subst hk decide · obtain rfl : a = [false] := ha + dsimp only [BoundedErrorAt] generalize hk : (1 : Polynomial ℕ).eval (encBits [false]).length = k rw [Polynomial.eval_one] at hk subst hk