From 1a372aaedec70dd86dcbe4a38eb836ab552c8c2b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:15:53 -0400 Subject: [PATCH 1/2] refactor(classes): make proof helpers private, second pass Second pass of #610 item 2, over the classes-area modules that the first pass (#634) skipped because the deprecation sweep (#631), #632 or #621 edited them. Makes 199 theorems and definitions private in 25 modules with the same rule as #634: a privatization candidate of `scripts/quality_report.py` (no reference from another module, test or abstract, not named in a module doc, no implicit-use attribute, not pinned by a public statement or exposed body) that its own module uses and whose name is not API-shaped. Statements and proofs are unchanged; only the `private` modifier and signature line breaks change. Three definitions of `ValiantVazirani/Reduction` (`point`, `auxValue`, `solutions`) stay public because public declarations of that module need them. Modules that #610 item 9 moves to Machines, the graph modules of #689 and files under other open PRs are left out. Refs #610 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Complexity/AffineDisperser/PolyTime.lean | 31 +++++----- .../Classes/ArthurMerlin/Amplification.lean | 12 ++-- .../ArthurMerlin/GraphNonIsomorphism.lean | 36 ++++++------ .../Complexity/Classes/Hierarchy.lean | 2 +- .../Complexity/Classes/Hierarchy/Time.lean | 4 +- .../Computability/Complexity/Classes/IP.lean | 10 ++-- .../Complexity/Classes/IP/OptimalProver.lean | 21 +++---- .../Complexity/Classes/IP/PSPACE.lean | 47 ++++++++------- .../Complexity/Classes/IP/TQBF.lean | 22 +++---- .../Complexity/Classes/IP/TQBF/Protocol.lean | 2 +- .../Complexity/Classes/IP/TQBF/Verifier.lean | 10 ++-- .../Complexity/Classes/Ladner/PolyTime.lean | 22 +++---- .../Complexity/Classes/Oracle/PP.lean | 5 +- .../Complexity/Classes/Promise/Reduction.lean | 4 +- .../Classes/ValiantVazirani/Reduction.lean | 57 ++++++++++--------- .../Computability/Complexity/Fagin/Power.lean | 17 +++--- .../Complexity/Fagin/StrictVerifier.lean | 2 +- .../Complexity/Problems/CircuitValue.lean | 2 +- .../Problems/Hamiltonian/Directed.lean | 4 +- .../Computability/Complexity/ProofSystem.lean | 4 +- .../PCP/Approximation/Hastad/LinearTest.lean | 2 +- .../Sensitivity/Hypercube.lean | 7 ++- .../TreeEval/Reader/Cert/Weight.lean | 22 +++---- .../TreeEval/Reader/Correct.lean | 46 ++++++++------- .../Computability/USTCON/Reader/Correct.lean | 24 ++++---- 25 files changed, 216 insertions(+), 199 deletions(-) diff --git a/Complexity/Computability/Complexity/AffineDisperser/PolyTime.lean b/Complexity/Computability/Complexity/AffineDisperser/PolyTime.lean index 45bf19583..38c1a5b0a 100644 --- a/Complexity/Computability/Complexity/AffineDisperser/PolyTime.lean +++ b/Complexity/Computability/Complexity/AffineDisperser/PolyTime.lean @@ -84,7 +84,7 @@ theorem computableTidilyInPolyTime_mulXMod : unfold mulXMod fun_prop -theorem length_mulXMod_le (g r : List Bool) : (mulXMod g r).length ≤ g.length - 1 := +private theorem length_mulXMod_le (g r : List Bool) : (mulXMod g r).length ≤ g.length - 1 := List.length_take_le _ _ /-- The remainder modulo a binary polynomial, by a left fold over the coefficients whose state, the @@ -150,7 +150,7 @@ theorem computableTidilyInPolyTime_powerTable : /-! ### Lists of unary naturals -/ /-- Take a unary number of elements of a framed list, by reversing and dropping. -/ -theorem computableTidilyInPolyTime_take {α : Type} (enc : α ↪ List Bool) : +private theorem computableTidilyInPolyTime_take {α : Type} (enc : α ↪ List Bool) : ComputableTidilyInPolyTime (fun p : List α × ℕ => p.1.take p.2) (encPair (encList enc) encUnary) (encList enc) := by have hrev := (listReverse enc).comp (fst (encList enc) encUnary) @@ -163,7 +163,8 @@ theorem computableTidilyInPolyTime_take {α : Type} (enc : α ↪ List Bool) : /-- The product of a computed list of positive unary naturals, when the product is polynomially bounded: every partial product is at most the whole product. -/ -theorem computableTidilyInPolyTime_prod_of_le {α : Type} {input : α ↪ List Bool} {list : α → List ℕ} +private theorem computableTidilyInPolyTime_prod_of_le {α : Type} {input : α ↪ List Bool} + {list : α → List ℕ} (hlist : ComputableTidilyInPolyTime list input (encList encUnary)) (hpos : ∀ a, ∀ p ∈ list a, 0 < p) {B : α → ℕ} (hB : PolyBounded (fun a => (input a).length) B) (hle : ∀ a, (list a).prod ≤ B a) : @@ -202,7 +203,7 @@ theorem computableTidilyInPolyTime_primesIoc : def selectStep (state : ℕ × List ℕ) (p : ℕ) : ℕ × List ℕ := if p ≤ state.1 then (state.1 / p, state.2 ++ [p]) else state -theorem foldl_selectStep (T : ℕ) (ps chosen : List ℕ) : +private theorem foldl_selectStep (T : ℕ) (ps chosen : List ℕ) : (ps.foldl selectStep (T, chosen)).2 = chosen ++ selectBelow T ps := by induction ps generalizing T chosen with | nil => simp [selectBelow] @@ -255,14 +256,14 @@ theorem computableTidilyInPolyTime_degreePrimes : unfold degreePrimes fun_prop -theorem selectBelow_zero {ps : List ℕ} (hps : ∀ p ∈ ps, 0 < p) : selectBelow 0 ps = [] := by +private theorem selectBelow_zero {ps : List ℕ} (hps : ∀ p ∈ ps, 0 < p) : selectBelow 0 ps = [] := by induction ps with | nil => rfl | cons p ps ih => rw [selectBelow, ite_eq_right_iff.2 (by have := hps p List.mem_cons_self; omega)] exact ih fun q hq => hps q (List.mem_cons_of_mem _ hq) -theorem prod_degreePrimes_le (N : ℕ) : (degreePrimes N).prod ≤ N + 1 := by +private theorem prod_degreePrimes_le (N : ℕ) : (degreePrimes N).prod ≤ N + 1 := by rcases Nat.eq_zero_or_pos (N / (Nat.log 2 N + 1) ^ 2) with hT | hT · rw [degreePrimes, hT, selectBelow_zero fun p hp => (mem_primesIoc.1 hp).2.2.pos] simp @@ -328,7 +329,7 @@ theorem computableTidilyInPolyTime_explicitPowerTables : /-- The mixed-radix digits in the radix of the field degree on `N` bits; every partial product of the radix is at most `N + 1`. -/ -theorem computableTidilyInPolyTime_mixedDigit_degreePrimes : +private theorem computableTidilyInPolyTime_mixedDigit_degreePrimes : ComputableTidilyInPolyTime (fun q : (ℕ × ℕ) × ℕ => mixedDigit (degreePrimes q.1.1) q.1.2 q.2) (encPair (encPair encUnary encUnary) encUnary) encUnary := by have htake : ComputableTidilyInPolyTime (fun q : (ℕ × ℕ) × ℕ => (degreePrimes q.1.1).take q.2) @@ -358,7 +359,7 @@ theorem computableTidilyInPolyTime_mixedDigit_degreePrimes' {α : Type} {input : /-- Coordinates of the products of monomials of the explicit field on `N` bits, `N` in unary. -/ -theorem computableTidilyInPolyTime_monomialBit_explicit : ComputableTidilyInPolyTime +private theorem computableTidilyInPolyTime_monomialBit_explicit : ComputableTidilyInPolyTime (fun q : ((ℕ × ℕ) × ℕ) × ℕ => monomialBit (degreePrimes q.1.1.1) (explicitPowerTables q.1.1.1) q.1.1.2 q.1.2 q.2) (encPair (encPair (encPair encUnary encUnary) encUnary) encUnary) encBool := by @@ -426,7 +427,7 @@ theorem length_fieldMul (tab : List (List (List Bool))) (a b : List Bool) : /-- The powers `y ^ (2 ^ (k + 1) - 1)`, by `k` multiplications and squarings; every intermediate power has `n` coordinates. -/ -theorem computableTidilyInPolyTime_powerPred : ComputableTidilyInPolyTime +private theorem computableTidilyInPolyTime_powerPred : ComputableTidilyInPolyTime (fun p : List (List (List Bool)) × List Bool × ℕ => powerPred p.1 p.2.1 p.2.2) (encPair encTable (encPair encBits encUnary)) encBits := by unfold powerPred @@ -446,20 +447,20 @@ theorem computableTidilyInPolyTime_powerPred' {α : Type} {input : α ↪ List B computableTidilyInPolyTime_powerPred.comp (htab.prod (hy.prod hk)) /-- One step of the dynamic program for the elementary symmetric polynomials. -/ -theorem computableTidilyInPolyTime_esymmStep : ComputableTidilyInPolyTime +private theorem computableTidilyInPolyTime_esymmStep : ComputableTidilyInPolyTime (fun p : (List (List (List Bool)) × List (List Bool)) × List Bool => esymmStep p.1.1 p.1.2 p.2) (encPair (encPair encTable (encList encBits)) encBits) (encList encBits) := by unfold esymmStep fun_prop -theorem length_esymmStep (tab : List (List (List Bool))) (E : List (List Bool)) +private theorem length_esymmStep (tab : List (List (List Bool))) (E : List (List Bool)) (z : List Bool) : (esymmStep tab E z).length = E.length := by simp [esymmStep] /-- **The elementary symmetric polynomial `e_t` in coordinates**: the dynamic program keeps `t` words of at most `n` coordinates. -/ -theorem computableTidilyInPolyTime_esymmCoords : ComputableTidilyInPolyTime +private theorem computableTidilyInPolyTime_esymmCoords : ComputableTidilyInPolyTime (fun p : (List (List (List Bool)) × ℕ) × List (List Bool) => esymmCoords p.1.1 p.1.2 p.2) (encPair (encPair encTable encUnary) (encList encBits)) encBits := by have hsize : ComputableTidilyInPolyTime @@ -503,7 +504,7 @@ theorem computableTidilyInPolyTime_esymmCoords' {α : Type} {input : α ↪ List computableTidilyInPolyTime_esymmCoords.comp ((htab.prod ht).prod hzs) /-- The traces of the basis elements, from the diagonals of the multiplication table. -/ -theorem computableTidilyInPolyTime_traceVector : +private theorem computableTidilyInPolyTime_traceVector : ComputableTidilyInPolyTime traceVector encTable encBits := by unfold traceVector fun_prop @@ -516,7 +517,7 @@ theorem computableTidilyInPolyTime_traceVector' {α : Type} {input : α ↪ List simpa only [Function.comp_def] using computableTidilyInPolyTime_traceVector.comp htab /-- The trace as a bit. -/ -theorem computableTidilyInPolyTime_traceBit : ComputableTidilyInPolyTime +private theorem computableTidilyInPolyTime_traceBit : ComputableTidilyInPolyTime (fun p : List Bool × List Bool => traceBit p.1 p.2) (encPair encBits encBits) encBool := by unfold traceBit fun_prop @@ -541,7 +542,7 @@ theorem computableTidilyInPolyTime_traceSymCoords : ComputableTidilyInPolyTime /-! ### The explicit disperser -/ /-- **The program is polynomial-time.** -/ -theorem computableTidilyInPolyTime_explicitDisperserProgram : +private theorem computableTidilyInPolyTime_explicitDisperserProgram : ComputableTidilyInPolyTime explicitDisperserProgram encBits encBool := by unfold explicitDisperserProgram simpa only [Function.comp_def] using computableTidilyInPolyTime_traceSymCoords.comp diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean index 92f5d031b..6ed996260 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean @@ -123,7 +123,8 @@ theorem computableTidilyInPolyTime_merlinArthurRepeat {V : α × List Bool → B /-- 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)`. -/ -theorem merlinArthurRepeat_ofFn_append_ofFn {q r p : Polynomial ℕ} {V : α × List Bool → Bool} +private theorem merlinArthurRepeat_ofFn_append_ofFn {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 < @@ -168,7 +169,8 @@ theorem IsMerlinArthurVerifier.repeatMajority {q p : Polynomial ℕ} {V : α × omega /-- Error at most `2 ^ (-e(n)) ≤ 1 / 4` is error at most `1 / 3`. -/ -theorem IsMerlinArthurVerifierWithErrorExponent.isMerlinArthurVerifier {e q p : Polynomial ℕ} +private 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 := @@ -235,7 +237,8 @@ theorem computableTidilyInPolyTime_arthurMerlinRepeat {V : α × List Bool → B /-- On `2 r(n)` rows followed by `2 r(n)` replies, the parallel majority vote compares the number of rows accepted with their replies with `r(n)`. -/ -theorem arthurMerlinRepeat_ofFn_append_ofFn {r p q : Polynomial ℕ} {V : α × List Bool → Bool} +private theorem arthurMerlinRepeat_ofFn_append_ofFn {r p q : Polynomial ℕ} + {V : α × List Bool → Bool} (a : α) (x : BitString (2 * r.eval (enc a).length * p.eval (enc a).length)) (y : BitString (2 * r.eval (enc a).length * q.eval (enc a).length)) : arthurMerlinRepeat enc r p q V (a, List.ofFn x ++ List.ofFn y) = @@ -323,7 +326,8 @@ theorem IsArthurMerlinVerifier.repeatMajority {p q : Polynomial ℕ} {V : α × omega /-- Error at most `2 ^ (-e(n)) ≤ 1 / 4` is error at most `1 / 3`. -/ -theorem IsArthurMerlinVerifierWithErrorExponent.isArthurMerlinVerifier {e p q : Polynomial ℕ} +private 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 := diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean index b21b5473c..7a9352e85 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean @@ -85,12 +85,12 @@ namespace PublicCoin variable {n : ℕ} /-- Relabelling by a product of permutations is relabelling twice. -/ -theorem reindex_mul (σ τ : Equiv.Perm (Fin n)) (M : Matrix (Fin n) (Fin n) Bool) : +private theorem reindex_mul (σ τ : Equiv.Perm (Fin n)) (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex (σ * τ) (σ * τ) M = Matrix.reindex σ σ (Matrix.reindex τ τ M) := (DFunLike.congr_fun (Matrix.reindex_trans τ τ σ σ) M).symm /-- Relabelling by the identity permutation does nothing. -/ -theorem reindex_one (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex 1 1 M = M := +private theorem reindex_one (M : Matrix (Fin n) (Fin n) Bool) : Matrix.reindex 1 1 M = M := Matrix.reindex_refl_refl M /-- `Matrix.reindex τ τ A = M` says that `τ` carries `A` to `M`. -/ @@ -107,7 +107,7 @@ theorem reindex_eq_iff {τ : Equiv.Perm (Fin n)} {A M : Matrix (Fin n) (Fin n) B def orbit (A : Matrix (Fin n) (Fin n) Bool) : Finset (Matrix (Fin n) (Fin n) Bool) := univ.image fun τ => Matrix.reindex τ τ A -theorem mem_orbit {A M : Matrix (Fin n) (Fin n) Bool} : +private theorem mem_orbit {A M : Matrix (Fin n) (Fin n) Bool} : M ∈ orbit A ↔ ∃ τ, Matrix.reindex τ τ A = M := by simp [orbit] @@ -129,7 +129,7 @@ def pairs (A : Matrix (Fin n) (Fin n) Bool) : /-- A relabelling `M` of `A` has as many automorphisms as there are permutations carrying `A` to `M`: composing with one permutation carrying `A` to `M` is a bijection. -/ -theorem card_filter_reindex_eq {A M : Matrix (Fin n) (Fin n) Bool} (hM : M ∈ orbit A) : +private theorem card_filter_reindex_eq {A M : Matrix (Fin n) (Fin n) Bool} (hM : M ∈ orbit A) : #{σ : Equiv.Perm (Fin n) | Matrix.reindex σ σ M = M} = #{τ : Equiv.Perm (Fin n) | Matrix.reindex τ τ A = M} := by obtain ⟨τ₀, rfl⟩ := mem_orbit.1 hM @@ -189,14 +189,14 @@ private theorem index_symm {q : ℕ} (h : q < n * n) : def matrixBit (A : Matrix (Fin n) (Fin n) Bool) (q : ℕ) : Bool := if h : q < n * n then BitString.blocksEquiv.symm (Matrix.of.symm A) ⟨q, h⟩ else false -theorem matrixBit_index (A : Matrix (Fin n) (Fin n) Bool) (i j : Fin n) : +private theorem matrixBit_index (A : Matrix (Fin n) (Fin n) Bool) (i j : Fin n) : matrixBit A (i * n + j) = A i j := by have hq : (⟨i * n + j, index_lt i j⟩ : Fin (n * n)) = finProdFinEquiv (i, j) := Fin.ext (val_finProdFinEquiv i j).symm simp only [matrixBit, index_lt i j, ↓reduceDIte, hq, BitString.blocksEquiv_symm_apply, Matrix.of_symm_apply, Equiv.symm_apply_apply] -theorem matrixBit_of_le (A : Matrix (Fin n) (Fin n) Bool) {q : ℕ} (h : n * n ≤ q) : +private theorem matrixBit_of_le (A : Matrix (Fin n) (Fin n) Bool) {q : ℕ} (h : n * n ≤ q) : matrixBit A q = false := by simp [matrixBit, Nat.not_lt.2 h] @@ -214,11 +214,11 @@ def code (E : ℕ) (M : Matrix (Fin n) (Fin n) Bool) (σ : Equiv.Perm (Fin n)) : /-- Bit `q` of a certificate naming the graph `b` and a permutation `τ`: `b`, then the entries of the matrix of `τ`, row by row, then `false`. -/ -def certBit (b : Bool) (τ : Equiv.Perm (Fin n)) (q : ℕ) : Bool := +private def certBit (b : Bool) (τ : Equiv.Perm (Fin n)) (q : ℕ) : Bool := if q = 0 then b else matrixBit (Matrix.of fun i j => decide (τ i = j)) (q - 1) /-- A certificate naming the graph `b` and a permutation `τ`, in `C` bits. -/ -def cert (C : ℕ) (b : Bool) (τ : Equiv.Perm (Fin n)) : BitString C := +private def cert (C : ℕ) (b : Bool) (τ : Equiv.Perm (Fin n)) : BitString C := fun q => certBit b τ q private theorem getD_ofFn {E : ℕ} (x : BitString E) {p : ℕ} (hp : p < E) : @@ -226,15 +226,15 @@ private theorem getD_ofFn {E : ℕ} (x : BitString E) {p : ℕ} (hp : p < E) : rw [List.getD_eq_getElem _ _ (by simpa using hp), List.getElem_ofFn] /-- The matrix read from the first `n * n` bits of a word. -/ -def decodeMatrix (n : ℕ) (u : List Bool) : Matrix (Fin n) (Fin n) Bool := +private def decodeMatrix (n : ℕ) (u : List Bool) : Matrix (Fin n) (Fin n) Bool := Matrix.of fun i j => u.getD (i * n + j) false /-- The map read from the matrix starting after `k` bits of a word: row `i` selects its first set bit (`Cslib.Complexity.GraphIsomorphism.image`). -/ -def decodeMap (n k : ℕ) (u : List Bool) (i : Fin n) : Fin n := +private def decodeMap (n k : ℕ) (u : List Bool) (i : Fin n) : Fin n := ⟨GraphIsomorphism.image n (u.drop k) i, GraphIsomorphism.image_lt _ _ i.pos⟩ -theorem decodeMatrix_code {E : ℕ} (hE : n * n ≤ E) (M : Matrix (Fin n) (Fin n) Bool) +private theorem decodeMatrix_code {E : ℕ} (hE : n * n ≤ E) (M : Matrix (Fin n) (Fin n) Bool) (σ : Equiv.Perm (Fin n)) : decodeMatrix n (List.ofFn (code E M σ)) = M := by ext i j rw [decodeMatrix, Matrix.of_apply, getD_ofFn _ ((index_lt i j).trans_le hE)] @@ -245,7 +245,7 @@ private theorem decide_val_eq {σ : Equiv.Perm (Fin n)} {i : Fin n} {j : ℕ} (h decide (σ i = ⟨j, hj⟩) = decide (j = σ i) := decide_eq_decide.2 ⟨fun h => by rw [h], fun h => Fin.ext h.symm⟩ -theorem decodeMap_code {E : ℕ} (hE : 2 * (n * n) ≤ E) (M : Matrix (Fin n) (Fin n) Bool) +private theorem decodeMap_code {E : ℕ} (hE : 2 * (n * n) ≤ E) (M : Matrix (Fin n) (Fin n) Bool) (σ : Equiv.Perm (Fin n)) : decodeMap n (n * n) (List.ofFn (code E M σ)) = σ := by funext i refine Fin.ext (GraphIsomorphism.image_eq (σ i).2 fun j hj => ?_) @@ -256,12 +256,12 @@ theorem decodeMap_code {E : ℕ} (hE : 2 * (n * n) ≤ E) (M : Matrix (Fin n) (F Nat.add_sub_cancel_left] rw [matrixBit_index _ i ⟨j, hj⟩, Matrix.of_apply, decide_val_eq hj] -theorem getD_ofFn_cert_zero {C : ℕ} (hC : 0 < C) (b : Bool) (τ : Equiv.Perm (Fin n)) : +private theorem getD_ofFn_cert_zero {C : ℕ} (hC : 0 < C) (b : Bool) (τ : Equiv.Perm (Fin n)) : (List.ofFn (cert C b τ)).getD 0 false = b := by rw [getD_ofFn _ hC] simp [cert, certBit] -theorem decodeMap_cert {C : ℕ} (hC : n * n + 1 ≤ C) (b : Bool) (τ : Equiv.Perm (Fin n)) : +private theorem decodeMap_cert {C : ℕ} (hC : n * n + 1 ≤ C) (b : Bool) (τ : Equiv.Perm (Fin n)) : decodeMap n 1 (List.ofFn (cert C b τ)) = τ := by funext i refine Fin.ext (GraphIsomorphism.image_eq (τ i).2 fun j hj => ?_) @@ -332,14 +332,14 @@ section Check variable {E : ℕ} {adj : Bool → ℕ → ℕ → Bool} {u v : List Bool} -theorem injective_decodeMap_left (h : check n E adj u v = true) : +private theorem injective_decodeMap_left (h : check n E adj u v = true) : Function.Injective (decodeMap n (n * n) u) := by intro i j hij rcases ((check_eq_true_iff.1 h).2 i i.2 j j.2).2.1 with h' | h' · exact Fin.ext h' · exact absurd (congrArg Fin.val hij) h' -theorem injective_decodeMap_right (h : check n E adj u v = true) : +private theorem injective_decodeMap_right (h : check n E adj u v = true) : Function.Injective (decodeMap n 1 v) := by intro i j hij rcases ((check_eq_true_iff.1 h).2 i i.2 j j.2).2.2.2.1 with h' | h' @@ -347,7 +347,7 @@ theorem injective_decodeMap_right (h : check n E adj u v = true) : · exact absurd (congrArg Fin.val hij) h' /-- The map selected by an accepted element is an automorphism of its matrix. -/ -theorem reindex_decodeMatrix (h : check n E adj u v = true) : +private theorem reindex_decodeMatrix (h : check n E adj u v = true) : Matrix.reindex (Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (injective_decodeMap_left h))) (Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (injective_decodeMap_left h))) @@ -356,7 +356,7 @@ theorem reindex_decodeMatrix (h : check n E adj u v = true) : reindex_eq_iff.2 fun i j => ((check_eq_true_iff.1 h).2 i i.2 j j.2).2.2.1 /-- The matrix of an accepted element is a relabelling of the graph named by the certificate. -/ -theorem decodeMatrix_mem_orbit (h : check n E adj u v = true) : +private theorem decodeMatrix_mem_orbit (h : check n E adj u v = true) : decodeMatrix n u ∈ orbit (Matrix.of fun i j : Fin n => adj (v.getD 0 false) i j) := mem_orbit.2 ⟨Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (injective_decodeMap_right h)), diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy.lean b/Complexity/Computability/Complexity/Classes/Hierarchy.lean index 53c84d60a..fce87bbce 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy.lean @@ -192,7 +192,7 @@ theorem computableTidilyInO_verdict : /-- The numeric core of the resources of the diagonal: for an input of length `n`, a decoded description of encoded length `D`, encoded symbols of length `N`, a clock `J ≥ 1` and a result of encoded length `E`, everything is within `K * M ^ 5 * J ^ 3` steps and `K * M ^ 5 * J` cells. -/ -theorem bounds_aux {n A D N J L I E cD cO M K : ℕ} (hJ : 1 ≤ J) +private theorem bounds_aux {n A D N J L I E cD cO M K : ℕ} (hJ : 1 ≤ J) (hD : D ≤ cD * (A + 1)) (hN : N ≤ 3 * n) (hL : L = n + 1) (hI : I = 2 * D + 1 + (2 * N + 1 + L)) (hM : M = cD * (A + 1) + A + 4 * n + 2) (hK : K = 100100 + 44100 * (cO + 1) ^ 2) (hE : E ≤ cO * (A + (n + n) + (runBound D N J + I) + 1)) : diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean index 5f31d36e4..a79cc08df 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean @@ -87,7 +87,7 @@ open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Universal Filter namespace Diagonal /-- The space of the universal run grows with the number of steps. -/ -theorem runBound_le_succ (D N J : ℕ) : runBound D N J ≤ runBound D N (J + 1) := by +private theorem runBound_le_succ (D N J : ℕ) : runBound D N J ≤ runBound D N (J + 1) := by simp only [runBound, ctxBound, cfgBound, tapeBound] gcongr <;> omega @@ -95,7 +95,7 @@ theorem runBound_le_succ (D N J : ℕ) : runBound D N J ≤ runBound D N (J + 1) decoding time `A` linear in `n`, a decoded description of encoded length `D`, encoded symbols of length `N`, a clock `J` of `L` binary digits and a result of encoded length `E`, everything is within `K * (n + 1) ^ 5 * (J + 1) ^ 3` steps and cells. -/ -theorem clockedBounds_aux (cA cD cO C₂ : ℕ) : ∃ K, ∀ {n A D N J L I E : ℕ}, +private theorem clockedBounds_aux (cA cD cO C₂ : ℕ) : ∃ K, ∀ {n A D N J L I E : ℕ}, A ≤ cA * (n + 1) → D ≤ cD * (n + A + 1) → N ≤ 3 * n → (L + 1) ^ 2 ≤ C₂ * (J + 1) → I = 2 * D + 1 + (2 * N + 1 + L) → E ≤ cO * (n + A + (n + J) + (runBound D N J + I) + 1) → diff --git a/Complexity/Computability/Complexity/Classes/IP.lean b/Complexity/Computability/Complexity/Classes/IP.lean index b69f768f9..1ff6e4018 100644 --- a/Complexity/Computability/Complexity/Classes/IP.lean +++ b/Complexity/Computability/Complexity/Classes/IP.lean @@ -161,7 +161,7 @@ theorem acceptProb_sample_bind {β : Type} (program : ProbComp β) rfl /-- A verifier none of whose possible results accepts has acceptance probability zero. -/ -theorem acceptProb_eq_zero {verifier : WordOracleComp Operation Bool} (P : Prover Operation) +private theorem acceptProb_eq_zero {verifier : WordOracleComp Operation Bool} (P : Prover Operation) (h : ∀ x ∈ (P.run verifier P.init).support, x.1 = false) : acceptProb verifier P = 0 := by rw [acceptProb, PMF.apply_eq_zero_iff, PMF.support_map] rintro ⟨x, hx, hx'⟩ @@ -223,7 +223,7 @@ def npVerifier (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Boo /-- The one-message verifier of a polynomial-time `NP` verifier is strict oracle PPT: it reads only a polynomially long prefix of the prover's reply. -/ -theorem isOraclePPTOn_npVerifier {p : Polynomial ℕ} {V : α × List Bool → Bool} +private theorem isOraclePPTOn_npVerifier {p : Polynomial ℕ} {V : α × List Bool → Bool} (hV : ComputableTidilyInPolyTime V (encPair enc encBits) encBool) : IsOraclePPTOn enc encBool (npVerifier enc p V) := by unfold npVerifier @@ -258,12 +258,12 @@ theorem NP_subset_IP (enc : α ↪ List Bool) : NP enc ⊆ IP enc := by /-- The interactive proof without messages for a bounded-error decider `V` with random strings of length `p`: sample a random string and run `V`. -/ -noncomputable def bppVerifier (enc : α ↪ List Bool) (p : Polynomial ℕ) +private noncomputable def bppVerifier (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) : WordOracleComp Unit Bool := ProbOracleComp.sample ((fun r => V (a, r)) <$> BitString.sampleList (p.eval (enc a).length)) /-- The verifier without messages of a polynomial-time decider is strict oracle PPT. -/ -theorem isOraclePPTOn_bppVerifier {p : Polynomial ℕ} {V : α × List Bool → Bool} +private theorem isOraclePPTOn_bppVerifier {p : Polynomial ℕ} {V : α × List Bool → Bool} (hV : ComputableTidilyInPolyTime V (encPair enc encBits) encBool) : IsOraclePPTOn enc encBool (bppVerifier enc p V) := by have hcount : ComputableTidilyInPolyTime (fun a => p.eval (enc a).length) enc encUnary := by @@ -272,7 +272,7 @@ theorem isOraclePPTOn_bppVerifier {p : Polynomial ℕ} {V : α × List Bool → /-- The verifier without messages accepts every prover with the fraction of accepted random strings. -/ -theorem acceptProb_bppVerifier {p : Polynomial ℕ} {V : α × List Bool → Bool} (a : α) +private theorem acceptProb_bppVerifier {p : Polynomial ℕ} {V : α × List Bool → Bool} (a : α) (P : Prover Unit) : acceptProb (bppVerifier enc p V a) P = (Finset.univ.filter fun r : Fin (p.eval (enc a).length) → Bool => diff --git a/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean b/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean index bdf89eafd..c5e71779a 100644 --- a/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean +++ b/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean @@ -99,7 +99,7 @@ theorem after_query_bind_cons (m : List Bool) (next : List Bool → WordQueryCom if m' = m then after (next y) h else none := rfl /-- What remains after a concatenation is what remains of what remains. -/ -theorem after_append (p : WordQueryComp Unit α) (h e : History) : +private theorem after_append (p : WordQueryComp Unit α) (h e : History) : after p (h ++ e) = (after p h).bind (after · e) := by induction h generalizing p with | nil => simp @@ -132,7 +132,7 @@ def outcome (p : WordQueryComp Unit Bool) (h : History) : Outcome := | some (.liftBind q _) => .ask q.2 /-- A program that is still in play after a one-step extension sent its message. -/ -theorem outcome_eq_ask_of_after_append_singleton {p : WordQueryComp Unit Bool} {h : History} +private theorem outcome_eq_ask_of_after_append_singleton {p : WordQueryComp Unit Bool} {h : History} {m y : List Bool} (hp : (after p (h ++ [(m, y)])).isSome) : outcome p h = .ask m := by rw [after_append] at hp unfold outcome @@ -155,14 +155,14 @@ noncomputable def acceptFrom (P : Prover Unit) (s : P.State) : @[simp] theorem acceptFrom_none (P : Prover Unit) (s : P.State) : acceptFrom P s none = 0 := rfl -theorem acceptFrom_pure (P : Prover Unit) (s : P.State) (b : Bool) : +private theorem acceptFrom_pure (P : Prover Unit) (s : P.State) (b : Bool) : acceptFrom P s (some (pure b)) = if b then 1 else 0 := by simp only [acceptFrom, OracleComp.interpret_pure, StateT.run_pure, Probability.PMF.monad_pure_eq_pure, PMF.pure_map, PMF.pure_apply] cases b <;> simp /-- A message is answered by the prover, and what remains continues from its new state. -/ -theorem acceptFrom_query_bind (P : Prover Unit) (s : P.State) (m : List Bool) +private theorem acceptFrom_query_bind (P : Prover Unit) (s : P.State) (m : List Bool) (next : List Bool → WordQueryComp Unit Bool) : acceptFrom P s (some (OracleComp.query ((), m) >>= next)) = ∑' ys : List Bool × P.State, (P.respond ((), m)).run s ys * acceptFrom P ys.2 @@ -220,7 +220,7 @@ theorem value_congr {h h' : History} simpa only [List.append_assoc, List.singleton_append] using hh r ((m, y) :: e) /-- Only the first `L` bits of a reply matter to the value. -/ -theorem value_take (hF : IsBounded F D L) (n : ℕ) (h : History) (m y : List Bool) : +private theorem value_take (hF : IsBounded F D L) (n : ℕ) (h : History) (m y : List Bool) : value F L n (h ++ [(m, y)]) = value F L n (h ++ [(m, y.take L)]) := value_congr (fun r e => by simpa only [List.append_assoc, List.singleton_append] using hF.reply r h m y e) n @@ -265,7 +265,7 @@ theorem value_le_card (n : ℕ) (h : History) : /-- One round of a prover against a program: if the program has finished, it accepts or not; if it sends a message of length at most `L`, the prover answers and what remains continues. -/ -theorem acceptFrom_after_eq (P : Prover Unit) (s : P.State) (p : WordQueryComp Unit Bool) +private theorem acceptFrom_after_eq (P : Prover Unit) (s : P.State) (p : WordQueryComp Unit Bool) (h : History) (hp : ∀ m, outcome p h = .ask m → m.length ≤ L) : acceptFrom P s (after p h) = (if outcome p h = .done true then 1 else 0) + ∑ m ∈ BitString.shortWords L, ∑' ys : List Bool × P.State, @@ -288,7 +288,8 @@ theorem acceptFrom_after_eq (P : Prover Unit) (s : P.State) (p : WordQueryComp U /-- **No prover beats the value**, from any history it is in and any of its states: the probabilities that `P` makes what remains of the programs accept sum to at most the value, when the programs have at most `n` rounds to go. -/ -theorem sum_acceptFrom_after_le (hF : IsBounded F D L) (P : Prover Unit) (n : ℕ) (h : History) +private theorem sum_acceptFrom_after_le (hF : IsBounded F D L) (P : Prover Unit) (n : ℕ) + (h : History) (hn : D ≤ h.length + n) (s : P.State) : ∑ r, acceptFrom P s (after (F r) h) ≤ value F L n h := by induction n generalizing h s with @@ -352,13 +353,13 @@ noncomputable def bestReply (n : ℕ) (h : History) (m : List Bool) : List Bool ((BitString.shortWords L).exists_max_image (fun y => value F L n (h ++ [(m, y)])) ⟨[], BitString.nil_mem_shortWords L⟩).choose -theorem bestReply_mem (n : ℕ) (h : History) (m : List Bool) : +private theorem bestReply_mem (n : ℕ) (h : History) (m : List Bool) : bestReply F L n h m ∈ BitString.shortWords L := ((BitString.shortWords L).exists_max_image (fun y => value F L n (h ++ [(m, y)])) ⟨[], BitString.nil_mem_shortWords L⟩).choose_spec.1 /-- The best reply attains the best value. -/ -theorem value_bestReply (n : ℕ) (h : History) (m : List Bool) : +private theorem value_bestReply (n : ℕ) (h : History) (m : List Bool) : value F L n (h ++ [(m, bestReply F L n h m)]) = (BitString.shortWords L).sup fun y => value F L n (h ++ [(m, y)]) := le_antisymm (Finset.le_sup (f := fun y => value F L n (h ++ [(m, y)])) @@ -379,7 +380,7 @@ noncomputable def optimalProver (D : ℕ) : Prover Unit where variable {F L} /-- **The optimal prover attains the value** from every history it is in. -/ -theorem sum_acceptFrom_optimalProver_after (hF : IsBounded F D L) (n : ℕ) (h : History) +private theorem sum_acceptFrom_optimalProver_after (hF : IsBounded F D L) (n : ℕ) (h : History) (hn : h.length + n = D) : ∑ r, acceptFrom (optimalProver F L D) h (after (F r) h) = value F L n h := by induction n generalizing h with diff --git a/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean b/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean index 887d49786..3bc71bb2c 100644 --- a/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean +++ b/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean @@ -97,7 +97,7 @@ zeros, a one, then `w`. -/ def encodeWord (L : ℕ) (w : List Bool) : List Bool := List.replicate (L - w.length) false ++ true :: w -theorem idxOf_true_replicate_false_append (n : ℕ) (w : List Bool) : +private theorem idxOf_true_replicate_false_append (n : ℕ) (w : List Bool) : (List.replicate n false ++ true :: w).idxOf true = n := by induction n with | zero => simp @@ -105,25 +105,26 @@ theorem idxOf_true_replicate_false_append (n : ℕ) (w : List Bool) : rw [List.replicate_succ, List.cons_append, List.idxOf_cons_ne _ (by simp), ih] /-- Decoding inverts coding. -/ -theorem decodeWord_encodeWord (L : ℕ) (w : List Bool) : decodeWord (encodeWord L w) = w := by +private theorem decodeWord_encodeWord (L : ℕ) (w : List Bool) : decodeWord + (encodeWord L w) = w := by rw [decodeWord, encodeWord, idxOf_true_replicate_false_append, List.drop_append] simp -theorem length_encodeWord {L : ℕ} {w : List Bool} (hw : w.length ≤ L) : +private theorem length_encodeWord {L : ℕ} {w : List Bool} (hw : w.length ≤ L) : (encodeWord L w).length = L + 1 := by simp only [encodeWord, List.length_append, List.length_replicate, List.length_cons] lia -theorem true_mem_encodeWord (L : ℕ) (w : List Bool) : true ∈ encodeWord L w := by +private theorem true_mem_encodeWord (L : ℕ) (w : List Bool) : true ∈ encodeWord L w := by simp [encodeWord] -theorem length_decodeWord_le {L : ℕ} {u : List Bool} (hu : u.length = L + 1) : +private theorem length_decodeWord_le {L : ℕ} {u : List Bool} (hu : u.length = L + 1) : (decodeWord u).length ≤ L := by simp only [decodeWord, List.length_drop] lia /-- A word with a `true` is its first `true` preceded by zeros and followed by its decoding. -/ -theorem eq_replicate_append_decodeWord : ∀ {u : List Bool}, true ∈ u → +private theorem eq_replicate_append_decodeWord : ∀ {u : List Bool}, true ∈ u → u = List.replicate (u.idxOf true) false ++ true :: decodeWord u | b :: u, h => by cases b @@ -136,7 +137,8 @@ theorem eq_replicate_append_decodeWord : ∀ {u : List Bool}, true ∈ u → · simp [decodeWord] /-- Coding inverts decoding on the words of length `L + 1` with a `true`. -/ -theorem encodeWord_decodeWord {L : ℕ} {u : List Bool} (hu : u.length = L + 1) (ht : true ∈ u) : +private theorem encodeWord_decodeWord {L : ℕ} {u : List Bool} (hu : u.length = L + 1) + (ht : true ∈ u) : encodeWord L (decodeWord u) = u := by have h := eq_replicate_append_decodeWord ht have hlen := congrArg List.length h @@ -155,7 +157,7 @@ def lastCode (u : List Bool) : Bool := decide (u = List.replicate (L + 1) true) /-- The number of codes, and of the words of length at most `L`. -/ def codeCount : ℕ := 2 ^ (L + 1) - 1 -theorem iterate_firstCode (i : ℕ) : +private theorem iterate_firstCode (i : ℕ) : increment^[i] (firstCode L) = increment^[i + 1] (List.replicate (L + 1) false) := by rw [Function.iterate_succ_apply] rfl @@ -163,14 +165,14 @@ theorem iterate_firstCode (i : ℕ) : variable {L} /-- The `i`-th code has value `i + 1` and length `L + 1`. -/ -theorem lsbValue_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : +private theorem lsbValue_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : lsbValue (increment^[i] (firstCode L)) = i + 1 ∧ (increment^[i] (firstCode L)).length = L + 1 := by rw [iterate_firstCode] exact BitString.iterate_increment (L + 1) (i + 1) (by simp only [codeCount] at hi; lia) /-- The last code is the `codeCount L`-th. -/ -theorem lastCode_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : +private theorem lastCode_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : lastCode L (increment^[i] (firstCode L)) = decide (i + 1 = codeCount L) := by obtain ⟨hv, hl⟩ := lsbValue_iterate_firstCode hi have hall := BitString.lsbValue_replicate_true (L + 1) @@ -185,7 +187,7 @@ theorem lastCode_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : simp only [codeCount] at h lia -theorem true_mem_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : +private theorem true_mem_iterate_firstCode {i : ℕ} (hi : i < codeCount L) : true ∈ increment^[i] (firstCode L) := by by_contra h have := BitString.lsbValue_eq_zero_of_true_not_mem h @@ -211,7 +213,7 @@ theorem image_decodeWord_iterate_firstCode : rw [iterate_firstCode, Nat.sub_add_cancel hpos, ← hlen, BitString.iterate_increment_lsbValue, decodeWord_encodeWord] -theorem injOn_decodeWord_iterate_firstCode : +private theorem injOn_decodeWord_iterate_firstCode : Set.InjOn (fun i => decodeWord (increment^[i] (firstCode L))) (range (codeCount L)) := by intro i hi j hj h simp only [coe_range, Set.mem_Iio] at hi hj @@ -275,7 +277,7 @@ section PolyTime open _root_.Turing _root_.Turing.MultiTapeTM ComputableTidilyInPolyTime /-- Decoding a word is polynomial-time. -/ -theorem computableTidilyInPolyTime_decodeWord : +private theorem computableTidilyInPolyTime_decodeWord : ComputableTidilyInPolyTime decodeWord encBits encBits := by have hidx : ComputableTidilyInPolyTime (fun u : List Bool => u.idxOf true + 1) encBits encUnary := by @@ -286,7 +288,7 @@ theorem computableTidilyInPolyTime_decodeWord : exact bitsDropWithInput id' hidx /-- Decoding a history is polynomial-time. -/ -theorem computableTidilyInPolyTime_decodeHistory : +private theorem computableTidilyInPolyTime_decodeHistory : ComputableTidilyInPolyTime decodeHistory (encList (encPair encBits encBits)) encHistory := by have hd := computableTidilyInPolyTime_decodeWord unfold decodeHistory @@ -318,7 +320,8 @@ def evaluate (a : α) : ℕ := ((evalStep enc M fuel)^[evalTime fuel a] (a, [], none)).2.2.getD 0 /-- The evaluation keeps its instance and runs the game-tree evaluator. -/ -theorem iterate_evalStep (a : α) (st : List (GameTree.Frame (List Bool)) × Option ℕ) (j : ℕ) : +private theorem iterate_evalStep (a : α) (st : List (GameTree.Frame (List Bool)) × Option ℕ) + (j : ℕ) : (evalStep enc M fuel)^[j] (a, st) = (a, (GameTree.step (fuel a) (2 ^ fuel a) (firstCode (fuel a)) increment (lastCode (fuel a)) (leafValue (coinFamily M (fuel a) (enc a))))^[j] st) := by @@ -342,7 +345,7 @@ theorem evaluate_eq (a : α) : rw [gameTree_value_eq _ (by simp), decodeHistory_nil] /-- Returning a value into the stack, with its explicit cases. -/ -def returnStep (L cap : ℕ) (st : List (GameTree.Frame (List Bool))) (v : ℕ) : +private def returnStep (L cap : ℕ) (st : List (GameTree.Frame (List Bool))) (v : ℕ) : List (GameTree.Frame (List Bool)) × Option ℕ := if st.isEmpty then (st, some v) else @@ -353,7 +356,7 @@ def returnStep (L cap : ℕ) (st : List (GameTree.Frame (List Bool))) (v : ℕ) else ((f.1, increment f.2.1, f.2.2.1, max f.2.2.2 v) :: st.tail, none) /-- A value returned into the stack, by `returnStep`. -/ -theorem step_some_eq (L cap : ℕ) (leaf : List (List Bool × List Bool) → ℕ) +private theorem step_some_eq (L cap : ℕ) (leaf : List (List Bool × List Bool) → ℕ) (st : List (GameTree.Frame (List Bool))) (v : ℕ) : GameTree.step L cap (firstCode L) increment (lastCode L) leaf (st, some v) = returnStep L cap st v := by @@ -373,7 +376,7 @@ theorem step_none_eq (L cap : ℕ) (leaf : List (List Bool × List Bool) → ℕ pushStep L st (min cap (leaf (GameTree.history st))) := rfl /-- One step of the evaluation, as a case distinction calling the leaf value once. -/ -theorem evalStep_eq (s : EvalState α) : evalStep enc M fuel s = +private theorem evalStep_eq (s : EvalState α) : evalStep enc M fuel s = if s.2.2.isSome then (s.1, returnStep (fuel s.1) (2 ^ fuel s.1) s.2.1 (s.2.2.getD 0)) else (s.1, pushStep (fuel s.1) s.2.1 (min (2 ^ fuel s.1) (leafValue (coinFamily M (fuel s.1) (enc s.1)) (GameTree.history s.2.1)))) := by @@ -433,7 +436,7 @@ variable {enc fuel} (hfuel : ComputableTidilyInPolyTime fuel enc encUnary) include hfuel /-- Returning a value into the stack is polynomial-time. -/ -theorem computableTidilyInPolyTime_returnStep : +private theorem computableTidilyInPolyTime_returnStep : ComputableTidilyInPolyTime (fun s : EvalState α => (s.1, returnStep (fuel s.1) (2 ^ fuel s.1) s.2.1 (s.2.2.getD 0))) (encEvalState enc) (encEvalState enc) := by @@ -443,7 +446,7 @@ theorem computableTidilyInPolyTime_returnStep : fun_prop /-- Pushing a frame is polynomial-time. -/ -theorem computableTidilyInPolyTime_pushStep : +private theorem computableTidilyInPolyTime_pushStep : ComputableTidilyInPolyTime (fun p : EvalState α × ℕ => (p.1.1, pushStep (fuel p.1.1) p.1.2.1 p.2)) (encPair (encEvalState enc) encNat) (encEvalState enc) := by @@ -453,7 +456,7 @@ theorem computableTidilyInPolyTime_pushStep : fun_prop /-- **The leaf value within polynomial space**: the count of accepting coins, capped. -/ -theorem computableTidilyInPolySpace_leaf [Finite Control] [Inhabited α] : +private theorem computableTidilyInPolySpace_leaf [Finite Control] [Inhabited α] : ComputableTidilyInPolySpace (fun s : EvalState α => min (2 ^ fuel s.1) (leafValue (coinFamily M (fuel s.1) (enc s.1)) (GameTree.history s.2.1))) (encEvalState enc) encNat := by @@ -474,7 +477,7 @@ theorem computableTidilyInPolySpace_leaf [Finite Control] [Inhabited α] : simp only [leafValue, countAccepts_eq_accepted] /-- **A step of the evaluation within polynomial space.** -/ -theorem computableTidilyInPolySpace_evalStep [Finite Control] [Inhabited α] : +private theorem computableTidilyInPolySpace_evalStep [Finite Control] [Inhabited α] : ComputableTidilyInPolySpace (evalStep enc M fuel) (encEvalState enc) (encEvalState enc) := by have hcond : ComputableTidilyInPolyTime (fun s : EvalState α => s.2.2.isSome) (encEvalState enc) encBool := by fun_prop diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF.lean index 4c62e845e..42001f4f6 100644 --- a/Complexity/Computability/Complexity/Classes/IP/TQBF.lean +++ b/Complexity/Computability/Complexity/Classes/IP/TQBF.lean @@ -78,18 +78,18 @@ variable {S : Type} noncomputable def verdict (I : LoopInput) (st : VState) (n : ℕ) : WordOracleComp Unit Bool := (fun st => st.2.2) <$> OracleComp.iterate n (Machine.step I) st -theorem verdict_succ (I : LoopInput) (st : VState) (n : ℕ) : +private theorem verdict_succ (I : LoopInput) (st : VState) (n : ℕ) : verdict I st (n + 1) = Machine.step I st >>= fun st' => verdict I st' n := by rw [verdict, OracleComp.iterate_succ_bind, map_bind] rfl /-- After a failed check the machine stays put and rejects. -/ -theorem verdict_of_ok_eq_false (I : LoopInput) {st : VState} (h : st.2.2 = false) (n : ℕ) : +private theorem verdict_of_ok_eq_false (I : LoopInput) {st : VState} (h : st.2.2 = false) (n : ℕ) : verdict I st n = pure false := by rw [verdict, OracleComp.iterate_eq_pure _ _ _ (by simp [Machine.step, h]), map_pure, h] /-- Without tokens the machine stays put and accepts when every check passed. -/ -theorem verdict_nil (I : LoopInput) (St : List Claim) (n : ℕ) : +private theorem verdict_nil (I : LoopInput) (St : List Claim) (n : ℕ) : verdict I ([], St, true) n = pure true := by rw [verdict, OracleComp.iterate_eq_pure _ _ _ (by simp [Machine.step]), map_pure] @@ -399,7 +399,7 @@ section Formula variable (ψ : QBF ℕ) /-- The variables of a formula are linearized by the machine. -/ -theorem mem_linVars {ψ : QBF ℕ} {v : ℕ} (hv : v ∈ ψ.vars) : v ∈ linVars ψ := by +private theorem mem_linVars {ψ : QBF ℕ} {v : ℕ} (hv : v ∈ ψ.vars) : v ∈ linVars ψ := by unfold linVars induction ψ with | var w => simp_all [QBF.vars, QBF.tokens] @@ -426,22 +426,22 @@ theorem mem_linVars {ψ : QBF ℕ} {v : ℕ} (hv : v ∈ ψ.vars) : v ∈ linVar /-- The arithmetic formula checked by the machine on `ψ`. -/ def arithOf : ArithQBF ℕ := ψ.arithmetize (linVars ψ) -theorem modOf_loopInput : modOf (loopInput ψ) = modulus ψ := +private theorem modOf_loopInput : modOf (loopInput ψ) = modulus ψ := Nat.sub_add_cancel (prime_modulus ψ).1.one_lt.le local instance : Fact (modOf (loopInput ψ)).Prime := ⟨modOf_loopInput ψ ▸ (prime_modulus ψ).1⟩ -theorem one_lt_modOf : 1 < modOf (loopInput ψ) := +private theorem one_lt_modOf : 1 < modOf (loopInput ψ) := (Fact.out (p := (modOf (loopInput ψ)).Prime)).one_lt -theorem vars_arithOf {w : ℕ} (hw : w ∈ (arithOf ψ).vars) : w ∈ (loopInput ψ).1.1 := +private theorem vars_arithOf {w : ℕ} (hw : w ∈ (arithOf ψ).vars) : w ∈ (loopInput ψ).1.1 := (QBF.mem_vars_arithmetize hw).elim mem_linVars id -theorem maxRoundDegree_arithOf : (arithOf ψ).maxRoundDegree ≤ (loopInput ψ).1.2.2 := by +private theorem maxRoundDegree_arithOf : (arithOf ψ).maxRoundDegree ≤ (loopInput ψ).1.2.2 := by refine (QBF.maxRoundDegree_arithmetize_le fun v hv => mem_linVars hv).trans (le_of_eq ?_) rw [loopInput, degreeBound, QBF.length_tokens] -theorem tokens_arithOf : (arithOf ψ).tokens = (loopInput ψ).2 := by +private theorem tokens_arithOf : (arithOf ψ).tokens = (loopInput ψ).2 := by rw [arithOf, QBF.tokens_arithmetize] rfl @@ -473,7 +473,7 @@ theorem acceptProb_verifier_eq (hψ : ψ.Closed) (P : Prover Unit) : rfl /-- The samples of the protocol give every residue probability at most `2 / p`. -/ -theorem eval_samplerOf_le (I : LoopInput) (z : ZMod (modOf I)) : +private theorem eval_samplerOf_le (I : LoopInput) (z : ZMod (modOf I)) : ProbComp.eval (samplerOf I) z ≤ 2 / modOf I := by rw [samplerOf, ProbComp.eval_map, PMF.map_apply, tsum_eq_single z.val] · split_ifs @@ -583,7 +583,7 @@ private theorem getD_decoded {p : ℕ} [NeZero p] (D : ℕ) (L : List (ZMod p)) variable (ψ : QBF ℕ) -theorem one_le_degree : 1 ≤ (loopInput ψ).1.2.2 := by +private theorem one_le_degree : 1 ≤ (loopInput ψ).1.2.2 := by have : 0 < ψ.tokens.length := List.length_pos_of_ne_nil (QBF.tokens_ne_nil ψ) simp only [loopInput, degreeBound] omega diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Protocol.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Protocol.lean index dac424909..342dca7b6 100644 --- a/Complexity/Computability/Complexity/Classes/IP/TQBF/Protocol.lean +++ b/Complexity/Computability/Complexity/Classes/IP/TQBF/Protocol.lean @@ -152,7 +152,7 @@ noncomputable def honest : Query V F → StateT Unit PMF (List F) := fun q s => PMF.pure (honestReply q, s) /-- Against the honest prover, the verifier accepts every true claim with certainty. -/ -theorem run_honest_verify (e : ArithQBF V) (r : V → F) (s : Unit) : +private theorem run_honest_verify (e : ArithQBF V) (r : V → F) (s : Unit) : runWith honest (verify sampler e r (e.eval r)) s = PMF.pure (true, s) := by induction e generalizing r with | var v => simp only [verify, ArithQBF.eval_var, decide_true, ProbOracleComp.runWith_pure] diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean index 2e856ceab..4b5126bc3 100644 --- a/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean +++ b/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean @@ -94,14 +94,14 @@ modulus less one, so that the modulus is positive, and the degree bound `D` of e abbrev Params := List ℕ × ℕ × ℕ /-- The encoding of the parameters, the numbers in unary. -/ -abbrev encParams : Params ↪ List Bool := +private abbrev encParams : Params ↪ List Bool := encPair (encList encNat) (encPair encUnary encUnary) /-- The input of the loop: the parameters and the tokens of the arithmetic formula. -/ abbrev LoopInput := Params × List (ArithQBF.Kind × ℕ) /-- The encoding of the input of the loop. -/ -noncomputable abbrev encLoopInput : LoopInput ↪ List Bool := +private noncomputable abbrev encLoopInput : LoopInput ↪ List Bool := encPair encParams (encList encArithToken) /-- A pending claim: a point and a value. -/ @@ -122,7 +122,7 @@ noncomputable abbrev encVState : VState ↪ List Bool := abbrev StepData := LoopInput × VState /-- The encoding of the data of a step. -/ -noncomputable abbrev encStepData : StepData ↪ List Bool := encPair encLoopInput encVState +private noncomputable abbrev encStepData : StepData ↪ List Bool := encPair encLoopInput encVState namespace StepData @@ -334,7 +334,7 @@ private lemma stepAt_pt (k : ArithQBF.Kind) : · exact ask_pt.bind_with (opCont_pt .lin) /-- **A step of the machine is strict oracle PPT** in the encoded input and state. -/ -theorem isOraclePPTOn_step : +private theorem isOraclePPTOn_step : IsOraclePPTOn encStepData encVState (fun a : StepData => step a.1 a.2) := by unfold step exact IsOraclePPTOn.cond (by fun_prop) @@ -482,7 +482,7 @@ private lemma growth_polyBounded : nlinarith /-- **The machine is strict oracle PPT** in its encoded input. -/ -theorem isOraclePPTOn_loop : IsOraclePPTOn encLoopInput encVState loop := by +private theorem isOraclePPTOn_loop : IsOraclePPTOn encLoopInput encVState loop := by unfold loop exact IsOraclePPTOn.iterateWith_of_bounded_growth (count := fun I => I.2.length) (by fun_prop) init_pt isOraclePPTOn_step growth_polyBounded diff --git a/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean b/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean index 88e8bcb54..f759157cf 100644 --- a/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean +++ b/Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean @@ -90,7 +90,7 @@ theorem computableTidilyInPolyTime_decodeCNF : /-! ### Capped powers -/ -theorem min_min_mul (a b c : ℕ) : min (min a c * b) c = min (a * b) c := by +private theorem min_min_mul (a b c : ℕ) : min (min a c * b) c = min (a * b) c := by rcases le_total a c with h | h · rw [min_eq_left h] · rw [min_eq_right h] @@ -99,7 +99,7 @@ theorem min_min_mul (a b c : ℕ) : min (min a c * b) c = min (a * b) c := by · rw [min_eq_right (Nat.le_mul_of_pos_right c hb), min_eq_right (h.trans (Nat.le_mul_of_pos_right a hb))] -theorem iterate_min_mul (b c e a : ℕ) : +private theorem iterate_min_mul (b c e a : ℕ) : (fun x => min (x * b) c)^[e] (min a c) = min (a * b ^ e) c := by induction e generalizing a with | zero => simp @@ -111,7 +111,7 @@ def capPow (b e c : ℕ) : ℕ := min (b ^ e) c /-- **Capped powers in unary.** `min (b ^ e) c` is polynomial-time on unary numbers: multiplying `e` times and capping at `c` never holds a number larger than the input. -/ -theorem computableTidilyInPolyTime_capPow_pair : +private theorem computableTidilyInPolyTime_capPow_pair : ComputableTidilyInPolyTime (fun p : ℕ × ℕ × ℕ => capPow p.1 p.2.1 p.2.2) (encPair encUnary (encPair encUnary encUnary)) encUnary := by have h := iterateWith (encIn := encPair encUnary (encPair encUnary encUnary)) @@ -194,7 +194,7 @@ theorem mem_padSAT_iff {e : ℕ → ℕ} {y : List Bool} : simp only [padCheck_eq_some_iff, padSAT, Set.mem_ofPred_eq] exact ⟨fun ⟨φ, hφ, h⟩ => ⟨φ, h, hφ⟩, fun ⟨φ, h, hφ⟩ => ⟨φ, hφ, h⟩⟩ -theorem computableTidilyInPolyTime_idxOf_false_reverse : +private theorem computableTidilyInPolyTime_idxOf_false_reverse : ComputableTidilyInPolyTime (fun y : List Bool => y.reverse.idxOf false) encBits encUnary := idxOfWithInput (encA := encBool) (list := fun y : List Bool => y.reverse) (value := fun _ => false) (bitsToList.comp bitsReverse) (const false) @@ -208,7 +208,7 @@ theorem computableTidilyInPolyTime_unpad : fun_prop /-- Reading the formula padded with a given exponent is polynomial-time. -/ -theorem computableTidilyInPolyTime_padCheckAt : +private theorem computableTidilyInPolyTime_padCheckAt : ComputableTidilyInPolyTime (fun p : List Bool × ℕ => padCheckAt p.1 p.2) (encPair encBits encUnary) (encOption encCNF) := by have henc : ComputableTidilyInPolyTime (fun φ => encCNF φ) encCNF encBits := encode encCNF @@ -300,7 +300,7 @@ def hstepB (T : List ℕ) : ℕ := (List.range T.length).all fun j => agreesB T i j).getD (Nat.log 2 (Nat.log 2 T.length)) /-- The least index below `m` passing a test, or `m`, as a search over `List.range m`. -/ -theorem find?_range_getD_eq_sInf (m : ℕ) (p : ℕ → Bool) : +private theorem find?_range_getD_eq_sInf (m : ℕ) (p : ℕ → Bool) : ((List.range m).find? p).getD m = sInf {i | i = m ∨ p i = true} := by set v := ((List.range m).find? p).getD m with hv have hmem : v ∈ {i | i = m ∨ p i = true} ∧ ∀ i < v, i ∉ {i | i = m ∨ p i = true} := by @@ -344,13 +344,13 @@ theorem computableTidilyInPolyTime_runIndexed {α : Type} {input : α ↪ List B unfold runIndexed fun_prop -theorem computableTidilyInPolyTime_memB : +private theorem computableTidilyInPolyTime_memB : ComputableTidilyInPolyTime (fun p : List ℕ × List Bool => memB p.1 p.2) (encPair (encList encUnary) encBits) encBool := by unfold memB fun_prop -theorem computableTidilyInPolyTime_agreesB : +private theorem computableTidilyInPolyTime_agreesB : ComputableTidilyInPolyTime (fun p : (List ℕ × ℕ) × ℕ => agreesB p.1.1 p.1.2 p.2) (encPair (encPair (encList encUnary) encUnary) encUnary) encBool := by have hm := computableTidilyInPolyTime_memB @@ -358,7 +358,7 @@ theorem computableTidilyInPolyTime_agreesB : fun_prop /-- The step of the exponent function is polynomial-time in its table. -/ -theorem computableTidilyInPolyTime_hstepB : +private theorem computableTidilyInPolyTime_hstepB : ComputableTidilyInPolyTime hstepB (encList encUnary) encUnary := by have ha := computableTidilyInPolyTime_agreesB have hall : ComputableTidilyInPolyTime @@ -407,7 +407,7 @@ assignment the certificate describes. -/ noncomputable def verifier (x : List Bool × List Bool) : Bool := (padCheck H x.1).elim false fun φ => SAT.verifier (φ, x.2) -theorem computableTidilyInPolyTime_verifier : +private theorem computableTidilyInPolyTime_verifier : ComputableTidilyInPolyTime verifier (encPair encBits encBits) encBool := by have hH : ComputableTidilyInPolyTime (fun p : (List Bool × List Bool) × ℕ => H p.2) (encPair (encPair encBits encBits) encUnary) encUnary := @@ -416,7 +416,7 @@ theorem computableTidilyInPolyTime_verifier : fun_prop /-- Padding a certificate with `false` does not change the assignment it describes. -/ -theorem assignment_append_replicate (φ : CNF ℕ) (w : List Bool) (k : ℕ) : +private theorem assignment_append_replicate (φ : CNF ℕ) (w : List Bool) (k : ℕ) : SAT.assignment φ (w ++ List.replicate k false) = SAT.assignment φ w := by funext v simp only [SAT.assignment, List.getD_eq_getElem?_getD, List.getElem?_append] diff --git a/Complexity/Computability/Complexity/Classes/Oracle/PP.lean b/Complexity/Computability/Complexity/Classes/Oracle/PP.lean index a5a8ceb5f..6d05d265e 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/PP.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/PP.lean @@ -219,7 +219,7 @@ private theorem interpret_searchQuery (u : List Bool) (s : ℕ × ℕ) : open Classical in /-- Against an oracle containing the code of `(u, k)` exactly when `k ≤ F`, a round of the search is `BinarySearch.step F`. -/ -theorem interpret_id_searchQuery {F : ℕ} {A : Set (List Bool)} {u : List Bool} +private theorem interpret_id_searchQuery {F : ℕ} {A : Set (List Bool)} {u : List Bool} (hA : ∀ k, encPair encBits encNat (u, k) ∈ A ↔ k ≤ F) (s : ℕ × ℕ) : OracleComp.interpret (m := Id) (languageOracle A) (searchQuery u s) = BinarySearch.step F s := by @@ -322,7 +322,8 @@ def bitQuery (r : Polynomial ℕ) (q : Unit × List Bool) : WordQueryComp Unit ( open Classical in /-- Against an oracle agreeing with `{(b, k) | k ≤ f b}` on codes, `bitQuery` answers bit `i` of `f b` to the code of `(b, i)`, when `f b ≤ 2 ^ r (|encβ b|)`. -/ -theorem interpret_id_bitQuery {β : Type} {encβ : β ↪ List Bool} {f : β → ℕ} {r : Polynomial ℕ} +private theorem interpret_id_bitQuery {β : Type} {encβ : β ↪ List Bool} {f : β → ℕ} + {r : Polynomial ℕ} (hr : ∀ b, f b ≤ 2 ^ r.eval (encβ b).length) {A : Set (List Bool)} (hA : ∀ x : β × ℕ, encPair encβ encNat x ∈ A ↔ x.2 ≤ f x.1) (b : β) (i : ℕ) : OracleComp.interpret (m := Id) (languageOracle A) (bitQuery r ((), encPair encβ encNat (b, i))) diff --git a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean index 40efc6664..4b62e7f2e 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean @@ -92,7 +92,7 @@ def PolyTimeReducible (encA : α ↪ List Bool) (encB : β ↪ List Bool) (X : P /-- Reductions of promise problems with a reduction computable tidily in polynomial time, the form in which proofs build reductions. -/ -theorem polyTimeReducible_iff_tidy : PolyTimeReducible encA encB X Y ↔ +private theorem polyTimeReducible_iff_tidy : PolyTimeReducible encA encB X Y ↔ ∃ f : α → β, ComputableTidilyInPolyTime f encA encB ∧ Set.MapsTo f X.yes Y.yes ∧ Set.MapsTo f X.no Y.no := by simp only [PolyTimeReducible, computableInPolyTime_iff_computableTidilyInPolyTime] @@ -120,7 +120,7 @@ theorem PolyTimeReducible.trans (hXY : PolyTimeReducible encA encB X Y) /-- A promise problem reduces, by the identity, to any problem with more yes-instances and more no-instances: enlarging the promise can only make a problem harder. -/ -theorem PolyTimeReducible.of_subset (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) : +private theorem PolyTimeReducible.of_subset (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) : PolyTimeReducible encB encB Y Y' := ⟨id, ComputableInPolyTime.id', fun _ h => hyes h, fun _ h => hno h⟩ diff --git a/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean b/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean index 48d21f06c..7c4b42cf4 100644 --- a/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean +++ b/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean @@ -143,16 +143,16 @@ theorem computableTidilyInPolyTime_hashCNF : /-- The selector ranges over the dyadic range of `φ.vars.length + 2`: the least power of two above it. -/ -theorem two_pow_hashBits (φ : CNF ℕ) : +private theorem two_pow_hashBits (φ : CNF ℕ) : 2 ^ hashBits φ = Probability.dyadicSize (φ.vars.length + 2) := rfl /-- `2 ^ hashBits φ` is at most twice `φ.vars.length + 3`. -/ -theorem two_pow_hashBits_le (φ : CNF ℕ) : 2 ^ hashBits φ ≤ 2 * (φ.vars.length + 3) := +private theorem two_pow_hashBits_le (φ : CNF ℕ) : 2 ^ hashBits φ ≤ 2 * (φ.vars.length + 3) := (two_pow_hashBits φ).trans_le (Probability.dyadicSize_le _) /-- Every number of equations up to `φ.vars.length + 2` can be selected. -/ -theorem lt_two_pow_hashBits (φ : CNF ℕ) : φ.vars.length + 2 < 2 ^ hashBits φ := +private theorem lt_two_pow_hashBits (φ : CNF ℕ) : φ.vars.length + 2 < 2 ^ hashBits φ := (two_pow_hashBits φ).symm ▸ Probability.lt_dyadicSize _ private theorem binaryValue_take_hashBits (φ : CNF ℕ) (r : List Bool) : @@ -191,7 +191,7 @@ theorem eval_stepClauses (σ : Var → Bool) (bit : Bool) (next prev x : Var) : /-- The clauses of one equation hold exactly when the auxiliary variables start at the offset, follow the steps, and end at `false`. -/ -theorem eval_rowClauses (σ : Var → Bool) (vars : List ℕ) (i : ℕ) (row : List Bool) +private theorem eval_rowClauses (σ : Var → Bool) (vars : List ℕ) (i : ℕ) (row : List Bool) (offset : Bool) : (rowClauses vars i row offset).eval σ = true ↔ σ (.inr (i, 0)) = offset ∧ σ (.inr (i, vars.length)) = false ∧ @@ -206,7 +206,7 @@ theorem eval_rowClauses (σ : Var → Bool) (vars : List ℕ) (i : ℕ) (row : L exact h j hj /-- The `i`-th row read by `hashCNF`, for `i < k`, is the `i`-th block of the padded word. -/ -theorem mem_zipIdx_listRows {k width : ℕ} {w row : List Bool} {i : ℕ} : +private theorem mem_zipIdx_listRows {k width : ℕ} {w row : List Bool} {i : ℕ} : (row, i) ∈ (BitString.listRows k width w).zipIdx ↔ ∃ hi : i < k, row = List.ofFn (BitString.block (BitString.ofList (k * width) w) ⟨i, hi⟩) := by @@ -230,7 +230,7 @@ def offset (k width : ℕ) (w : List Bool) : BitString k := /-- The equations hold exactly when, for each `i < k`, the auxiliary variables of the `i`-th equation start at its offset, follow its coefficients, and end at `false`. -/ -theorem eval_hashCNF (σ : Var → Bool) (vars : List ℕ) (k : ℕ) (w : List Bool) : +private theorem eval_hashCNF (σ : Var → Bool) (vars : List ℕ) (k : ℕ) (w : List Bool) : (hashCNF vars k w).eval σ = true ↔ ∀ i : Fin k, σ (.inr (i, 0)) = offset k vars.length w i ∧ σ (.inr (i, vars.length)) = false ∧ ∀ (j : ℕ) (hj : j < vars.length), σ (.inr (i, j + 1)) = @@ -254,7 +254,7 @@ theorem eval_hashCNF (σ : Var → Bool) (vars : List ℕ) (k : ℕ) (w : List B /-- A sequence that starts at `c` and adds `f j` at each step `j < n` holds `c + ∑ j' < j, f j'` up to step `n`. -/ -theorem eq_add_sum_of_step {z f : ℕ → Bool} {c : Bool} {n : ℕ} (h0 : z 0 = c) +private theorem eq_add_sum_of_step {z f : ℕ → Bool} {c : Bool} {n : ℕ} (h0 : z 0 = c) (hstep : ∀ j < n, z (j + 1) = (z j ^^ f j)) : ∀ j ≤ n, z j = c + ∑ j' ∈ Finset.range j, f j' := by intro j hj @@ -277,7 +277,7 @@ def auxValue (vars : List ℕ) (k : ℕ) (w : List Bool) (σ : ℕ → Bool) (i if h : j' < vars.length then matrix k vars.length w i ⟨j', h⟩ && σ vars[j'] else false /-- After all terms, the auxiliary value is the `i`-th coordinate of the hash. -/ -theorem auxValue_length (vars : List ℕ) (k : ℕ) (w : List Bool) (σ : ℕ → Bool) +private theorem auxValue_length (vars : List ℕ) (k : ℕ) (w : List Bool) (σ : ℕ → Bool) (i : Fin k) : auxValue vars k w σ i vars.length = affineHash (matrix k vars.length w, offset k vars.length w) (point vars σ) i := by @@ -287,7 +287,7 @@ theorem auxValue_length (vars : List ℕ) (k : ℕ) (w : List Bool) (σ : ℕ /-- In a satisfying assignment of the equations, the auxiliary variables hold the forced values. -/ -theorem eq_auxValue_of_eval {σ : Var → Bool} {vars : List ℕ} {k : ℕ} {w : List Bool} +private theorem eq_auxValue_of_eval {σ : Var → Bool} {vars : List ℕ} {k : ℕ} {w : List Bool} (h : (hashCNF vars k w).eval σ = true) (i : Fin k) {j : ℕ} (hj : j ≤ vars.length) : σ (.inr (i, j)) = auxValue vars k w (σ ∘ .inl) i j := by obtain ⟨h0, -, hs⟩ := (eval_hashCNF σ vars k w).1 h i @@ -295,7 +295,7 @@ theorem eq_auxValue_of_eval {σ : Var → Bool} {vars : List ℕ} {k : ℕ} {w : simp only [hs j hj, hj, dite_true, Function.comp_apply] /-- A satisfying assignment of the equations hashes its point to zero. -/ -theorem hash_point_eq_zero_of_eval {σ : Var → Bool} {vars : List ℕ} {k : ℕ} {w : List Bool} +private theorem hash_point_eq_zero_of_eval {σ : Var → Bool} {vars : List ℕ} {k : ℕ} {w : List Bool} (h : (hashCNF vars k w).eval σ = true) : affineHash (matrix k vars.length w, offset k vars.length w) (point vars (σ ∘ .inl)) = 0 := by funext i @@ -304,7 +304,7 @@ theorem hash_point_eq_zero_of_eval {σ : Var → Bool} {vars : List ℕ} {k : /-- An assignment of the original variables whose point hashes to zero extends, by the forced auxiliary values, to a satisfying assignment of the equations. -/ -theorem eval_hashCNF_extend {vars : List ℕ} {k : ℕ} {w : List Bool} {σ : ℕ → Bool} +private theorem eval_hashCNF_extend {vars : List ℕ} {k : ℕ} {w : List Bool} {σ : ℕ → Bool} (h : affineHash (matrix k vars.length w, offset k vars.length w) (point vars σ) = 0) : (hashCNF vars k w).eval (Sum.elim σ fun p => if hp : p.1 < k then auxValue vars k w σ ⟨p.1, hp⟩ p.2 else false) = true := by @@ -321,7 +321,7 @@ theorem eval_hashCNF_extend {vars : List ℕ} {k : ℕ} {w : List Bool} {σ : /-! ### Variables of the reduced formula -/ /-- The clauses of a step only mention its three variables. -/ -theorem mem_vars_stepClauses {bit : Bool} {next prev x u : Var} +private theorem mem_vars_stepClauses {bit : Bool} {next prev x u : Var} (h : u ∈ (stepClauses bit next prev x).vars) : u = next ∨ u = prev ∨ u = x := by cases bit <;> simp only [stepClauses, CNF.vars, Bool.false_eq_true, ite_false, ite_true, List.flatten_cons, List.flatten_nil, List.map_append, List.map_cons, List.map_nil, @@ -329,7 +329,7 @@ theorem mem_vars_stepClauses {bit : Bool} {next prev x u : Var} /-- Every variable of the `i`-th equation is an original variable among `vars`, or an auxiliary variable `inr (i, j)` with `j ≤ vars.length`. -/ -theorem mem_vars_rowClauses {vars : List ℕ} {i : ℕ} {row : List Bool} {c : Bool} {u : Var} +private theorem mem_vars_rowClauses {vars : List ℕ} {i : ℕ} {row : List Bool} {c : Bool} {u : Var} (h : u ∈ (rowClauses vars i row c).vars) : (∃ v ∈ vars, u = .inl v) ∨ ∃ j ≤ vars.length, u = .inr (i, j) := by simp only [rowClauses, CNF.mem_vars, List.mem_cons, List.mem_flatMap] at h @@ -348,7 +348,7 @@ theorem mem_vars_rowClauses {vars : List ℕ} {i : ℕ} {row : List Bool} {c : B /-- Every variable of the equations is an original variable among `vars`, or an auxiliary variable `inr (i, j)` with `i < k` and `j ≤ vars.length`. -/ -theorem mem_vars_hashCNF {vars : List ℕ} {k : ℕ} {w : List Bool} {u : Var} +private theorem mem_vars_hashCNF {vars : List ℕ} {k : ℕ} {w : List Bool} {u : Var} (h : u ∈ (hashCNF vars k w).vars) : (∃ v ∈ vars, u = .inl v) ∨ ∃ i < k, ∃ j ≤ vars.length, u = .inr (i, j) := by simp only [hashCNF, CNF.mem_vars, List.mem_flatMap] at h @@ -362,7 +362,7 @@ theorem mem_vars_hashCNF {vars : List ℕ} {k : ℕ} {w : List Bool} {u : Var} /-- **Soundness.** A satisfying assignment of the reduced formula restricts to one of `φ`: the equations only add constraints. -/ -theorem satisfiable_of_satisfiable_reduceWith {φ : CNF ℕ} {k : ℕ} {w : List Bool} +private theorem satisfiable_of_satisfiable_reduceWith {φ : CNF ℕ} {k : ℕ} {w : List Bool} (h : (reduceWith φ k w).Satisfiable) : φ.Satisfiable := by obtain ⟨τ, hτ⟩ := h simp only [reduceWith, CNF.eval_relabel, CNF.eval_append, Bool.and_eq_true] at hτ @@ -379,7 +379,7 @@ open Classical in noncomputable def solutions (φ : CNF ℕ) : Finset (BitString φ.vars.length) := Finset.univ.filter fun x => ∃ σ : ℕ → Bool, φ.eval σ = true ∧ point φ.vars σ = x -theorem mem_solutions {φ : CNF ℕ} {x : BitString φ.vars.length} : +private theorem mem_solutions {φ : CNF ℕ} {x : BitString φ.vars.length} : x ∈ solutions φ ↔ ∃ σ : ℕ → Bool, φ.eval σ = true ∧ point φ.vars σ = x := by simp [solutions] @@ -452,28 +452,29 @@ theorem reduceWith_mem_USAT {φ : CNF ℕ} {k : ℕ} {w : List Bool} /-- The number of equations isolating a solution with probability at least `3 / 16`: with `s` solutions, `2 ^ (log₂ s + 2)` lies between `2 s` and `4 s`. -/ -noncomputable def goodRows (φ : CNF ℕ) : ℕ := Nat.log 2 (solutions φ).card + 2 +private noncomputable def goodRows (φ : CNF ℕ) : ℕ := Nat.log 2 (solutions φ).card + 2 /-- A satisfiable formula has a solution. -/ -theorem solutions_nonempty {φ : CNF ℕ} (hφ : φ.Satisfiable) : (solutions φ).Nonempty := +private theorem solutions_nonempty {φ : CNF ℕ} (hφ : φ.Satisfiable) : (solutions φ).Nonempty := let ⟨σ, hσ⟩ := hφ ⟨_, mem_solutions.2 ⟨σ, hσ, rfl⟩⟩ /-- `2 ^ goodRows φ` is at most four times the number of solutions. -/ -theorem two_pow_goodRows_le {φ : CNF ℕ} (hφ : φ.Satisfiable) : +private theorem two_pow_goodRows_le {φ : CNF ℕ} (hφ : φ.Satisfiable) : 2 ^ goodRows φ ≤ 4 * (solutions φ).card := by have := Nat.pow_log_le_self 2 (solutions_nonempty hφ).card_pos.ne' rw [goodRows, pow_add] omega /-- `2 ^ goodRows φ` is at least twice the number of solutions. -/ -theorem two_mul_card_solutions_le (φ : CNF ℕ) : 2 * (solutions φ).card ≤ 2 ^ goodRows φ := by +private theorem two_mul_card_solutions_le (φ : CNF ℕ) : 2 * + (solutions φ).card ≤ 2 ^ goodRows φ := by have := Nat.lt_pow_succ_log_self (b := 2) (by decide) (solutions φ).card rw [goodRows, pow_add, pow_succ] at * omega /-- At most `2 ^ φ.vars.length` solutions need at most `φ.vars.length + 2` equations. -/ -theorem goodRows_le (φ : CNF ℕ) : goodRows φ ≤ φ.vars.length + 2 := by +private theorem goodRows_le (φ : CNF ℕ) : goodRows φ ≤ φ.vars.length + 2 := by have hcard : (solutions φ).card ≤ 2 ^ φ.vars.length := (Finset.card_le_univ _).trans_eq (by simp) have := Nat.log_mono_right (b := 2) hcard @@ -482,13 +483,13 @@ theorem goodRows_le (φ : CNF ℕ) : goodRows φ ≤ φ.vars.length + 2 := by omega /-- The selector bits can select `goodRows φ` equations. -/ -theorem goodRows_lt_two_pow_hashBits (φ : CNF ℕ) : goodRows φ < 2 ^ hashBits φ := +private theorem goodRows_lt_two_pow_hashBits (φ : CNF ℕ) : goodRows φ < 2 ^ hashBits φ := (goodRows_le φ).trans_lt (lt_two_pow_hashBits φ) open Classical in /-- **The Valiant–Vazirani lemma for the formula**: with `goodRows φ` random equations, exactly one solution of a satisfiable `φ` satisfies them with probability at least `3 / 16`. -/ -theorem three_sixteenths_le_dens {φ : CNF ℕ} (hφ : φ.Satisfiable) : +private theorem three_sixteenths_le_dens {φ : CNF ℕ} (hφ : φ.Satisfiable) : 3 / 16 ≤ Finset.dens (Finset.univ.filter fun p : (Fin (goodRows φ) → BitString φ.vars.length) × BitString (goodRows φ) => Isolates φ p) := by @@ -502,7 +503,7 @@ theorem three_sixteenths_le_dens {φ : CNF ℕ} (hφ : φ.Satisfiable) : open Classical in /-- The density bound in integers: at least `3 / 16` of the `2 ^ (k * n + k)` seeds isolate a solution. -/ -theorem three_mul_two_pow_le_card_isolates {φ : CNF ℕ} (hφ : φ.Satisfiable) : +private theorem three_mul_two_pow_le_card_isolates {φ : CNF ℕ} (hφ : φ.Satisfiable) : 3 * 2 ^ (goodRows φ * φ.vars.length + goodRows φ) ≤ 16 * (Finset.univ.filter fun p : (Fin (goodRows φ) → BitString φ.vars.length) × BitString (goodRows φ) => @@ -551,13 +552,13 @@ theorem offset_take (k width : ℕ) (w : List Bool) : rw [ite_eq_left (by omega)] /-- The coefficients of a word of exactly `k * width + k` bits are its first blocks. -/ -theorem matrix_ofFn_append {k width : ℕ} (a : BitString (k * width)) (b : BitString k) : +private theorem matrix_ofFn_append {k width : ℕ} (a : BitString (k * width)) (b : BitString k) : matrix k width (List.ofFn (Fin.append a b)) = BitString.blocksEquiv a := by rw [matrix, List.ofFn_fin_append, BitString.ofList_ofFn_append] rfl /-- The offsets of a word of exactly `k * width + k` bits are its last `k` bits. -/ -theorem offset_ofFn_append {k width : ℕ} (a : BitString (k * width)) (b : BitString k) : +private theorem offset_ofFn_append {k width : ℕ} (a : BitString (k * width)) (b : BitString k) : offset k width (List.ofFn (Fin.append a b)) = b := by rw [offset, List.ofFn_fin_append, List.drop_left' (by simp), BitString.ofList_ofFn] @@ -583,7 +584,7 @@ open Classical in /-- The random words of length `m` for which the reduction outputs a uniquely satisfiable formula are at least `3 / (16 * 2 ^ hashBits φ)` of all words, once `m` covers the selector bits and the coefficients and offsets of `goodRows φ` equations. -/ -theorem three_mul_two_pow_le_card {φ : CNF ℕ} (hφ : φ.Satisfiable) {m : ℕ} +private theorem three_mul_two_pow_le_card {φ : CNF ℕ} (hφ : φ.Satisfiable) {m : ℕ} (hm : hashBits φ + (goodRows φ * φ.vars.length + goodRows φ) ≤ m) : 3 * 2 ^ m ≤ 16 * 2 ^ hashBits φ * (Finset.univ.filter fun r : Fin m → Bool => reduce (φ, List.ofFn r) ∈ USAT).card := by @@ -638,7 +639,7 @@ coefficients and offsets of up to `φ.vars.length + 2` equations of `φ.vars.len def randomBits (φ : CNF ℕ) : ℕ := hashBits φ + (φ.vars.length + 2) * (φ.vars.length + 1) /-- The selector reads at most `φ.vars.length + 2` bits. -/ -theorem hashBits_le (φ : CNF ℕ) : hashBits φ ≤ φ.vars.length + 2 := +private theorem hashBits_le (φ : CNF ℕ) : hashBits φ ≤ φ.vars.length + 2 := Nat.succ_le_of_lt (Nat.log_lt_self 2 (by omega)) /-- The reduction reads at most `(φ.vars.length + 2) ^ 2` random bits. -/ diff --git a/Complexity/Computability/Complexity/Fagin/Power.lean b/Complexity/Computability/Complexity/Fagin/Power.lean index a5d160bbe..395849309 100644 --- a/Complexity/Computability/Complexity/Fagin/Power.lean +++ b/Complexity/Computability/Complexity/Fagin/Power.lean @@ -113,11 +113,11 @@ def powerStructure (a : EncodedStructure) (B : ℕ) : v.powerLanguage.Structure (x 0 : ℕ) < a.1 ^ v.arity i ∧ (v.table a (v.symbol i)).getD (x 0 : ℕ) false = true | 2, () => x 0 < x 1 -theorem relMap_powerLt (a : EncodedStructure) (B : ℕ) (x : Fin 2 → Fin B) : +private theorem relMap_powerLt (a : EncodedStructure) (B : ℕ) (x : Fin 2 → Fin B) : (v.powerStructure a B).RelMap v.powerLt x ↔ x 0 < x 1 := Iff.rfl -theorem relMap_powerIsElem (a : EncodedStructure) (B : ℕ) (x : Fin 1 → Fin B) : +private theorem relMap_powerIsElem (a : EncodedStructure) (B : ℕ) (x : Fin 1 → Fin B) : (v.powerStructure a B).RelMap v.powerIsElem x ↔ (x 0 : ℕ) < a.1 := Iff.rfl @@ -126,7 +126,7 @@ theorem relMap_powerInTable (a : EncodedStructure) (B : ℕ) (i : Fin v.count) (v.powerStructure a B).RelMap (v.powerInTable i) x ↔ (x 0 : ℕ) < a.1 ^ v.arity i := Iff.rfl -theorem relMap_powerTableBit (a : EncodedStructure) (B : ℕ) (i : Fin v.count) +private theorem relMap_powerTableBit (a : EncodedStructure) (B : ℕ) (i : Fin v.count) (x : Fin 1 → Fin B) : (v.powerStructure a B).RelMap (v.powerTableBit i) x ↔ (x 0 : ℕ) < a.1 ^ v.arity i ∧ (v.table a (v.symbol i)).getD (x 0 : ℕ) false = true := @@ -149,7 +149,7 @@ element of the linear order. -/ def isMinVarFormula {α : Type*} (p : α) : (L.sum ESO.orderLanguage).Formula α := ∀' ∼(ltRel.boundedFormula₂ &0 (.var (.inl p))) -theorem relMap_ltRel {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) +private theorem relMap_ltRel {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (x : Fin 2 → M) : @RelMap (L.sum ESO.orderLanguage) M (@sumStructure _ _ M _ @@ -157,14 +157,15 @@ theorem relMap_ltRel {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) ltRel x ↔ e (x 0) < e (x 1) := Iff.rfl -theorem realize_ltVarFormula {α : Type*} {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) +private theorem realize_ltVarFormula {α : Type*} {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (val : α → M) (p q : α) : (letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2) (ESO.orderRelOfEquiv e); (ltVarFormula (L := L) p q).Realize val) ↔ e (val p) < e (val q) := by let _ := ESO.varLanguage.structure (arity := fun _ : Unit => 2) (ESO.orderRelOfEquiv e) simp [ltVarFormula, Formula.Realize, relMap_ltRel] -theorem realize_isMinVarFormula {α : Type*} {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) +private theorem realize_isMinVarFormula {α : Type*} {M : Type} [L.Structure M] {n : ℕ} + (e : M ≃ Fin n) (val : α → M) (p : α) : (letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2) (ESO.orderRelOfEquiv e); (isMinVarFormula (L := L) p).Realize val) ↔ (e (val p) : ℕ) = 0 := by @@ -213,7 +214,7 @@ noncomputable def powerInterpretation : | 1, .inr (.inr idx) => v.powerTableBitFormula k har idx | 2, () => powerLtFormula k -theorem realize_highZeroFormula {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) +private theorem realize_highZeroFormula {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (a : ℕ) (ha : a ≤ k) (x : Fin k → M) : (letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2) (ESO.orderRelOfEquiv e); (highZeroFormula (L := L) k a).Realize (fun p : Fin 1 × Fin k => x p.2)) ↔ @@ -222,7 +223,7 @@ theorem realize_highZeroFormula {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ simp only [highZeroFormula, Formula.realize_iInf, realize_isMinVarFormula e, Subtype.forall] exact (tupleIndex_lt_pow_iff ha (e ∘ x)).symm -theorem realize_powerLtFormula {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) +private theorem realize_powerLtFormula {M : Type} [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (x y : Fin k → M) : (letI := ESO.varLanguage.structure (arity := fun _ : Unit => 2) (ESO.orderRelOfEquiv e); (powerLtFormula (L := L) k).Realize diff --git a/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean b/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean index 2cd8c71bc..ace11d4fc 100644 --- a/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean +++ b/Complexity/Computability/Complexity/Fagin/StrictVerifier.lean @@ -74,7 +74,7 @@ theorem strictVerifier_eq_true_iff (enc : α ↪ List Bool) (p : Polynomial ℕ) w.length = p.eval (enc a).length ∧ V (a, w) = true := by simp [strictVerifier] -theorem length_eq_of_strictVerifier_eq_true {enc : α ↪ List Bool} {p : Polynomial ℕ} +private theorem length_eq_of_strictVerifier_eq_true {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {w : List Bool} (h : strictVerifier enc p V (a, w) = true) : w.length = p.eval (enc a).length := diff --git a/Complexity/Computability/Complexity/Problems/CircuitValue.lean b/Complexity/Computability/Complexity/Problems/CircuitValue.lean index b2c12da3b..e2b8ef751 100644 --- a/Complexity/Computability/Complexity/Problems/CircuitValue.lean +++ b/Complexity/Computability/Complexity/Problems/CircuitValue.lean @@ -78,7 +78,7 @@ namespace CircuitValue /-- The output of a circuit is the output of its code: the output wire is the only entry of the list of output wires. -/ -theorem eval_eq_evalOutput (x : Σ n, Circuit signature n 1 × BitString n) : +private theorem eval_eq_evalOutput (x : Σ n, Circuit signature n 1 × BitString n) : x.2.1.eval interpretation x.2.2 0 = evalOutput (List.ofFn x.2.2) x.2.1.code.1 (x.2.1.code.2.headD 0) := by rw [Circuit.eval_eq_evalOutput] diff --git a/Complexity/Computability/Complexity/Problems/Hamiltonian/Directed.lean b/Complexity/Computability/Complexity/Problems/Hamiltonian/Directed.lean index 13921d6d6..83ce0ca00 100644 --- a/Complexity/Computability/Complexity/Problems/Hamiltonian/Directed.lean +++ b/Complexity/Computability/Complexity/Problems/Hamiltonian/Directed.lean @@ -123,7 +123,7 @@ private theorem mem_diamondDetours {φ : CNF ℕ} {d : Diamond.Detour} : exact ⟨(φ[j], j), List.mem_zipIdx_iff_getElem?.2 (by simp [hj]), l, hl, rfl⟩ /-- The diamond graph is well formed: the detours across slot `j` all belong to clause `j`. -/ -theorem wellFormed_diamondDetours (φ : CNF ℕ) : +private theorem wellFormed_diamondDetours (φ : CNF ℕ) : Diamond.WellFormed φ.vars.length (fun _ => φ.length) φ.length (diamondDetours φ) where clause_lt d hd := by obtain ⟨j, hj, l, hl, rfl⟩ := mem_diamondDetours.1 hd @@ -182,7 +182,7 @@ namespace SAT /-! ### Polynomial-time reductions -/ /-- The detours of the diamond graph are computable in polynomial time. -/ -theorem computableTidilyInPolyTime_diamondDetours : +private theorem computableTidilyInPolyTime_diamondDetours : ComputableTidilyInPolyTime diamondDetours encCNF (encList Diamond.encDetour) := by have hvars := computableTidilyInPolyTime_vars unfold diamondDetours diff --git a/Complexity/Computability/Complexity/ProofSystem.lean b/Complexity/Computability/Complexity/ProofSystem.lean index 6f1628eab..e5f789fd1 100644 --- a/Complexity/Computability/Complexity/ProofSystem.lean +++ b/Complexity/Computability/Complexity/ProofSystem.lean @@ -100,7 +100,7 @@ namespace ProofSystem instance : CoeFun (ProofSystem enc L) fun _ => List Bool → α := ⟨toFun⟩ /-- **Soundness**: every word proves a member of `L`. -/ -theorem mem (P : ProofSystem enc L) (π : List Bool) : P π ∈ L := +private theorem mem (P : ProofSystem enc L) (π : List Bool) : P π ∈ L := P.range_eq.subset ⟨π, rfl⟩ /-- **Completeness**: every member of `L` has a proof. -/ @@ -268,7 +268,7 @@ theorem ofVerifier_frame_append (D : Decoder enc) /-- The proof system of a verifier is polynomially bounded: an instance `a` has a proof of length `2 * (enc a).length + 1 + p (enc a).length`. -/ -theorem polynomiallyBounded_ofVerifier (D : Decoder enc) +private theorem polynomiallyBounded_ofVerifier (D : Decoder enc) (hV : ComputableInPolyTime V (encPair enc encBits) encBool) (hVL : IsVerifier enc p V L) {a₀ : α} (ha₀ : a₀ ∈ L) : (ofVerifier D hV hVL ha₀).PolynomiallyBounded := by diff --git a/Complexity/Computability/PCP/Approximation/Hastad/LinearTest.lean b/Complexity/Computability/PCP/Approximation/Hastad/LinearTest.lean index ce330cb3c..d98f9324f 100644 --- a/Complexity/Computability/PCP/Approximation/Hastad/LinearTest.lean +++ b/Complexity/Computability/PCP/Approximation/Hastad/LinearTest.lean @@ -206,7 +206,7 @@ theorem sum_spectralWeight_le_one (k : ℕ) (A : (α → Bool) → Bool) : /-- Low-degree terms in the Cauchy–Schwarz bound are controlled by the collision probability of the spectral decoding distributions along `π`. -/ -theorem sum_lowDegree_fourierCoeff_sq_le (π : β → γ) (k : ℕ) +private theorem sum_lowDegree_fourierCoeff_sq_le (π : β → γ) (k : ℕ) (B : (γ → Bool) → Bool) (A : (β → Bool) → Bool) : (∑ T ∈ univ.filter (fun T : Finset β => #T < k ∧ projectSet π T ≠ ∅), fourierCoeff (fun g => signVal (A g)) T ^ 2 * diff --git a/Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean b/Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean index 90f28abbc..f8e278899 100644 --- a/Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean +++ b/Complexity/Computability/QueryComplexity/Sensitivity/Hypercube.lean @@ -63,7 +63,8 @@ open Finset Function Module variable {ι : Type*} /-- Flipping a bit of `T` negates the character of `T`. -/ -theorem chi_update_not_of_mem {R : Type*} [CommRing R] [DecidableEq ι] {T : Finset ι} {i : ι} +private theorem chi_update_not_of_mem {R : Type*} [CommRing R] [DecidableEq ι] {T : Finset ι} + {i : ι} (hi : i ∈ T) (x : ι → Bool) : chi R T (update x i (!x i)) = -chi R T x := by have h := chi_update_of_mem (R := R) hi x (x i) rw [update_eq_self] at h @@ -152,7 +153,7 @@ theorem signedAdjacency_signedAdjacency (S : Finset ι) (v : (ι → Bool) → /-- The eigenspaces of the signed adjacency operator along a nonempty `S` for `√|S|` and `-√|S|` together span all functions on the cube: `v` is `1 / (2√|S|)` times the difference of `(A + √|S|) v` and `(A - √|S|) v`. -/ -theorem eigenspace_sup_eigenspace_signedAdjacency {S : Finset ι} (hS : S.Nonempty) : +private theorem eigenspace_sup_eigenspace_signedAdjacency {S : Finset ι} (hS : S.Nonempty) : (signedAdjacency S).eigenspace √(#S : ℝ) ⊔ (signedAdjacency S).eigenspace (-√(#S : ℝ)) = ⊤ := by set A := signedAdjacency S set c : ℝ := √(#S : ℝ) @@ -177,7 +178,7 @@ variable [Fintype ι] /-- One of the eigenspaces of the signed adjacency operator along a nonempty `S` for `±√|S|` has dimension at least half the number of points of the cube. -/ -theorem exists_abs_eq_sqrt_two_pow_le_two_mul_finrank {S : Finset ι} (hS : S.Nonempty) : +private theorem exists_abs_eq_sqrt_two_pow_le_two_mul_finrank {S : Finset ι} (hS : S.Nonempty) : ∃ μ : ℝ, |μ| = √(#S : ℝ) ∧ 2 ^ Fintype.card ι ≤ 2 * finrank ℝ ((signedAdjacency S).eigenspace μ) := by have h := Submodule.finrank_add_le_finrank_add_finrank diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Weight.lean b/Complexity/Computability/TreeEval/Reader/Cert/Weight.lean index 38c5cdfd5..9e9d8c2f3 100644 --- a/Complexity/Computability/TreeEval/Reader/Cert/Weight.lean +++ b/Complexity/Computability/TreeEval/Reader/Cert/Weight.lean @@ -37,11 +37,11 @@ open Turing MultiTapeTM ComputableTidilyInSpace /-! ### Half of a weight, over a counter -/ /-- A factor of half of a weight, on `((p, k, o), x)` and the counter and product `(j, a)`. -/ -def halfStep (s : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ × ℕ) : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ × ℕ := +private def halfStep (s : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ × ℕ) : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ × ℕ := (s.1, s.2.1 + 1, mulMod s.1.1.1 s.2.2 (chi s.1.1.1 (s.1.1.2.1.testBit (s.1.1.2.2 + s.2.1)) (s.1.2.getD s.2.1 0))) -theorem iterate_halfStep (p k o : ℕ) (x : List ℕ) (a : ℕ) (n : ℕ) : +private theorem iterate_halfStep (p k o : ℕ) (x : List ℕ) (a : ℕ) (n : ℕ) : halfStep^[n] (((p, k, o), x), 0, a) = (((p, k, o), x), n, (List.range n).foldl (fun a j => mulMod p a (chi p (k.testBit (o + j)) (x.getD j 0))) a) := by induction n with @@ -50,12 +50,12 @@ theorem iterate_halfStep (p k o : ℕ) (x : List ℕ) (a : ℕ) (n : ℕ) : rw [Function.iterate_succ_apply', ih, List.range_succ, List.foldl_append] rfl -theorem weight_eq (p ℓ k : ℕ) (x y : List ℕ) : +private theorem weight_eq (p ℓ k : ℕ) (x y : List ℕ) : weight p ℓ k x y = mulMod p (halfStep^[ℓ] (((p, k, 0), x), 0, 1 % p)).2.2 (halfStep^[ℓ] (((p, k, ℓ), y), 0, 1 % p)).2.2 := by simp only [weight, iterate_halfStep, zero_add] -theorem length_chi_le (p : ℕ) (b : Bool) (x : ℕ) : +private theorem length_chi_le (p : ℕ) (b : Bool) (x : ℕ) : (encNat (chi p b x)).length ≤ (encNat p).length + (encNat x).length + 1 := by rcases Nat.eq_zero_or_pos p with rfl | hp · cases b @@ -66,7 +66,7 @@ theorem length_chi_le (p : ℕ) (b : Bool) (x : ℕ) : (show chi p b x ≤ p by cases b <;> exact (Nat.mod_lt _ hp).le) omega -theorem sum_length_getD_le (x : List ℕ) (j : ℕ) : +private theorem sum_length_getD_le (x : List ℕ) (j : ℕ) : ∑ i ∈ Finset.range j, (encNat (x.getD i 0)).length ≤ (encList encNat x).length := by induction x generalizing j with | nil => simp @@ -80,7 +80,7 @@ theorem sum_length_getD_le (x : List ℕ) (j : ℕ) : omega /-- For `p = 0`, the products of half of a weight are no longer than their factors together. -/ -theorem length_halfStep_zero_le (k o : ℕ) (x : List ℕ) (j : ℕ) : +private theorem length_halfStep_zero_le (k o : ℕ) (x : List ℕ) (j : ℕ) : (encNat (halfStep^[j] (((0, k, o), x), 0, 1 % 0)).2.2).length ≤ ∑ i ∈ Finset.range j, ((encNat (x.getD i 0)).length + 1) + 1 := by induction j with @@ -97,7 +97,7 @@ theorem length_halfStep_zero_le (k o : ℕ) (x : List ℕ) (j : ℕ) : /-- **The products of half of a weight** are no longer than the prime, the register and the counter together. -/ -theorem length_halfStep_le (p k o : ℕ) (x : List ℕ) (j : ℕ) : +private theorem length_halfStep_le (p k o : ℕ) (x : List ℕ) (j : ℕ) : (encNat (halfStep^[j] (((p, k, o), x), 0, 1 % p)).2.2).length ≤ (encNat p).length + (encList encNat x).length + j + 1 := by rcases Nat.eq_zero_or_pos p with rfl | hp @@ -118,10 +118,10 @@ theorem length_halfStep_le (p k o : ℕ) (x : List ℕ) (j : ℕ) : omega /-- The encoding of the states of `halfStep`. -/ -abbrev encHalf : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ × ℕ ↪ List Bool := +private abbrev encHalf : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ × ℕ ↪ List Bool := encPair (encPair encNat3 (encList encNat)) (encPair encNat encNat) -theorem halfStep_inSpace : +private theorem halfStep_inSpace : ComputableTidilyInSpace halfStep encHalf encHalf fun s => (encHalf s).length + 1 := by have hl : (fun s => (encHalf s).length) ≼ fun s => (encHalf s).length + 1 := .of_le fun _ => by omega @@ -145,11 +145,11 @@ theorem halfStep_inSpace : exact budget_prod hpar (budget_prod hsucc hm) /-- The encoding of the arguments of half of a weight. -/ -abbrev encHalfIn : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ ↪ List Bool := +private abbrev encHalfIn : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ ↪ List Bool := encPair (encPair encNat3 (encList encNat)) encNat /-- **Half of a weight**, from `(((p, k, o), x), n)`. -/ -theorem half_inSpace : +private theorem half_inSpace : ComputableTidilyInSpace (fun h : ((ℕ × ℕ × ℕ) × List ℕ) × ℕ => (halfStep^[h.2] (h.1, 0, 1 % h.1.1.1)).2.2) encHalfIn encNat fun h => 256 * ((encHalfIn h).length + h.2 + 1) := by diff --git a/Complexity/Computability/TreeEval/Reader/Correct.lean b/Complexity/Computability/TreeEval/Reader/Correct.lean index d839582a2..b58fb964f 100644 --- a/Complexity/Computability/TreeEval/Reader/Correct.lean +++ b/Complexity/Computability/TreeEval/Reader/Correct.lean @@ -49,7 +49,7 @@ abbrev cfg (p : ℕ) (R : Regs) (st : List Frame) (mode : Mode) (ctl : Ctl) (out variable {T} /-- One step of the leaf loop. -/ -theorem next_leaf {p : ℕ} (R : Regs) (st : List Frame) (neg : Bool) (t : Fin 3) {i : ℕ} +private theorem next_leaf {p : ℕ} (R : Regs) (st : List Frame) (neg : Bool) (t : Fin 3) {i : ℕ} (hi : i < ℓ) (out : List Bool) : machine.next T.encode (cfg (ℓ := ℓ) (H := H) p R st (.call neg t) (.leaf i) out) = cfg (ℓ := ℓ) (H := H) p (R.set t (modifyAt (R.get t) i (addMod p @@ -58,12 +58,12 @@ theorem next_leaf {p : ℕ} (R : Regs) (st : List Frame) (neg : Bool) (t : Fin 3 simp [ReadMachine.next, machine, step, addr, ReadMachine.readBit, offset, hi, Nat.add_assoc, List.getD_eq_getElem?_getD] -theorem cast_ite_sgnVal {p : ℕ} [Fact p.Prime] (b neg : Bool) : +private theorem cast_ite_sgnVal {p : ℕ} [Fact p.Prime] (b neg : Bool) : (((if b then sgnVal p neg else 0 : ℕ)) : ZMod p) = sgn neg * bitVal (ZMod p) b := by cases b <;> simp [BitString.bitVal] /-- **The leaf loop**: after `i ≤ ℓ` steps, bits `0, …, i - 1` of the leaf have been added. -/ -theorem runFrom_leaf_loop {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin ℓ → Bool} +private theorem runFrom_leaf_loop {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin ℓ → Bool} (hv : T.nodeAt (path st) = .leaf v) (R : Regs) (hR : R.WF p ℓ) (neg : Bool) (t : Fin 3) (out : List Bool) : ∀ i ≤ ℓ, ∃ R', machine.runFrom T.encode (cfg (ℓ := ℓ) (H := H) p R st (.call neg t) (.leaf 0) out) i = @@ -97,7 +97,7 @@ theorem runFrom_leaf_loop {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin /-- **The leaf phase**: a call on the leaf at the current path adds `±` its value to the target register and returns, in `ℓ + 2` steps. -/ -theorem runFrom_leaf {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin ℓ → Bool} +private theorem runFrom_leaf {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin ℓ → Bool} (hv : T.nodeAt (path st) = .leaf v) (R : Regs) (hR : R.WF p ℓ) (neg : Bool) (t : Fin 3) (out : List Bool) : ∃ R', machine.runFrom T.encode (cfg (ℓ := ℓ) (H := H) p R st (.call neg t) .run out) (ℓ + 2) = @@ -120,7 +120,7 @@ theorem runFrom_leaf {p : ℕ} [Fact p.Prime] {st : List Frame} {v : Fin ℓ → /-- Sums over the positions of a table of `n` blocks of `ℓ` bits whose position within the block is `i`, as sums over the blocks. -/ -theorem sum_range_mul_ite_mod {M : Type*} [AddCommMonoid M] (n : ℕ) {i : ℕ} (hi : i < ℓ) +private theorem sum_range_mul_ite_mod {M : Type*} [AddCommMonoid M] (n : ℕ) {i : ℕ} (hi : i < ℓ) (F : ℕ → M) : ∑ q ∈ Finset.range (n * ℓ), (if q % ℓ = i then F q else 0) = ∑ k ∈ Finset.range n, F (k * ℓ + i) := by @@ -135,7 +135,7 @@ theorem sum_range_mul_ite_mod {M : Type*} [AddCommMonoid M] (n : ℕ) {i : ℕ} simp [hi] /-- One step of the pass over a table. -/ -theorem next_scan {p : ℕ} (R : Regs) (fr : Frame) (st : List Frame) {k : ℕ} +private theorem next_scan {p : ℕ} (R : Regs) (fr : Frame) (st : List Frame) {k : ℕ} (hk : k < tableLength ℓ) (acc : List ℕ) (out : List Bool) : machine.next T.encode (cfg (ℓ := ℓ) (H := H) p R (fr :: st) .ret (.scan k acc) out) = cfg (ℓ := ℓ) (H := H) p R (fr :: st) .ret (.scan (k + 1) @@ -148,7 +148,7 @@ theorem next_scan {p : ℕ} (R : Regs) (fr : Frame) (st : List Frame) {k : ℕ} /-- **The pass over a table**: after `k` bits, the sums for every output bit `i` cover the positions `q < k` of the table for `i` that are set, weighted by the masked registers. -/ -theorem runFrom_scan_loop {p : ℕ} [Fact p.Prime] {fr : Frame} {st : List Frame} +private theorem runFrom_scan_loop {p : ℕ} [Fact p.Prime] {fr : Frame} {st : List Frame} {f : Gate ℓ} (hf : T.nodeAt (path st) = .gate f) (R : Regs) (out : List Bool) : ∀ k ≤ tableLength ℓ, ∃ acc, machine.runFrom T.encode @@ -187,7 +187,7 @@ theorem runFrom_scan_loop {p : ℕ} [Fact p.Prime] {fr : Frame} {st : List Frame · simp [hb, hi, modifyAt, List.getD_eq_getElem?_getD] · simp [hb, BitString.bitVal] -theorem mul_add_div_self (k : ℕ) (i : Fin ℓ) : (k * ℓ + i) / ℓ = k := by +private theorem mul_add_div_self (k : ℕ) (i : Fin ℓ) : (k * ℓ + i) / ℓ = k := by rw [Nat.add_comm, Nat.add_mul_div_right _ _ (Nat.zero_lt_of_lt i.isLt), Nat.div_eq_of_lt i.isLt, zero_add] @@ -201,7 +201,7 @@ theorem tableBit_mul_add (f : Gate ℓ) (k : ℕ) (i : Fin ℓ) : /-- **The update of a round**: from phase `1`, the pass over the table of the gate subtracts `±` the multilinear extensions of its output bits at the masked registers, in `4^ℓ * ℓ + 2` steps, and calls the left child for subtraction. -/ -theorem runFrom_update {p : ℕ} [Fact p.Prime] {fr : Frame} {st : List Frame} +private theorem runFrom_update {p : ℕ} [Fact p.Prime] {fr : Frame} {st : List Frame} {f : Gate ℓ} (hf : T.nodeAt (path st) = .gate f) (hph : fr.phase = 1) (R : Regs) (hR : R.WF p ℓ) (out : List Bool) : ∃ R', machine.runFrom T.encode @@ -232,28 +232,28 @@ theorem runFrom_update {p : ℕ} [Fact p.Prime] {fr : Frame} {st : List Frame} rw [tableBit_mul_add, cast_weight, mul_add_div_self] rfl -theorem next_push {p : ℕ} (R : Regs) {st : List Frame} (hst : st.length ≠ H) (neg : Bool) +private theorem next_push {p : ℕ} (R : Regs) {st : List Frame} (hst : st.length ≠ H) (neg : Bool) (t : Fin 3) (out : List Bool) : machine.next T.encode (cfg (ℓ := ℓ) (H := H) p R st (.call neg t) .run out) = cfg (ℓ := ℓ) (H := H) p (R.scale p (t + 1) (unitVal 0)) (⟨0, 0, neg, t⟩ :: st) (.call false (t + 1)) .run out := by simp [ReadMachine.next, machine, step, runStep, hst] -theorem next_phase0 {p : ℕ} (R : Regs) (j : ℕ) (neg : Bool) (t : Fin 3) (st : List Frame) +private theorem next_phase0 {p : ℕ} (R : Regs) (j : ℕ) (neg : Bool) (t : Fin 3) (st : List Frame) (out : List Bool) : machine.next T.encode (cfg (ℓ := ℓ) (H := H) p R (⟨j, 0, neg, t⟩ :: st) .ret .run out) = cfg (ℓ := ℓ) (H := H) p (R.scale p (t + 2) (unitVal j)) (⟨j, 1, neg, t⟩ :: st) (.call false (t + 2)) .run out := by simp [ReadMachine.next, machine, step, runStep] -theorem next_phase2 {p : ℕ} (R : Regs) (j : ℕ) (neg : Bool) (t : Fin 3) (st : List Frame) +private theorem next_phase2 {p : ℕ} (R : Regs) (j : ℕ) (neg : Bool) (t : Fin 3) (st : List Frame) (out : List Bool) : machine.next T.encode (cfg (ℓ := ℓ) (H := H) p R (⟨j, 2, neg, t⟩ :: st) .ret .run out) = cfg (ℓ := ℓ) (H := H) p (R.scale p (t + 1) (unitInv p j)) (⟨j, 3, neg, t⟩ :: st) (.call true (t + 2)) .run out := by simp [ReadMachine.next, machine, step, runStep] -theorem next_phase3 {p : ℕ} (R : Regs) (j : ℕ) (neg : Bool) (t : Fin 3) (st : List Frame) +private theorem next_phase3 {p : ℕ} (R : Regs) (j : ℕ) (neg : Bool) (t : Fin 3) (st : List Frame) (out : List Bool) : machine.next T.encode (cfg (ℓ := ℓ) (H := H) p R (⟨j, 3, neg, t⟩ :: st) .ret .run out) = if j + 1 < p - 1 then @@ -272,7 +272,7 @@ def CallSpec (T : Tree ℓ H) (p : ℕ) [Fact p.Prime] (P : List Bool) /-- **One round** of the machine at a gate performs `gateRound` and starts the next round or returns. -/ -theorem exists_runFrom_round {p : ℕ} [Fact p.Prime] {st : List Frame} +private theorem exists_runFrom_round {p : ℕ} [Fact p.Prime] {st : List Frame} {f : Gate ℓ} (hf : T.nodeAt (path st) = .gate f) {pl pr : ZMod p → Fin 3 → TreeEval.State (ZMod p) ℓ → TreeEval.State (ZMod p) ℓ} (hl : CallSpec T p (path st ++ [false]) pl) (hr : CallSpec T p (path st ++ [true]) pr) @@ -311,7 +311,7 @@ theorem exists_runFrom_round {p : ℕ} [Fact p.Prime] {st : List Frame} /-- The rounds `j, …, j + k` of a gate, the last ones before `p - 1`, perform the corresponding `gateRound`s and return. -/ -theorem exists_runFrom_rounds {p : ℕ} [Fact p.Prime] {st : List Frame} +private theorem exists_runFrom_rounds {p : ℕ} [Fact p.Prime] {st : List Frame} {f : Gate ℓ} (hf : T.nodeAt (path st) = .gate f) {pl pr : ZMod p → Fin 3 → TreeEval.State (ZMod p) ℓ → TreeEval.State (ZMod p) ℓ} (hl : CallSpec T p (path st ++ [false]) pl) (hr : CallSpec T p (path st ++ [true]) pr) @@ -392,12 +392,13 @@ theorem getElem?_encode_height_end : T.encode[ℓ + 1 + H]? = some false := by simp [show ℓ + 1 + H - ℓ = H + 1 by omega] /-- The state while searching the prime. -/ -abbrev primeCfg (ℓ H q d : ℕ) : ReadMachine.Cfg State := +private abbrev primeCfg (ℓ H q d : ℕ) : ReadMachine.Cfg State := ⟨⟨ℓ, H, 0, ([], [], []), [], .ret, .prime q d⟩, []⟩ /-- **The header**: after `ℓ + H + 2` steps the machine has read `ℓ` and `H` and starts the search for the prime at `2ℓ + 2`. -/ -theorem run_header : machine.run T.encode (ℓ + 1 + (H + 1)) = primeCfg ℓ H (2 * ℓ + 2) 2 := by +private theorem run_header : machine.run T.encode (ℓ + 1 + (H + 1)) = primeCfg ℓ H + (2 * ℓ + 2) 2 := by have h₁ : ∀ n ≤ ℓ, machine.run T.encode n = ⟨⟨0, 0, 0, ([], [], []), [], .ret, .hdrLength n⟩, []⟩ := by intro n hn @@ -424,11 +425,12 @@ theorem run_header : machine.run T.encode (ℓ + 1 + (H + 1)) = primeCfg ℓ H ( getElem?_encode_height_end (T := T)] /-- The registers at the start: three registers of `ℓ` zeros. -/ -abbrev zeroRegs (ℓ : ℕ) : Regs := (List.replicate ℓ 0, List.replicate ℓ 0, List.replicate ℓ 0) +private abbrev zeroRegs (ℓ : ℕ) : Regs := + (List.replicate ℓ 0, List.replicate ℓ 0, List.replicate ℓ 0) /-- **Testing a candidate**: from divisor `d`, with no divisor in `[2, d)`, the machine finds that `q` is prime and starts the procedure with it, or that it is not and moves to `q + 1`. -/ -theorem exists_runFrom_test {q : ℕ} : +private theorem exists_runFrom_test {q : ℕ} : ∀ k d, d + k = q → 2 ≤ d → (∀ e, 2 ≤ e → e < d → q % e ≠ 0) → ∃ n, machine.runFrom T.encode (primeCfg ℓ H q d) n = if q.Prime then cfg (ℓ := ℓ) (H := H) q (zeroRegs ℓ) [] (.call false 2) .run [] @@ -468,7 +470,7 @@ theorem le_primeFor (ℓ : ℕ) : 2 * ℓ + 2 ≤ primeFor ℓ := (Nat.find_spec (Nat.exists_infinite_primes (2 * ℓ + 2))).1 /-- **The search for the prime** finds `primeFor ℓ` and starts the procedure with it. -/ -theorem exists_runFrom_search : +private theorem exists_runFrom_search : ∀ k q, q + k = primeFor ℓ → 2 * ℓ + 2 ≤ q → ∃ n, machine.runFrom T.encode (primeCfg ℓ H q 2) n = cfg (ℓ := ℓ) (H := H) (primeFor ℓ) (zeroRegs ℓ) [] (.call false 2) .run [] := by @@ -493,12 +495,12 @@ theorem exists_runFrom_search : obtain ⟨n', hn'⟩ := ih (q + 1) (by omega) (by omega) exact ⟨n + n', by rw [ReadMachine.runFrom_add, hn, hn']⟩ -theorem toState_zeroRegs (p : ℕ) : (zeroRegs ℓ).toState p ℓ = 0 := by +private theorem toState_zeroRegs (p : ℕ) : (zeroRegs ℓ).toState p ℓ = 0 := by funext r i fin_cases r <;> simp [Regs.toState, Regs.get, List.getD_eq_getElem?_getD] /-- Registers holding the bits of a value, read in `ZMod p`, hold `0` and `1`. -/ -theorem map_get_eq_ofFn {p : ℕ} [Fact p.Prime] {R : Regs} (hR : R.WF p ℓ) {v : Fin ℓ → Bool} +private theorem map_get_eq_ofFn {p : ℕ} [Fact p.Prime] {R : Regs} (hR : R.WF p ℓ) {v : Fin ℓ → Bool} (h : R.toState p ℓ 2 = embed v) : (R.get 2).map (· == 1) = List.ofFn v := by have hp := (Fact.out : p.Prime).one_lt obtain ⟨hlen, hlt⟩ := hR 2 diff --git a/Complexity/Computability/USTCON/Reader/Correct.lean b/Complexity/Computability/USTCON/Reader/Correct.lean index d46386ddb..a424019f9 100644 --- a/Complexity/Computability/USTCON/Reader/Correct.lean +++ b/Complexity/Computability/USTCON/Reader/Correct.lean @@ -116,7 +116,7 @@ theorem Reaches.trans {q₁ q₂ q₃ : State} (h₁ : Reaches I q₁ q₂) (h ⟨k₁ + k₂, by rw [Turing.ReadMachine.runFrom_add, hk₁, hk₂]⟩ /-- One step without output. -/ -theorem Reaches.single {q q' : State} (hh : q.ctl ≠ .done) +private theorem Reaches.single {q q' : State} (hh : q.ctl ≠ .done) (hs : step q (machine.readBit I.encode q) = (q', [])) : Reaches I q q' := fun o ↦ ⟨1, by rw [Turing.ReadMachine.runFrom_one, Turing.ReadMachine.next_of_not_halt _ _ @@ -125,7 +125,7 @@ theorem Reaches.single {q q' : State} (hh : q.ctl ≠ .done) rw [hs, List.append_nil]⟩ /-- Steps along a sequence of states. -/ -theorem reaches_iterate (f : ℕ → State) (m : ℕ) (h : ∀ i < m, Reaches I (f i) (f (i + 1))) : +private theorem reaches_iterate (f : ℕ → State) (m : ℕ) (h : ∀ i < m, Reaches I (f i) (f (i + 1))) : Reaches I (f 0) (f m) := by induction m with | zero => exact .refl _ @@ -164,7 +164,7 @@ def headerState (I : USTCONInstance) : State := len := 136240 } /-- **The header**: the machine counts the number of vertices, the source and the target. -/ -theorem reaches_header : Reaches I init (headerState I) := by +private theorem reaches_header : Reaches I init (headerState I) := by -- the number of vertices have h₁ : Reaches I init { init with ctl := .hdrS, n := I.n } := by refine (reaches_iterate (fun i ↦ { init with cnt := i }) I.n @@ -195,7 +195,7 @@ theorem reaches_header : Reaches I init (headerState I) := by /-- **The halvings**: halving `m` until it vanishes adds `16` to the depth and `4168` to the walk length for each of its binary digits. -/ -theorem reaches_size (q : State) (m d l : ℕ) : +private theorem reaches_size (q : State) (m d l : ℕ) : Reaches I { q with ctl := .size, cnt := m, depth := d, len := l } { q with ctl := .start @@ -261,7 +261,7 @@ private theorem inputRot_slotVal (v : Fin I.n × Fin I.n) (b : Label) : /-- **The evaluation of the rotation map**: from a frame for level `m ≥ 1`, freshly pushed with the label `a` above the registers of a vertex `x` of the `m`-th graph, the machine reaches the registers of the rotation of the `m`-th graph at `(x, a)`, with the label at the far end below the frames. -/ -theorem reaches_eval (q : State) (hc : q.ctl = .eval) (hn : q.n = I.n) (hs : q.s = I.s) +private theorem reaches_eval (q : State) (hc : q.ctl = .eval) (hn : q.n = I.n) (hs : q.s = I.s) (ht : q.t = I.t) {m : ℕ} (hm : m ≠ 0) (x : ReingoldVertex (Fin I.n × Fin I.n) Label m) (a : Label) (hev : q.ev = (⟨(x.toList).1, (x.toList).2, [(.zig₀, a)]⟩ : @@ -327,7 +327,7 @@ private theorem depth_ne_zero (a : ℕ) : depth a ≠ 0 := by /-- **The steps of a walk**: from the next step with the registers of `x`, the digits `w` and `j` steps left, the machine reaches the end of the walk with the registers of its last vertex and the digits `w / B ^ j` left. -/ -theorem reaches_walk {m : ℕ} (hm : m ≠ 0) (q : State) (hc : q.ctl = .next) (hn : q.n = I.n) +private theorem reaches_walk {m : ℕ} (hm : m ≠ 0) (q : State) (hc : q.ctl = .next) (hn : q.n = I.n) (hs : q.s = I.s) (ht : q.t = I.t) (x : ReingoldVertex (Fin I.n × Fin I.n) Label m) (w j : ℕ) (hev : q.ev = ⟨slotVal x.root, (x.toList).2, []⟩) (hw : q.w = w) (hj : q.j = j) : Reaches I q { q with @@ -392,7 +392,8 @@ theorem reaches_walk {m : ℕ} (hm : m ≠ 0) (q : State) (hc : q.ctl = .next) ( /-- **A walk of a counter**: from the start of the walk of the counter `c`, the machine fills the labels of the start vertex `(⋯ ((s, s), 0) ⋯, 0)` and walks along the digits of `c`. -/ -theorem reaches_start {m : ℕ} (hm : m ≠ 0) (q : State) (hc : q.ctl = .start) (hn : q.n = I.n) +private theorem reaches_start {m : ℕ} (hm : m ≠ 0) (q : State) (hc : q.ctl = .start) + (hn : q.n = I.n) (hs : q.s = I.s) (ht : q.t = I.t) (hd : q.depth = m) : Reaches I q { q with ctl := .check @@ -444,14 +445,15 @@ def Outputs (q : State) (b : Bool) : Prop := (machine.runFrom I.encode ⟨q, o⟩ k).out = o ++ [b] /-- Steps without output before halting with an output. -/ -theorem Reaches.outputs {q q' : State} {b : Bool} (h : Reaches I q q') (h' : Outputs I q' b) : +private theorem Reaches.outputs {q q' : State} {b : Bool} (h : Reaches I q q') + (h' : Outputs I q' b) : Outputs I q b := fun o ↦ let ⟨k₁, hk₁⟩ := h o let ⟨k₂, hk₂⟩ := h' o ⟨k₁ + k₂, by rw [Turing.ReadMachine.runFrom_add, hk₁]; exact hk₂⟩ /-- Halting in one step with an output. -/ -theorem outputs_single {q q' : State} {b : Bool} (hh : q.ctl ≠ .done) +private theorem outputs_single {q q' : State} {b : Bool} (hh : q.ctl ≠ .done) (hs : step q (machine.readBit I.encode q) = (q', [b])) (hq' : q'.ctl = .done) : Outputs I q b := fun o ↦ ⟨1, by @@ -489,7 +491,7 @@ open scoped Classical in /-- **The counters**: from the start of the walk of a counter `c ≤ B ^ T`, the machine halts with the output `[true]` if the walk of some counter between `c` and `B ^ T` succeeds, and `[false]` otherwise. -/ -theorem outputs_start {m T : ℕ} (hm : m ≠ 0) : +private theorem outputs_start {m T : ℕ} (hm : m ≠ 0) : ∀ d (q : State), numLabels ^ T - q.c = d → q.c ≤ numLabels ^ T → q.ctl = .start → q.n = I.n → q.s = I.s → q.t = I.t → q.depth = m → q.len = T → Outputs I q (decide (∃ c', q.c ≤ c' ∧ c' < numLabels ^ T ∧ Success I m T c')) := by @@ -573,7 +575,7 @@ private theorem walkLength_eq (a : ℕ) : 136240 + 4168 * a = walkLength a := by open scoped Classical in /-- **The machine decides undirected connectivity**: from the initial state, it halts with the output `[true]` if `t` is reachable from `s`, and `[false]` otherwise. -/ -theorem outputs_init : Outputs I init (decide (I ∈ USTCON)) := by +private theorem outputs_init : Outputs I init (decide (I ∈ USTCON)) := by classical set a := Nat.size I.n have hstart := (reaches_header (I := I)).trans From cf8017cc159cdc5ba58c79b577d7ddf39df1fb09 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:59:53 -0400 Subject: [PATCH 2/2] refactor(classes): keep five core API rules public Review 5636431835 on #691: `ProofSystem.mem`, `ProofSystem.polynomiallyBounded_ofVerifier`, `PolyTimeReducible.of_subset` and the two error-exponent-to-verifier conversions (`IsMerlinArthurVerifierWithErrorExponent.isMerlinArthurVerifier`, `IsArthurMerlinVerifierWithErrorExponent.isArthurMerlinVerifier`) are interface rules, not proof steps. Restore them as on `main`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Complexity/Classes/ArthurMerlin/Amplification.lean | 6 ++---- .../Computability/Complexity/Classes/Promise/Reduction.lean | 2 +- Complexity/Computability/Complexity/ProofSystem.lean | 4 ++-- 3 files changed, 5 insertions(+), 7 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean index 6ed996260..05ae31ec7 100644 --- a/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean @@ -169,8 +169,7 @@ theorem IsMerlinArthurVerifier.repeatMajority {q p : Polynomial ℕ} {V : α × omega /-- Error at most `2 ^ (-e(n)) ≤ 1 / 4` is error at most `1 / 3`. -/ -private theorem IsMerlinArthurVerifierWithErrorExponent.isMerlinArthurVerifier - {e q p : Polynomial ℕ} +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 := @@ -326,8 +325,7 @@ theorem IsArthurMerlinVerifier.repeatMajority {p q : Polynomial ℕ} {V : α × omega /-- Error at most `2 ^ (-e(n)) ≤ 1 / 4` is error at most `1 / 3`. -/ -private theorem IsArthurMerlinVerifierWithErrorExponent.isArthurMerlinVerifier - {e p q : Polynomial ℕ} +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 := diff --git a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean index 4b62e7f2e..8c3de198e 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean @@ -120,7 +120,7 @@ theorem PolyTimeReducible.trans (hXY : PolyTimeReducible encA encB X Y) /-- A promise problem reduces, by the identity, to any problem with more yes-instances and more no-instances: enlarging the promise can only make a problem harder. -/ -private theorem PolyTimeReducible.of_subset (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) : +theorem PolyTimeReducible.of_subset (hyes : Y.yes ⊆ Y'.yes) (hno : Y.no ⊆ Y'.no) : PolyTimeReducible encB encB Y Y' := ⟨id, ComputableInPolyTime.id', fun _ h => hyes h, fun _ h => hno h⟩ diff --git a/Complexity/Computability/Complexity/ProofSystem.lean b/Complexity/Computability/Complexity/ProofSystem.lean index e5f789fd1..6f1628eab 100644 --- a/Complexity/Computability/Complexity/ProofSystem.lean +++ b/Complexity/Computability/Complexity/ProofSystem.lean @@ -100,7 +100,7 @@ namespace ProofSystem instance : CoeFun (ProofSystem enc L) fun _ => List Bool → α := ⟨toFun⟩ /-- **Soundness**: every word proves a member of `L`. -/ -private theorem mem (P : ProofSystem enc L) (π : List Bool) : P π ∈ L := +theorem mem (P : ProofSystem enc L) (π : List Bool) : P π ∈ L := P.range_eq.subset ⟨π, rfl⟩ /-- **Completeness**: every member of `L` has a proof. -/ @@ -268,7 +268,7 @@ theorem ofVerifier_frame_append (D : Decoder enc) /-- The proof system of a verifier is polynomially bounded: an instance `a` has a proof of length `2 * (enc a).length + 1 + p (enc a).length`. -/ -private theorem polynomiallyBounded_ofVerifier (D : Decoder enc) +theorem polynomiallyBounded_ofVerifier (D : Decoder enc) (hV : ComputableInPolyTime V (encPair enc encBits) encBool) (hVL : IsVerifier enc p V L) {a₀ : α} (ha₀ : a₀ ∈ L) : (ofVerifier D hV hVL ha₀).PolynomiallyBounded := by