refactor(complexity): expose plain computableInPolyTime_splitAlternatingBlocks (#750)

Complexity/Computability/Complexity/Classes/BooleanHierarchy/Kadin.lean

@@ -121,23 +121,6 @@ private theorem computableTidilyInPolyTime_shiftVerifier (p : Polynomial ℕ)
     (bitsAppend (fst _ _).snd' (bitsTakeWithInput (snd _ _) hn))).prod
     (bitsDropWithInput (snd _ _) hn))
 
-private theorem computableTidilyInPolyTime_splitAlternatingBlocks' {γ : Type}
-    {encIn : γ ↪ List Bool} (ps : List (Polynomial ℕ × Polynomial ℕ)) {N : γ → ℕ}
-    (hN : ComputableTidilyInPolyTime N encIn encUnary) {W : γ → List Bool}
-    (hW : ComputableTidilyInPolyTime W encIn encBits) :
-    ComputableTidilyInPolyTime
-      (fun x => splitAlternatingBlocks (ps.map fun pq => (pq.1.eval (N x), pq.2.eval (N x)))
-        (W x)) encIn (encPair encBits encBits) := by
-  induction ps generalizing W with
-  | nil => exact .const ([], [])
-  | cons pq ps ih =>
-    have hp := (ComputableTidilyInPolyTime.unary_eval pq.1).comp hN
-    have hq := (ComputableTidilyInPolyTime.unary_eval pq.2).comp hN
-    have ht := ih (hW.bitsDropWithInput (ComputableTidilyInPolyTime.unary_add.comp
-      (hp.prod hq)))
-    exact ((hW.bitsTakeWithInput hp).bitsAppend ht.fst').prod
-      (((hW.bitsDropWithInput hp).bitsTakeWithInput hq).bitsAppend ht.snd')
-
 /-- `R : α → List Bool → Prop` is verified at `(b, k)` on prefixes `s` of length `q |enc a|` by a
 polynomial-time alternating verifier whose certificate block lengths are polynomials in
 `|enc a|`. -/
@@ -207,11 +190,11 @@ private theorem and (h₁ : OnSliceAlt enc b k q R₁) (h₂ : OnSliceAlt enc b
         (pqs.map fun pq => (pq.1.eval (enc x.1.1).length, pq.2.eval (enc x.1.1).length)) x.2
       V (x.1, w.1) && W (x.1, w.2),
     by simp [pqs, hp, hq], ?_, fun a s hs => ?_⟩
-  · have hn : ComputableTidilyInPolyTime
+  · have hn : ComputableInPolyTime
         (fun x : (α × List Bool) × List Bool => (enc x.1.1).length)
         (encPair (encPair enc encBits) encBits) encUnary :=
-      (encoding_length enc).comp (fst _ _).fst'
-    have hs := computableTidilyInPolyTime_splitAlternatingBlocks' pqs hn (snd _ _)
+      .of_tidy ((encoding_length enc).comp (fst _ _).fst')
+    have hs := (computableInPolyTime_splitAlternatingBlocks pqs hn (.snd _ _)).tidy
     exact .of_tidy <|
       (hV.tidy.comp ((fst _ _).prod hs.fst')).bool_and'
         (hW.tidy.comp ((fst _ _).prod hs.snd'))

Complexity/Computability/Complexity/Classes/PH/Closure.lean

@@ -25,6 +25,9 @@ The construction uses exact certificate lengths and polynomial-time bit-string s
 
 ## Main results
 
+* `alternation_splitAlternatingBlocks`: alternating-quantifier equivalence for paired blocks.
+* `computableInPolyTime_splitAlternatingBlocks`: plain polynomial-time certificate for splitting
+  paired blocks whose lengths are polynomials of a computed unary size.
 * `inter_mem_SigmaP`, `union_mem_SigmaP`: closure of each existential level.
 * `inter_mem_PiP`, `union_mem_PiP`: closure of each universal level.
 * `compl_mem_PH`, `inter_mem_PH`, `union_mem_PH`, `diff_mem_PH`: Boolean closure of the hierarchy.
@@ -102,8 +105,6 @@ theorem alternation_splitAlternatingBlocks (ns : List (ℕ × ℕ)) (q : Bool)
       · rintro ⟨⟨u, hu, hP⟩, ⟨v, hv, hQ⟩⟩
         exact ⟨u ++ v, by simp [hu, hv], (key u v hu hv false).2 ⟨hP, hQ⟩⟩
 
-/-- Splitting paired blocks is polynomial-time when their lengths are fixed polynomials of a
-computed unary size. -/
 private theorem computableTidilyInPolyTime_splitAlternatingBlocks {γ : Type}
     {encIn : γ ↪ List Bool} (ps : List (Polynomial ℕ × Polynomial ℕ)) {N : γ → ℕ}
     (hN : ComputableTidilyInPolyTime N encIn encUnary) {W : γ → List Bool}
@@ -121,6 +122,17 @@ private theorem computableTidilyInPolyTime_splitAlternatingBlocks {γ : Type}
     exact ((hW.bitsTakeWithInput hp).bitsAppend ht.fst').prod
       (((hW.bitsDropWithInput hp).bitsTakeWithInput hq).bitsAppend ht.snd')
 
+/-- Splitting paired blocks is polynomial-time when their lengths are fixed polynomials of a
+computed unary size. -/
+theorem computableInPolyTime_splitAlternatingBlocks {γ : Type}
+    {encIn : γ ↪ List Bool} (ps : List (Polynomial ℕ × Polynomial ℕ)) {N : γ → ℕ}
+    (hN : ComputableInPolyTime N encIn encUnary) {W : γ → List Bool}
+    (hW : ComputableInPolyTime W encIn encBits) :
+    ComputableInPolyTime
+      (fun x => splitAlternatingBlocks (ps.map fun pq => (pq.1.eval (N x), pq.2.eval (N x)))
+        (W x)) encIn (encPair encBits encBits) :=
+  .of_tidy (computableTidilyInPolyTime_splitAlternatingBlocks ps hN.tidy hW.tidy)
+
 variable {α : Type} {enc : α ↪ List Bool}
 
 /-- Conjoin two alternating verifiers by pairing equally positioned certificate blocks. -/
@@ -159,10 +171,10 @@ private theorem exists_inter_verifier {q : Bool} {k : ℕ} {A B : Set α}
     simpa only [List.map_snd_zip hlen.ge] using hB
   refine ⟨_, _, ?_, ?_, hA'.inter hB'⟩
   · simp [hp, hq]
-  · have hn : ComputableTidilyInPolyTime (fun x : α × List Bool => (enc x.1).length)
+  · have hn : ComputableInPolyTime (fun x : α × List Bool => (enc x.1).length)
         (encPair enc encBits) encUnary := by fun_prop
-    have hs := computableTidilyInPolyTime_splitAlternatingBlocks (ps.zip qs) hn
-      (ComputableTidilyInPolyTime.snd enc encBits)
+    have hs := (computableInPolyTime_splitAlternatingBlocks (ps.zip qs) hn
+      (.snd enc encBits)).tidy
     exact .of_tidy <|
       (hV.tidy.comp ((ComputableTidilyInPolyTime.fst enc encBits).prod hs.fst')).bool_and'
         (hW.tidy.comp ((ComputableTidilyInPolyTime.fst enc encBits).prod hs.snd'))

ComplexityTests/PHClosure.lean

@@ -32,6 +32,13 @@ example (q : Bool) (P Q : List Bool → Prop) :
       Alternation q [1, 0, 2] P ∧ Alternation q [2, 1, 0] Q :=
   alternation_splitAlternatingBlocks [(1, 2), (0, 1), (2, 0)] q P Q
 
+example (ps : List (Polynomial ℕ × Polynomial ℕ)) :
+    ComputableInPolyTime
+      (fun w : List Bool =>
+        splitAlternatingBlocks (ps.map fun pq => (pq.1.eval w.length, pq.2.eval w.length)) w)
+      encBits (encPair encBits encBits) :=
+  computableInPolyTime_splitAlternatingBlocks ps (.of_tidy (.encoding_length encBits)) .id'
+
 private theorem true_in_P : ({true} : Set Bool) ∈ P encBool :=
   ⟨id, ComputableInPolyTime.id', fun _ => Iff.rfl⟩
 
@@ -50,6 +57,13 @@ example : ({true} ∩ {false} : Set Bool) ∈ PiP 2 encBool :=
 /-- info: 'Cslib.Complexity.alternation_splitAlternatingBlocks' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in
 #print axioms alternation_splitAlternatingBlocks
+/--
+info: 'Cslib.Complexity.computableInPolyTime_splitAlternatingBlocks' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+-/
+#guard_msgs in
+#print axioms computableInPolyTime_splitAlternatingBlocks
 /-- info: 'Cslib.Complexity.inter_mem_SigmaP' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in
 #print axioms inter_mem_SigmaP