From 2e625f4c2f21f722bf22daa1477beaf3f92dca00 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 10:40:00 +0000 Subject: [PATCH] refactor(mcsp): bundle GapMCSP as PromiseProblem and extract single-output and tableVerifier API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address Issue #610 (Wave 2, Item 6 — MCSP and Kolmogorov): - Add `Circuit.computesOn_single_iff` and `Circuit.computes_single_iff` in `Complexity/Computability/Circuit/Complexity.lean` and `mem_computableFunctions_iff_complexity_le` in `Complexity/Computability/Circuit/Counting.lean`, simplifying proofs across `MCSP/Basic.lean`, `MCSP/Succinct.lean`, `MCSP/AntiChecker.lean`, and `MCSP/NP.lean`. - Bundle `Cslib.GapMCSP` as a `Complexity.PromiseProblem (BitString (2 ^ n))` in `Complexity/Computability/MCSP/Basic.lean` with `@[simp]` lemmas `GapMCSP.yes_eq`, `GapMCSP.no_eq`, and `GapMCSP.eq_ofSet`. - Move the reusable list truth-table and `tableVerifier` MCSP bridge (`tableFunction`, `tableFunction_ofFn_truthTable`, `complexity_le_of_tableVerifier`, and `exists_tableVerifier_append`) from `Complexity/Computability/Complexity/Classes/PH/Kannan.lean` into `Complexity/Computability/MCSP/NP.lean`. Ref #610 --- Complexity.lean | 1 + .../Computability/Circuit/Complexity.lean | 20 +++++- .../Computability/Circuit/Counting.lean | 40 ++++++++++++ .../Complexity/Classes/PH/Kannan.lean | 64 +++---------------- .../Computability/MCSP/AntiChecker.lean | 10 +-- Complexity/Computability/MCSP/Basic.lean | 45 +++++++++++-- Complexity/Computability/MCSP/NP.lean | 58 +++++++++++++++-- Complexity/Computability/MCSP/Succinct.lean | 21 ++---- ComplexityTests/Kannan.lean | 27 +++++++- 9 files changed, 195 insertions(+), 91 deletions(-) create mode 100644 Complexity/Computability/Circuit/Counting.lean diff --git a/Complexity.lean b/Complexity.lean index cdcc00fa44..3c6b3c080a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -342,6 +342,7 @@ public import Complexity.Computability.Circuit.Clique public import Complexity.Computability.Circuit.Complexity public import Complexity.Computability.Circuit.CompositionDepth public import Complexity.Computability.Circuit.Continuity +public import Complexity.Computability.Circuit.Counting public import Complexity.Computability.Circuit.Cyclic public import Complexity.Computability.Circuit.Cyclic.Feedback public import Complexity.Computability.Circuit.Decomposable diff --git a/Complexity/Computability/Circuit/Complexity.lean b/Complexity/Computability/Circuit/Complexity.lean index 31068b1e93..26c545f4d9 100644 --- a/Complexity/Computability/Circuit/Complexity.lean +++ b/Complexity/Computability/Circuit/Complexity.lean @@ -24,6 +24,8 @@ to each other. ## Main results +* `Cslib.Circuits.Circuit.computesOn_single_iff`, `Cslib.Circuits.Circuit.computes_single_iff`: + a one-output circuit computes `single f` when its output `0` agrees with `f`. * `Cslib.Circuits.complexity_single_proj`, `Cslib.Circuits.one_le_complexity_single`: exactly the projections are computed without gates. * `Cslib.Circuits.complexity_single_unary_le`, `Cslib.Circuits.complexity_single_binary_le`: @@ -47,6 +49,20 @@ variable {σ : Signature} {U : Type*} {I : Interpretation σ U} {n : ℕ} section Single +/-- A one-output circuit computes `single f` on `S` exactly when its output `0` agrees with `f` +on `S`. -/ +theorem Circuit.computesOn_single_iff {c : Circuit σ n 1} {S : Set (Fin n → U)} + {f : (Fin n → U) → U} : + c.ComputesOn I S (single f) ↔ ∀ x ∈ S, c.eval I x 0 = f x := + ⟨fun h _ hx => congrFun (h hx) 0, fun h _ hx => funext fun i => + Subsingleton.elim i 0 ▸ h _ hx⟩ + +/-- A one-output circuit computes `single f` exactly when its output `0` agrees with `f` on +every input. -/ +theorem Circuit.computes_single_iff {c : Circuit σ n 1} {f : (Fin n → U) → U} : + c.Computes I (single f) ↔ ∀ x, c.eval I x 0 = f x := + ⟨fun h x => congrFun (h x) 0, fun h x => funext fun i => Subsingleton.elim i 0 ▸ h x⟩ + variable [I.IsComplete] /-- The coordinate projections cost no gates. -/ @@ -63,8 +79,8 @@ theorem one_le_complexity_single {f : (Fin n → U) → U} (hf : ∀ i, f ≠ fu cases hw : c.outputs 0 with | input i => refine hf i (funext fun x => ?_) - have := congrFun (hc x) 0 - simp only [Circuit.eval, Function.comp_apply, hw, Program.trace_input, single_apply] at this + have := Circuit.computes_single_iff.mp hc x + simp only [Circuit.eval, Function.comp_apply, hw, Program.trace_input] at this exact this.symm | gate j => exact absurd j.isLt (by omega) diff --git a/Complexity/Computability/Circuit/Counting.lean b/Complexity/Computability/Circuit/Counting.lean new file mode 100644 index 0000000000..5a5ec361e1 --- /dev/null +++ b/Complexity/Computability/Circuit/Counting.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (additions to `Cslib/Computability/Circuit/Counting.lean`) + +public import Complexity.Init +public import Cslib.Computability.Circuit.Counting + +/-! +# Counting functions computed by finite circuits over a complete basis + +This module provides the `complexity` characterization of `Cslib.Circuits.computableFunctions` +over a complete gate basis, complementing +`Cslib.Circuits.mem_computableFunctions_iff_ecomplexity_le`. + +## Main results + +* `Cslib.Circuits.mem_computableFunctions_iff_complexity_le`: over a complete basis, the scalar + functions computable with at most `s` gates are those of complexity at most `s`. +-/ + +@[expose] public section + +namespace Cslib.Circuits + +universe v u +variable {σ : Signature.{v}} [Finite σ.Op] {U : Type u} +variable {I : Interpretation σ U} [I.IsComplete] {n s : ℕ} + +/-- Over a complete basis, the functions computable with at most `s` gates are those of +complexity at most `s`. -/ +theorem mem_computableFunctions_iff_complexity_le {f : (Fin n → U) → U} : + f ∈ computableFunctions I n s ↔ complexity I (single f) ≤ s := by + rw [mem_computableFunctions, complexity_le_iff] + +end Cslib.Circuits diff --git a/Complexity/Computability/Complexity/Classes/PH/Kannan.lean b/Complexity/Computability/Complexity/Classes/PH/Kannan.lean index 25ea6577e6..5e92020118 100644 --- a/Complexity/Computability/Complexity/Classes/PH/Kannan.lean +++ b/Complexity/Computability/Complexity/Classes/PH/Kannan.lean @@ -165,15 +165,11 @@ private theorem eventually_le_arity (k N : ℕ) : ∀ᶠ n in atTop, N ≤ arity /-! ### Hard truth tables -/ -/-- The function on `m` inputs with the truth table `T`, read as MCSP reads truth tables. -/ -def tableFunction (m : ℕ) (T : List Bool) : BooleanFunction m := - fun y => MCSP.tableValue T (List.ofFn y) - /-- `T` is a truth table on `arity k n` inputs whose function needs more than `threshold k n` gates. -/ def IsHard (k n : ℕ) (T : List Bool) : Prop := T.length = 2 ^ arity k n ∧ - threshold k n < complexity interpretation (single (tableFunction (arity k n) T)) + threshold k n < complexity interpretation (single (MCSP.tableFunction (arity k n) T)) /-- `T` is the first hard truth table in lexicographic order: the hard table that is least as a binary number, most significant bit first. -/ @@ -200,20 +196,13 @@ theorem exists_isFirstHard {k n : ℕ} (h : ∃ T, IsHard k n T) : ∃ T, IsFirs obtain ⟨T, hT, hv⟩ := Nat.find_spec hex exact ⟨T, hT, fun T' hT' => hv ▸ Nat.find_min' hex ⟨T', hT', rfl⟩⟩ -/-- The truth table of a function, as a list, is read back as the function. -/ -private theorem tableFunction_ofFn_truthTable (m : ℕ) (f : BooleanFunction m) : - tableFunction m (List.ofFn (MCSP.truthTable m f)) = f := by - funext y - exact (MCSP.tableValue_ofFn ⟨m, MCSP.truthTable m f, 0⟩ y).trans - (by simp [MCSP.Instance.function]) - /-- **Shannon's counting argument**: hard truth tables exist at all large lengths. -/ theorem eventually_exists_isHard (k : ℕ) : ∀ᶠ n in atTop, ∃ T, IsHard k n T := by obtain ⟨N, hN⟩ := Shannon.lt_complexity filter_upwards [eventually_le_arity k (max N 1), eventually_ge_atTop (k + 2)] with n hm hn obtain ⟨f, hf⟩ := hN (arity k n) (le_of_max_le_left hm) refine ⟨List.ofFn (MCSP.truthTable _ f), by simp, ?_⟩ - rw [tableFunction_ofFn_truthTable] + rw [MCSP.tableFunction_ofFn_truthTable] have hm0 : (0 : ℝ) < arity k n := by exact_mod_cast (le_of_max_le_right hm) have hlt : (threshold k n : ℝ) * arity k n < 2 ^ arity k n := by exact_mod_cast threshold_mul_arity_lt (by omega) @@ -269,44 +258,6 @@ theorem language_notMem_SIZE (k c : ℕ) : language k ∉ SIZE fun n => c * (n + have hpos : 1 ≤ (n + 1) ^ k := Nat.one_le_pow _ _ (by omega) nlinarith -/-! ### Truth tables in MCSP -/ - -/-- The MCSP instance of a truth table of length `2 ^ m`. -/ -private def tableInstance (m s : ℕ) (T : List Bool) (hT : T.length = 2 ^ m) : MCSP.Instance := - ⟨m, fun i => T[i.val]'(by rw [hT]; exact i.isLt), s⟩ - -private theorem ofFn_tableInstance {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) : - List.ofFn (tableInstance m s T hT).table = T := by - change List.ofFn (fun i : Fin (2 ^ m) => T[i.val]'(by rw [hT]; exact i.isLt)) = T - exact List.ext_getElem (by simp [hT]) fun _ _ _ => by simp - -private theorem function_tableInstance {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) : - (tableInstance m s T hT).function = tableFunction m T := by - funext y - rw [← MCSP.tableValue_ofFn, ofFn_tableInstance] - rfl - -/-- An accepted certificate for a truth table of length `2 ^ m` bounds the complexity of its -function. -/ -private theorem complexity_le_of_tableVerifier {m s : ℕ} {T c : List Bool} (hT : T.length = 2 ^ m) - (h : MCSP.tableVerifier ((T, s), c) = true) : - complexity interpretation (single (tableFunction m T)) ≤ s := by - have := MCSP.mem_of_verifier_eq_true (x := tableInstance m s T hT) (w := c) - (by rw [MCSP.verifier_eq_tableVerifier, ofFn_tableInstance]; exact h) - rwa [MCSP.mem_iff, function_tableInstance] at this - -/-- A truth table of length `2 ^ m` whose function has at most `s` gates has a certificate of -length `certLength m (MCSP.budget m s)`, accepted whatever bits follow it. -/ -private theorem exists_tableVerifier_append {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) - (h : complexity interpretation (single (tableFunction m T)) ≤ s) : - ∃ u : List Bool, u.length = certLength m (MCSP.budget m s) ∧ - ∀ extra, MCSP.tableVerifier ((T, s), u ++ extra) = true := by - obtain ⟨u, hu, hV⟩ := MCSP.exists_verifier_append (x := tableInstance m s T hT) - (by rw [MCSP.mem_iff, function_tableInstance]; exact h) - refine ⟨u, hu, fun extra => ?_⟩ - rw [← hV extra, MCSP.verifier_eq_tableVerifier, ofFn_tableInstance] - rfl - /-! ### The `Σ₃` verifier -/ /-- The length of the blocks holding truth tables. -/ @@ -411,10 +362,10 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) : (BitString.binaryValue (table k x.length w₂) < BitString.binaryValue T → MCSP.tableVerifier ((table k x.length w₂, threshold k x.length), w₃) = true) := by by_cases hlt : BitString.binaryValue (table k x.length w₂) < BitString.binaryValue T - · have heasy : complexity interpretation (single (tableFunction (arity k x.length) + · have heasy : complexity interpretation (single (MCSP.tableFunction (arity k x.length) (table k x.length w₂))) ≤ threshold k x.length := not_lt.1 fun h => absurd (hT.2 _ ⟨hT', h⟩) (not_le.2 hlt) - obtain ⟨u, hu, hV⟩ := exists_tableVerifier_append hT' heasy + obtain ⟨u, hu, hV⟩ := MCSP.exists_tableVerifier_append hT' heasy refine ⟨u ++ List.replicate (certBound k x.length - u.length) false, ?_, fun _ => hV _⟩ have := certLength_le_certBound k x.length simp only [List.length_append, List.length_replicate] @@ -428,7 +379,7 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) : · cases hc : MCSP.tableVerifier ((T, threshold k x.length), w₂.drop (tableBound k x.length) ++ w₃) · rfl - · exact absurd (complexity_le_of_tableVerifier hT.1.1 hc) (not_le.2 hT.1.2) + · exact absurd (MCSP.complexity_le_of_tableVerifier hT.1.1 hc) (not_le.2 hT.1.2) · by_cases hlt : BitString.binaryValue (table k x.length w₂) < BitString.binaryValue T · exact Or.inr (hw₃ hlt) · exact Or.inl (not_lt.1 hlt) @@ -458,7 +409,7 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) : refine ⟨table k x.length w₁, ⟨⟨hT, ?_⟩, fun T' hT' => ?_⟩, ?_⟩ · -- no circuit within the threshold computes the table by_contra hle - obtain ⟨u, hu, hV⟩ := exists_tableVerifier_append hT (not_lt.1 hle) + obtain ⟨u, hu, hV⟩ := MCSP.exists_tableVerifier_append hT (not_lt.1 hle) have hlen : (List.replicate (tableBound k x.length) false ++ u).length ≤ tableBound k x.length + certBound k x.length := by have := certLength_le_certBound k x.length @@ -474,7 +425,8 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) : exact hM.trans (Nat.le_add_right _ _) obtain ⟨w₃, -, -, hw, -⟩ := key _ (hpad _ hlen) rw [table_append hT'.1] at hw - exact absurd (complexity_le_of_tableVerifier hT'.1 (hw (not_le.1 hlt))) (not_le.2 hT'.2) + exact absurd (MCSP.complexity_le_of_tableVerifier hT'.1 (hw (not_le.1 hlt))) + (not_le.2 hT'.2) · obtain ⟨w₃, -, -, -, hw⟩ := key _ (hpad [] (Nat.zero_le _)) exact hw diff --git a/Complexity/Computability/MCSP/AntiChecker.lean b/Complexity/Computability/MCSP/AntiChecker.lean index 3b52f3b1b6..6e78c0e7c7 100644 --- a/Complexity/Computability/MCSP/AntiChecker.lean +++ b/Complexity/Computability/MCSP/AntiChecker.lean @@ -9,7 +9,6 @@ module public import Complexity.Computability.MCSP.Succinct public import Complexity.Foundations.Data.BitString.Threshold -import Complexity.Computability.Circuit.Complexity import Mathlib.Algebra.Order.BigOperators.Group.Finset import Mathlib.Data.Nat.Choose.Bounds @@ -230,16 +229,17 @@ exactly when `f` needs more than `s` gates on `S`. -/ theorem isAntiChecker_computableFunctions_iff {f : BooleanFunction n} {S : Set (BitString n)} : IsAntiChecker (computableFunctions n s) f S ↔ s < complexityOn interpretation S (single f) := by rw [← not_le, complexityOn_le_iff] + simp only [Circuit.computesOn_single_iff] constructor · rintro hS ⟨c, hc, hsize⟩ obtain ⟨x, hx, hne⟩ := hS (fun y => c.eval interpretation y 0) (Boolean.mem_computableFunctions.mpr - ⟨c, fun y => funext fun i => by rw [Subsingleton.elim i 0]; rfl, hsize⟩) - exact hne (congrFun (hc hx) 0) + ⟨c, Circuit.computes_single_iff.mpr fun _ => rfl, hsize⟩) + exact hne (hc x hx) · intro h g hg obtain ⟨c, hcg, hsize⟩ := Boolean.mem_computableFunctions.mp hg by_contra! hgS - exact h ⟨c, fun x hx => funext fun i => (congrFun (hcg x) i).trans (hgS x hx), hsize⟩ + exact h ⟨c, fun x hx => (Circuit.computes_single_iff.mp hcg x).trans (hgS x hx), hsize⟩ /-- Against the functions computable with at most `s` gates, `S` is an anti-checker for `f` exactly when the Succinct MCSP instance of the values of `f` on `S`, with threshold `s`, is a @@ -276,7 +276,7 @@ theorem exists_lt_complexityOn {m b : ℕ} (hm : 0 < m) (hnm : n ≤ m) {f : Boo have hle := complexity_strictMajority_le g rw [heq] at hle have hsum : ∑ i, complexity interpretation (single (g i)) ≤ ∑ _i : Fin m, s := - sum_le_sum fun i _ => mk_truthTable_mem_iff.mp (mk_truthTable_mem_iff_mem.mpr (hg i)) + sum_le_sum fun i _ => mem_computableFunctions_iff_complexity_le.mp (hg i) simp only [sum_const, card_univ, Fintype.card_fin, smul_eq_mul] at hsum omega obtain ⟨S, hS, hanti⟩ := exists_isAntiChecker hm hα _ hmaj hb diff --git a/Complexity/Computability/MCSP/Basic.lean b/Complexity/Computability/MCSP/Basic.lean index f73c110fc9..6fd97754cd 100644 --- a/Complexity/Computability/MCSP/Basic.lean +++ b/Complexity/Computability/MCSP/Basic.lean @@ -7,6 +7,9 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Circuit.Complexity +public import Complexity.Computability.Circuit.Counting +public import Complexity.Computability.Complexity.Classes.Promise.Basic public import Complexity.Foundations.Data.BitString.Basic public import Cslib.Computability.Circuit.Boolean.Complexity public import Cslib.Computability.Circuit.Boolean.Counting @@ -35,7 +38,8 @@ cslib's `computableFunctions n s`, so there are as many of them as such function * `Cslib.MCSP.truthTable`: truth tables of Boolean functions. * `Cslib.MCSP.Instance`, `Cslib.MCSP`: the instances and the yes-instances of MCSP. -* `Cslib.GapMCSP.yes`, `Cslib.GapMCSP.no`: the two sides of `GapMCSP[s₁, s₂]`. +* `Cslib.GapMCSP`: `GapMCSP[s₁, s₂]` as a `PromiseProblem`, with sides `Cslib.GapMCSP.yes` and + `Cslib.GapMCSP.no`. ## Main results @@ -43,7 +47,8 @@ cslib's `computableFunctions n s`, so there are as many of them as such function instances of MCSP, as circuits and as computable functions. * `Cslib.MCSP.ncard_setOf_mem`: the number of yes-instances of a given arity and threshold. * `Cslib.GapMCSP.disjoint_yes_no`: the promise of `GapMCSP[s₁, s₂]` is consistent when - `s₁ ≤ s₂`, and `Cslib.GapMCSP.no_eq_compl_yes`: `GapMCSP[s, s]` is MCSP at threshold `s`. + `s₁ ≤ s₂`, and `Cslib.GapMCSP.no_eq_compl_yes`, `Cslib.GapMCSP.eq_ofSet`: `GapMCSP[s, s]` is + MCSP at threshold `s`. ## References @@ -120,8 +125,7 @@ most `s`. -/ with at most `s` gates. -/ theorem mk_truthTable_mem_iff_mem {f : BooleanFunction n} : ⟨n, truthTable n f, s⟩ ∈ MCSP ↔ f ∈ computableFunctions n s := by - rw [mk_truthTable_mem_iff, mem_computableFunctions_iff_ecomplexity_le, ← natCast_complexity] - exact Nat.cast_le.symm + rw [mk_truthTable_mem_iff, mem_computableFunctions_iff_complexity_le] /-- An instance is a yes-instance exactly when some circuit with at most `threshold` gates computes its function. -/ @@ -132,8 +136,8 @@ theorem mem_iff_exists_circuit {x : Instance} : /-- The yes-instances are the truth tables of the functions computable within the threshold. -/ theorem mem_iff_mem_computableFunctions {x : Instance} : - x ∈ MCSP ↔ x.function ∈ computableFunctions x.arity x.threshold := by - rw [mem_iff_exists_circuit, mem_computableFunctions] + x ∈ MCSP ↔ x.function ∈ computableFunctions x.arity x.threshold := + mem_computableFunctions_iff_complexity_le.symm /-- Raising the threshold keeps a yes-instance a yes-instance. -/ theorem mem_of_le {T : BitString (2 ^ n)} (h : ⟨n, T, s⟩ ∈ MCSP) (hst : s ≤ t) : @@ -148,7 +152,8 @@ theorem ncard_setOf_mem (n s : ℕ) : truthTable n '' (computableFunctions n s : Set (BooleanFunction n)) := by ext T obtain ⟨f, rfl⟩ := (truthTable n).surjective T - simp [complexity_le_iff] + simp only [Set.mem_ofPred_eq, mk_truthTable_mem_iff_mem, Set.mem_image, SetLike.mem_coe, + EmbeddingLike.apply_eq_iff_eq, exists_eq_right] rw [h, Set.ncard_image_of_injective _ (truthTable n).injective, Set.ncard_coe_finset] end MCSP @@ -194,4 +199,30 @@ theorem no_anti {s₂' : ℕ → ℕ} (h : s₂ n ≤ s₂' n) : no s₂' n ⊆ end GapMCSP +/-- **`GapMCSP[s₁, s₂]` on functions of `n` inputs** [OliveiraPichSanthanam2019, Definition 2.4]: +the promise problem whose yes-instances are the truth tables of functions with circuits of at most +`s₁ n` gates and whose no-instances are those of functions that need more than `s₂ n` gates, when +`s₁ n ≤ s₂ n`. -/ +def GapMCSP (s₁ s₂ : ℕ → ℕ) (n : ℕ) (h : s₁ n ≤ s₂ n) : + Complexity.PromiseProblem (BitString (2 ^ n)) where + yes := GapMCSP.yes s₁ n + no := GapMCSP.no s₂ n + disjoint := GapMCSP.disjoint_yes_no h + +namespace GapMCSP + +variable {s₁ s₂ : ℕ → ℕ} {n : ℕ} + +@[simp] theorem yes_eq (h : s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ n h).yes = yes s₁ n := rfl + +@[simp] theorem no_eq (h : s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ n h).no = no s₂ n := rfl + +/-- At equal thresholds `s`, `GapMCSP[s, s]` is the decision problem `GapMCSP.yes s n`, MCSP on +`n` inputs at threshold `s`. -/ +@[simp] theorem eq_ofSet (s : ℕ → ℕ) (n : ℕ) : + GapMCSP s s n le_rfl = Complexity.PromiseProblem.ofSet (yes s n) := + Complexity.PromiseProblem.ext rfl (no_eq_compl_yes s n) + +end GapMCSP + end Cslib diff --git a/Complexity/Computability/MCSP/NP.lean b/Complexity/Computability/MCSP/NP.lean index 0c192ebb15..da515898b7 100644 --- a/Complexity/Computability/MCSP/NP.lean +++ b/Complexity/Computability/MCSP/NP.lean @@ -37,6 +37,7 @@ so they stay polynomially long in the length of the table. ## Main definitions * `Cslib.MCSP.encInstance`: the encoding of instances. +* `Cslib.MCSP.tableFunction`: the Boolean function read from a truth-table list. * `Cslib.MCSP.verifier`: the verifier. * `Cslib.MCSP.tableVerifier`: the verifier on the bits of a truth table and a threshold. @@ -45,6 +46,8 @@ so they stay polynomially long in the length of the table. * `Cslib.MCSP.mem_of_verifier_eq_true`, `Cslib.MCSP.exists_verifier_append`: the verifier accepts some certificate exactly for the instances in MCSP, certificates of a fixed length suffice, and bits after them are ignored. +* `Cslib.MCSP.complexity_le_of_tableVerifier`, `Cslib.MCSP.exists_tableVerifier_append`: soundness + and completeness of `tableVerifier` on truth-table lists of length `2 ^ m`. * `Cslib.MCSP.isVerifier`: the verifier is correct. * `Cslib.MCSP.computableTidilyInPolyTime_verifier`, `Cslib.MCSP.computableTidilyInPolyTime_tableVerifier`: the verifiers are polynomial-time. @@ -89,6 +92,10 @@ def budget (n s : ℕ) : ℕ := min s (2 ^ n * (2 * n + 3) + 1) def tableValue (table y : List Bool) : Bool := table.getD (BitString.boundedBinaryValue table.length y.reverse) false +/-- The function on `m` inputs with the truth table `T`, read as MCSP reads truth tables. -/ +def tableFunction (m : ℕ) (T : List Bool) : BooleanFunction m := + fun y => tableValue T (List.ofFn y) + /-- The verifier for MCSP: the certificate must describe a circuit on `n` inputs with at most `budget n s` gates (`readCertificate`) that agrees with the truth table on all `2 ^ n` inputs. -/ def verifier (p : Instance × List Bool) : Bool := @@ -108,6 +115,12 @@ theorem tableValue_ofFn (x : Instance) (y : BitString x.arity) : List.getElem_ofFn] rfl +/-- The truth table of a function, as a list, is read back as the function. -/ +@[simp] theorem tableFunction_ofFn_truthTable (m : ℕ) (f : BooleanFunction m) : + tableFunction m (List.ofFn (truthTable m f)) = f := by + funext y + exact (tableValue_ofFn ⟨m, truthTable m f, 0⟩ y).trans (by simp [Instance.function]) + /-- The polynomial bounding the length of certificates. -/ noncomputable def certPolynomial : Polynomial ℕ := 40 * (Polynomial.X + 1) ^ 4 @@ -140,10 +153,9 @@ theorem mem_of_verifier_eq_true {x : Instance} {w : List Bool} (hw : verifier (x have houtput : (c.outputs 0).toNat = r.2 := by have := congrArg (fun p => p.2.headD 0) hc simpa [Circuit.code] using this - refine complexity_le_iff.2 ⟨c, fun y => funext fun j => ?_, ?_⟩ - · rw [Fin.fin_one_eq_zero j, Circuit.eval_eq_evalOutput, houtput, show c.code.1 = r.1 by - rw [hc], hall _ (BitString.mem_enumList.2 (List.length_ofFn)), tableValue_ofFn, - single_apply] + refine complexity_le_iff.2 ⟨c, Circuit.computes_single_iff.2 fun y => ?_, ?_⟩ + · rw [Circuit.eval_eq_evalOutput, houtput, show c.code.1 = r.1 by rw [hc], + hall _ (BitString.mem_enumList.2 List.length_ofFn), tableValue_ofFn] · calc c.size = r.1.length := by rw [← Circuit.length_code_fst, hc] _ ≤ S := length_readCertificate_le _ _ _ _ ≤ x.threshold := Nat.min_le_left _ _ @@ -171,7 +183,7 @@ theorem exists_verifier_append {x : Instance} (hx : x ∈ MCSP) : obtain ⟨y, rfl⟩ : ∃ y' : BitString x.arity, List.ofFn y' = y := ⟨fun i => y[i.val]'(by rw [BitString.mem_enumList.1 hy]; exact i.isLt), List.ext_getElem (by simp [BitString.mem_enumList.1 hy]) fun _ _ _ => by simp⟩ - rw [← Circuit.eval_eq_evalOutput, hc y, tableValue_ofFn, single_apply] + rw [← Circuit.eval_eq_evalOutput, Circuit.computes_single_iff.1 hc y, tableValue_ofFn] /-- `MCSP.verifier` verifies MCSP, with certificates of length `certPolynomial`. -/ theorem isVerifier : IsVerifier encInstance certPolynomial verifier MCSP := by @@ -197,6 +209,42 @@ theorem verifier_eq_tableVerifier (p : Instance × List Bool) : simp only [tableVerifier, List.length_ofFn, Nat.log_pow Nat.one_lt_two] rfl +/-- The MCSP instance of a truth table of length `2 ^ m`. -/ +private def tableInstance (m s : ℕ) (T : List Bool) (hT : T.length = 2 ^ m) : Instance := + ⟨m, fun i => T[i.val]'(by rw [hT]; exact i.isLt), s⟩ + +private theorem ofFn_tableInstance {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) : + List.ofFn (tableInstance m s T hT).table = T := by + change List.ofFn (fun i : Fin (2 ^ m) => T[i.val]'(by rw [hT]; exact i.isLt)) = T + exact List.ext_getElem (by simp [hT]) fun _ _ _ => by simp + +private theorem function_tableInstance {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) : + (tableInstance m s T hT).function = tableFunction m T := by + funext y + rw [← tableValue_ofFn, ofFn_tableInstance hT] + rfl + +/-- An accepted certificate for a truth table of length `2 ^ m` bounds the complexity of its +function. -/ +theorem complexity_le_of_tableVerifier {m s : ℕ} {T c : List Bool} (hT : T.length = 2 ^ m) + (h : tableVerifier ((T, s), c) = true) : + complexity interpretation (single (tableFunction m T)) ≤ s := by + have := mem_of_verifier_eq_true (x := tableInstance m s T hT) (w := c) + (by rw [verifier_eq_tableVerifier, ofFn_tableInstance hT]; exact h) + rwa [mem_iff, function_tableInstance hT] at this + +/-- A truth table of length `2 ^ m` whose function has at most `s` gates has a certificate of +length `certLength m (budget m s)`, accepted whatever bits follow it. -/ +theorem exists_tableVerifier_append {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) + (h : complexity interpretation (single (tableFunction m T)) ≤ s) : + ∃ u : List Bool, u.length = certLength m (budget m s) ∧ + ∀ extra, tableVerifier ((T, s), u ++ extra) = true := by + obtain ⟨u, hu, hV⟩ := exists_verifier_append (x := tableInstance m s T hT) + (by rw [mem_iff, function_tableInstance hT]; exact h) + refine ⟨u, hu, fun extra => ?_⟩ + rw [← hV extra, verifier_eq_tableVerifier, ofFn_tableInstance hT] + rfl + /-- The verifier on raw data is polynomial-time. -/ theorem computableTidilyInPolyTime_tableVerifier : ComputableTidilyInPolyTime tableVerifier (encPair (encPair encBits encNat) encBits) encBool := by diff --git a/Complexity/Computability/MCSP/Succinct.lean b/Complexity/Computability/MCSP/Succinct.lean index 60e75500b7..374d5b91fa 100644 --- a/Complexity/Computability/MCSP/Succinct.lean +++ b/Complexity/Computability/MCSP/Succinct.lean @@ -85,26 +85,19 @@ variable {n s : ℕ} theorem mem_iff_exists_mem_computableFunctions {x : Instance} : x ∈ SuccinctMCSP ↔ ∃ g ∈ computableFunctions x.arity x.threshold, ∀ p ∈ x.samples, g p.1 = p.2 := by - simp only [mem_computableFunctions] - constructor - · rintro ⟨c, hc, hp⟩ - exact ⟨fun y => c.eval interpretation y 0, - ⟨c, fun y => funext fun i => by rw [Subsingleton.elim i 0]; rfl, hc⟩, hp⟩ - · rintro ⟨g, ⟨c, hcg, hc⟩, hp⟩ - exact ⟨c, hc, fun p hpx => (congrFun (hcg p.1) 0).trans (hp p hpx)⟩ + simp only [mem_computableFunctions, Circuit.computes_single_iff] + exact ⟨fun ⟨c, hc, hp⟩ => ⟨fun y => c.eval interpretation y 0, ⟨c, fun _ => rfl, hc⟩, hp⟩, + fun ⟨g, ⟨c, hcg, hc⟩, hp⟩ => ⟨c, hc, fun p hpx => (hcg p.1).trans (hp p hpx)⟩⟩ /-- Samples of `f` on `S` are a yes-instance exactly when `f` has complexity at most `s` on `S`. -/ theorem ofFunction_mem_iff {f : BooleanFunction n} {S : Finset (BitString n)} : Instance.ofFunction f S s ∈ SuccinctMCSP ↔ complexityOn interpretation S (single f) ≤ s := by rw [complexityOn_le_iff] simp only [SuccinctMCSP, Instance.ofFunction, Set.mem_ofPred_eq, Finset.mem_image, - forall_exists_index, and_imp, Prod.forall, Prod.mk.injEq] - refine exists_congr fun c => ⟨fun ⟨hc, hp⟩ => ⟨fun x hx => funext fun i => ?_, hc⟩, - fun ⟨hc, hs⟩ => ⟨hs, ?_⟩⟩ - · rw [Subsingleton.elim i 0] - exact hp x (f x) x hx rfl rfl - · rintro x b y hy rfl rfl - exact congrFun (hc hy) 0 + forall_exists_index, and_imp, Prod.forall, Prod.mk.injEq, Circuit.computesOn_single_iff, + Finset.mem_coe] + exact exists_congr fun c => ⟨fun ⟨hc, hp⟩ => ⟨fun x hx => hp x (f x) x hx rfl rfl, hc⟩, + fun ⟨hc, hs⟩ => ⟨hs, by rintro _ _ y hy rfl rfl; exact hc y hy⟩⟩ /-- With every input as a sample, Succinct MCSP is MCSP. -/ theorem ofFunction_univ_mem_iff {f : BooleanFunction n} : diff --git a/ComplexityTests/Kannan.lean b/ComplexityTests/Kannan.lean index 201b0299c6..1d78fdcd9a 100644 --- a/ComplexityTests/Kannan.lean +++ b/ComplexityTests/Kannan.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger import Complexity.Computability.Circuit.Boolean.Hierarchy import Complexity.Computability.Complexity.Classes.PH.Kannan +import Complexity.Computability.MCSP.Basic /-! # Tests for Kannan's theorem @@ -33,10 +34,14 @@ example : Kannan.certBound 0 0 = 16 := rfl /-! ### Truth tables -/ -- Truth tables are indexed by the input read least significant bit first. -example : Kannan.tableFunction 2 [false, true, true, false] ![true, false] = true := by decide -example : Kannan.tableFunction 2 [false, true, true, false] ![true, true] = false := by decide +example : MCSP.tableFunction 2 [false, true, true, false] ![true, false] = true := by decide +example : MCSP.tableFunction 2 [false, true, true, false] ![true, true] = false := by decide example : Kannan.table 0 0 (List.replicate 10 true) = List.replicate 8 true := by decide +-- GapMCSP bundles `GapMCSP.yes`, `GapMCSP.no`, and `GapMCSP.disjoint_yes_no` as a `PromiseProblem`. +example (s : ℕ → ℕ) (n : ℕ) : + GapMCSP s s n le_rfl = PromiseProblem.ofSet (GapMCSP.yes s n) := by simp + example : BitString.binaryValue [true, false, true] = 5 := by decide example {u v : List Bool} (hlen : u.length = v.length) (h : BitString.binaryValue u = BitString.binaryValue v) : u = v := @@ -124,6 +129,24 @@ info: 'Cslib.MCSP.computableTidilyInPolyTime_tableVerifier' depends on axioms: [ #guard_msgs in #print axioms Cslib.MCSP.computableTidilyInPolyTime_tableVerifier +/-- +info: 'Cslib.MCSP.complexity_le_of_tableVerifier' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.MCSP.complexity_le_of_tableVerifier + +/-- +info: 'Cslib.MCSP.exists_tableVerifier_append' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.MCSP.exists_tableVerifier_append + +/-- +info: 'Cslib.GapMCSP' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.GapMCSP + /-- info: 'Cslib.Complexity.Kannan.language_notMem_SIZE' depends on axioms: [propext, Classical.choice, Quot.sound] -/