refactor(Computability/PolyTime): deduplicate certificate and fold helpers (#949)

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean

@@ -66,8 +66,8 @@ bounded-incidence, bounded-width $\mathbb{F}_2$ polynomial-system branch evaluat
 
 namespace Cslib.Complexity.SubexponentialSAT.SparsePolyCounter
 
-open Finset Cslib Cslib.BitString Cslib.Complexity Cslib.GenericRAM Cslib.LinearAlgebra
-open Turing.MultiTapeTM
+open Finset Cslib Cslib.BitString Cslib.CommonCountingAccum Cslib.Complexity Cslib.GenericRAM
+open Cslib.LinearAlgebra Turing.MultiTapeTM
 
 local notation "encSys" => encList (encList (encList encNat))
 

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean

@@ -444,20 +444,6 @@ private theorem sum_card_listScopeFamily_augScopes (n' : ℕ) (eqs' : List (List
   exact Finset.sum_congr rfl fun f _ =>
     congrArg Finset.card (listScopeFamily_map_equationVars n' eqs' f)
 
-private theorem le_foldl_max_of_mem {init x : ℕ} {l : List ℕ} (hx : x ∈ l) :
-    x ≤ l.foldl max init := by
-  have hinit : ∀ (m : ℕ) (ys : List ℕ), m ≤ ys.foldl max m := fun m ys => by
-    induction ys generalizing m with
-    | nil => exact le_rfl
-    | cons b bs ih => exact le_trans (Nat.le_max_left m b) (ih (max m b))
-  induction l generalizing init with
-  | nil => cases hx
-  | cons a as ih =>
-    simp only [List.foldl_cons]
-    rcases List.mem_cons.mp hx with rfl | hmem
-    · exact le_trans (Nat.le_max_right init x) (hinit (max init x) as)
-    · exact ih hmem
-
 private theorem varIncidence_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : List (List (List ℕ)))
     (v : Fin n') :
     let augScopes := withNeutralScopesList (eqs'.map equationVars) n'

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean

@@ -76,8 +76,8 @@ globally polynomial workspace.
 
 namespace Cslib.Complexity.SubexponentialSAT.SparsePolyCounter
 
-open Finset Cslib Cslib.BitString Cslib.Complexity Cslib.GenericRAM Cslib.LinearAlgebra
-open Turing.MultiTapeTM
+open Finset Cslib Cslib.BitString Cslib.CommonCountingAccum Cslib.Complexity Cslib.GenericRAM
+open Cslib.LinearAlgebra Turing.MultiTapeTM
 
 local notation "encSys" => encList (encList (encList encNat))
 
@@ -566,28 +566,6 @@ section LoopCertificates
 
 open ComputableInPolyTime
 
-private theorem le_foldl_max_init (init : ℕ) (xs : List ℕ) : init ≤ xs.foldl max init := by
-  induction xs generalizing init with
-  | nil => exact le_rfl
-  | cons b bs ih => exact (Nat.le_max_left init b).trans (ih (max init b))
-
-private theorem le_foldl_max_of_mem {xs : List ℕ} {x init : ℕ} (hx : x ∈ xs) :
-    x ≤ xs.foldl max init := by
-  induction xs generalizing init with
-  | nil => cases hx
-  | cons a as ih =>
-    rcases List.mem_cons.mp hx with rfl | hmem
-    · exact (Nat.le_max_right init x).trans (le_foldl_max_init (max init x) as)
-    · exact ih hmem
-
-private theorem foldl_max_le {xs : List ℕ} {init B : ℕ} (hinit : init ≤ B)
-    (hxs : ∀ x ∈ xs, x ≤ B) : xs.foldl max init ≤ B := by
-  induction xs generalizing init with
-  | nil => exact hinit
-  | cons a as ih =>
-    exact ih (max_le hinit (hxs a (List.mem_cons_self ..))) fun x hx =>
-      hxs x (List.mem_cons_of_mem _ hx)
-
 /-- Maximum unary-clamped variable-group dimension `min (2 * n') |V_{t,g}|` across `g < r_u` at a
 fixed interpolation node `t`. -/
 def maxGroupDim (n' r_u : ℕ) (vGroups_t : List (List ℕ)) : ℕ :=
@@ -608,51 +586,6 @@ private theorem maxGroupDim_le_maxAllGroupDim {n' Q_u r_u t : ℕ}
     maxGroupDim n' r_u (varGroups.getD t []) ≤ maxAllGroupDim n' Q_u r_u varGroups :=
   le_foldl_max_of_mem (List.mem_map.mpr ⟨t, List.mem_range.mpr ht, rfl⟩)
 
-private def HasPolySpace {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool}
-    {f : α → β} (c : NativeCertificate f ei eo) : Prop :=
-  PolyBounded (fun a => (ei a).length) c.space
-
-private theorem polyBounded_length_of_hasPolySpace {α β : Type} {ei : α ↪ List Bool}
-    {eo : β ↪ List Bool} {f : α → β} {c : NativeCertificate f ei eo} (hc : HasPolySpace c) :
-    PolyBounded (fun a => (ei a).length) (fun a => (eo (f a)).length) := by
-  obtain ⟨c₀, d₀, hs⟩ := hc.exists_le
-  obtain ⟨k, _, hl⟩ := c.computes
-  refine .of_forall_le (k * (c₀ + 1)) d₀ fun a => (hl a).trans ?_
-  have h1 : 1 ≤ ((ei a).length + 1) ^ d₀ := Nat.one_le_pow _ _ (Nat.succ_pos _)
-  have := hs a; nlinarith
-
-private theorem hasPolySpace_comp {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
-    {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} {d : NativeCertificate g em eo}
-    {c : NativeCertificate f ei em} (hd : HasPolySpace d) (hc : HasPolySpace c) :
-    HasPolySpace (d.comp c) := hc.add (hd.comp (polyBounded_length_of_hasPolySpace hc))
-
-private theorem hasPolySpace_prod {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
-    {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} {c : NativeCertificate f ei em}
-    {d : NativeCertificate g ei eo} (hc : HasPolySpace c) (hd : HasPolySpace d) :
-    HasPolySpace (c.prod d) := hc.add hd
-
-private theorem exists_natAbs_rowEntry_le_two_pow {ι γ : Type} {sz : ι → ℕ}
-    {encΓ : γ ↪ List Bool} {f : γ → JetRows} {L : ι → ℕ}
-    (hf : PolyBounded (fun y => (encΓ y).length) (fun y => (encJet (f y)).length))
-    (hL : PolyBounded sz L) :
-    ∃ M : ι → ℕ, PolyBounded sz M ∧
-      ∀ x y, (encΓ y).length ≤ L x → ∀ j u, (rowEntry (f y) j u).natAbs ≤ 2 ^ M x := by
-  obtain ⟨c, d, hle⟩ := hf.exists_le
-  refine ⟨fun x => c * (L x + 1) ^ d, NativeCertificate.polyBounded_pow_of_polyBounded hL c d,
-    fun x y hy j u => ?_⟩
-  have hout := (hle y).trans
-    (Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hy 1) d))
-  exact (Nat.size_le.mp
-    ((CommonCountingAccum.size_natAbs_rowEntry_le_length_encJetRows (f y) j u).trans hout)).le
-
-private theorem foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
-    (par : π) (xs : List ι) (init : α) :
-    xs.foldl (fun pa i => (pa.1, step pa.1 pa.2 i)) (par, init) =
-      (par, xs.foldl (step par) init) := by
-  induction xs generalizing init with
-  | nil => rfl
-  | cons _ _ ih => exact ih _
-
 private theorem foldl_optAddJet_spec (J ℓ j M : ℕ) (f : ℕ → Option JetRows)
     (hf : ∀ i < j, ∀ y, f i = some y → ∀ j' < J, ∀ u' < ℓ, (rowEntry y j' u').natAbs ≤ M) :
     let res := (List.range j).foldl
@@ -688,52 +621,6 @@ private theorem length_encJetRows_foldl_optAddJet_le {J ℓ j N M : ℕ} {f : 
     (Nat.size_le_size ((hbd j' hj' u' hu').trans (Nat.mul_le_mul_right M hj))).trans
       (Nat.size_mul_le N M)
 
-private theorem computableInO_snd_indexFold {ι β : Type} {encIn : ι ↪ List Bool}
-    {encB : β ↪ List Bool} {count : ι → ℕ} {initial : ι → β} {body : ℕ × β → β}
-    (cn : NativeCertificate count encIn encNat) (ci : NativeCertificate initial encIn encB)
-    (cb : NativeCertificate body (encPair encNat encB) encB)
-    (hcn : cn.IsPolynomial) (hci : ci.IsPolynomial) (hcb : HasPolySpace cb)
-    {B : ι → ℕ} (hB_pb : PolyBounded (fun x => (encIn x).length) B)
-    (hB : ∀ x j, j ≤ count x → (encB (IndexFold.run body j (initial x)).2).length ≤ B x)
-    (R P_cb : ι → ℕ) (hP_cb : PolyBounded (fun x => (encIn x).length) P_cb)
-    (hR : ∀ x j, j ≤ count x →
-      (encPair encNat encB (IndexFold.run body j (initial x))).length ≤
-        2 * (encNat (count x)).length + 1 + B x →
-      cb.time (IndexFold.run body j (initial x)) ≤ R x + P_cb x) :
-    ∃ P : ι → ℕ, PolyBounded (fun x => (encIn x).length) P ∧
-      ComputableInO (fun x => (IndexFold.run body (count x) (initial x)).2) encIn encB
-        (fun x => (count x + 1) * (R x + P x)) P := by
-  have hcnt_pb := (cn.polyTime hcn).polyBounded_length
-  let S_st : ι → ℕ := fun x => 2 * (encNat (count x)).length + 1 + B x
-  have hSst_pb := (((PolyBounded.const 2).mul hcnt_pb).add (.const 1)).add hB_pb
-  obtain ⟨cs, ds, hcs⟩ := hcb.exists_le
-  let Q : ι → ℕ := fun x => cs * (S_st x + 1) ^ ds
-  have hQ_pb := NativeCertificate.polyBounded_pow_of_polyBounded hSst_pb cs ds
-  have hsq_pb := NativeCertificate.polyBounded_pow_of_polyBounded hcnt_pb 1 2
-  have hloop := IndexFold.computableInO cn ci cb (fun x => R x + P_cb x) Q B
-    (fun x j hj => hR x j hj (IndexFold.length_run_le body (initial x) hj (hB x j hj)))
-    (fun x j hj => (hcs _).trans (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left
-      (Nat.add_le_add_right (IndexFold.length_run_le body (initial x) hj (hB x j hj)) 1) ds))) hB
-  let cLoop : NativeCertificate (fun x => IndexFold.run body (count x) (initial x))
-      encIn (encPair encNat encB) := ⟨_, _, hloop⟩
-  let P : ι → ℕ := fun x => cn.time x + cn.space x + (encIn x).length + ci.time x + ci.space x +
-    2 * S_st x + 2 * (1 * ((encNat (count x)).length + 1) ^ 2) + P_cb x + Q x +
-    2 * (encNat (count x)).length + 1
-  have hP_pb : PolyBounded (fun x => (encIn x).length) P :=
-    ((((((((((hcn.1.add hcn.2).add .self).add hci.1).add hci.2).add
-      ((PolyBounded.const 2).mul hSst_pb)).add ((PolyBounded.const 2).mul hsq_pb)).add
-      hP_cb).add hQ_pb).add ((PolyBounded.const 2).mul hcnt_pb)).add (.const 1))
-  refine ⟨P, hP_pb, (NativeCertificate.snd cLoop).computes.mono_le (fun x => ?_) (fun x => ?_)⟩
-  · have hinit_le := Nat.le_mul_of_pos_left (cn.time x + ((encIn x).length + ci.time x))
-      (Nat.succ_pos (count x))
-    have hstep_le : (S_st x + ((encNat (count x)).length + 1) ^ 2 + (R x + P_cb x)) +
-        S_st x + ((encNat (count x)).length + 1) ^ 2 ≤
-        R x + (2 * S_st x + 2 * (1 * ((encNat (count x)).length + 1) ^ 2) + P_cb x) := by omega
-    have hmul_le := Nat.add_le_add hinit_le (Nat.mul_le_mul_left (count x + 1) hstep_le)
-    rw [← Nat.mul_add] at hmul_le
-    exact hmul_le.trans (Nat.mul_le_mul_left (count x + 1) (by dsimp only [P]; omega))
-  · dsimp only [NativeCertificate.snd_space, cLoop, S_st, P]; omega
-
 private def mapRangeStep {γ δ : Type} (f : γ × ℕ → δ)
     (p : ℕ × ((ℕ × γ) × List δ)) : (ℕ × γ) × List δ :=
   if decide (p.1 < p.2.1.1) then (p.2.1, p.2.2 ++ [f (p.2.1.2, min p.2.1.1 p.1)]) else p.2

Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean

@@ -219,17 +219,21 @@ def branchNeutralScope (n' : ℕ) (eqs' : List (List (List ℕ))) :
     Fin eqs'.length ⊕ Fin n' → Finset (Fin n') :=
   withNeutralScope fun i => equationScope (HeavyBranchFold.toFinsetEquation n' eqs'[i])
 
-private theorem foldl_max_le_iff {l : List ℕ} {init B : ℕ} :
+theorem foldl_max_le_iff {l : List ℕ} {init B : ℕ} :
     l.foldl max init ≤ B ↔ init ≤ B ∧ ∀ x ∈ l, x ≤ B := by
   induction l generalizing init with
   | nil => simp only [List.foldl_nil, List.not_mem_nil, IsEmpty.forall_iff, implies_true, and_true]
   | cons a as ih =>
     simp only [List.foldl_cons, ih, Nat.max_le, List.mem_cons, forall_eq_or_imp, and_assoc]
 
-private theorem le_foldl_max_init (init : ℕ) (l : List ℕ) : init ≤ l.foldl max init :=
+theorem foldl_max_le {l : List ℕ} {init B : ℕ} (hinit : init ≤ B) (hl : ∀ x ∈ l, x ≤ B) :
+    l.foldl max init ≤ B :=
+  foldl_max_le_iff.mpr ⟨hinit, hl⟩
+
+theorem le_foldl_max_init (init : ℕ) (l : List ℕ) : init ≤ l.foldl max init :=
   (foldl_max_le_iff.mp le_rfl).1
 
-private theorem le_foldl_max_of_mem {init : ℕ} {l : List ℕ} {x : ℕ} (hx : x ∈ l) :
+theorem le_foldl_max_of_mem {init : ℕ} {l : List ℕ} {x : ℕ} (hx : x ∈ l) :
     x ≤ l.foldl max init := (foldl_max_le_iff.mp le_rfl).2 x hx
 
 theorem checkVarsLt_eq_true_iff {n : ℕ} {sys : List (List (List ℕ))} :

Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean

@@ -538,13 +538,6 @@ private theorem scopeWidthOn_le_mul (N k maxTerms : ℕ) (eq : List (List ℕ))
     _ ≤ eq.length * k := List.length_flatMap_le hdeg
     _ ≤ maxTerms * k := Nat.mul_le_mul_right k hlen
 
-private theorem foldl_max_le_of_forall {l : List ℕ} {init B : ℕ} (hi : init ≤ B)
-    (hl : ∀ x ∈ l, x ≤ B) : l.foldl max init ≤ B := by
-  induction l generalizing init with
-  | nil => exact hi
-  | cons a as ih =>
-    exact ih (max_le hi (hl a List.mem_cons_self)) fun x hx => hl x (List.mem_cons_of_mem a hx)
-
 private theorem compiled_system_incidence_bounds (k C_B β_B : ℕ) :
     ∃ C_inc : ℕ, 12 ≤ C_inc ∧ ∀ {N m B : ℕ} {sys : List (List (List ℕ))},
       2 ≤ N → B ≤ C_B * Nat.clog 2 N ^ β_B → m ≤ B * N →
@@ -573,7 +566,7 @@ private theorem compiled_system_incidence_bounds (k C_B β_B : ℕ) :
     Nat.pow_le_pow_right hlam1 (by omega)
   have hw_le : branchMaxFactorWidth N sys ≤ C_inc * lam ^ (2 * β_B + 4) := by
     unfold branchMaxFactorWidth
-    refine foldl_max_le_of_forall (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_
+    refine foldl_max_le (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_
     obtain ⟨eq, heq, rfl⟩ := List.mem_map.mp hw
     have h1 := (hsc_all eq heq).trans (hT_le.trans (Nat.mul_le_mul_left _ hpow_step))
     dsimp only [C_inc]; nlinarith

Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean

@@ -70,66 +70,6 @@ namespace Cslib.Logic.PL.CNF.GreedyContext
 open Finset Cslib.BitString Cslib.GenericRAM Turing.MultiTapeTM
 variable {C : Type} {encC : C ↪ List Bool}
 
-private def candRowOfState (s : ℕ × SelectBestAcc) : List Bool :=
-  materializeTestRow s.2.1.1 (decodeTestTuple s.2.1.1 s.2.1.2 s.1)
-
-private theorem computableInPolyTime_candRowOfState :
-    ComputableInPolyTime candRowOfState (encPair encNat encSelectBestAcc) encBits := by
-  unfold candRowOfState encSelectBestAcc
-  let encRest := encPair (encList encBits) (encOption (encPair encBits encNat))
-  let encAcc := encPair (encPair encUnary encUnary) encRest
-  have hj := ComputableInPolyTime.fst encNat encAcc
-  have hmP := (ComputableInPolyTime.fst (encPair encUnary encUnary) encRest).comp
-    (ComputableInPolyTime.snd encNat encAcc)
-  have hm := (ComputableInPolyTime.fst encUnary encUnary).comp hmP
-  have hP := (ComputableInPolyTime.snd encUnary encUnary).comp hmP
-  exact computableInPolyTime_materializeTestRow' hm (computableInPolyTime_decodeTestTuple' hm hP hj)
-
-private def augCandidateRows (s : ℕ × SelectBestAcc) : List (List Bool) :=
-  s.2.2.1 ++ [candRowOfState s]
-
-private theorem computableInPolyTime_augCandidateRows :
-    ComputableInPolyTime augCandidateRows (encPair encNat encSelectBestAcc) (encList encBits) := by
-  unfold augCandidateRows
-  have hcand := computableInPolyTime_candRowOfState
-  unfold encSelectBestAcc at hcand ⊢
-  let encRest := encPair (encList encBits) (encOption (encPair encBits encNat))
-  have hrows := (ComputableInPolyTime.fst (encList encBits) _).comp
-    ((ComputableInPolyTime.snd (encPair encUnary encUnary) encRest).comp
-      (ComputableInPolyTime.snd encNat (encPair (encPair encUnary encUnary) encRest)))
-  exact (ComputableInPolyTime.snoc encBits).comp (hrows.prod hcand)
-
-private def finishSelectBestStep (p : (ℕ × SelectBestAcc) × ℕ) : SelectBestAcc :=
-  let candRow := candRowOfState p.1
-  let nextBest := p.1.2.2.2.elim (some (candRow, p.2)) fun best =>
-    if decide (p.2 < best.2) then some (candRow, p.2) else some best
-  (p.1.2.1, (p.1.2.2.1, nextBest))
-
-private theorem computableInPolyTime_finishSelectBestStep :
-    ComputableInPolyTime finishSelectBestStep
-      (encPair (encPair encNat encSelectBestAcc) encNat) encSelectBestAcc := by
-  unfold finishSelectBestStep
-  have hcand0 := computableInPolyTime_candRowOfState
-  unfold encSelectBestAcc at hcand0 ⊢
-  let eBest := encPair encBits encNat; let encRest := encPair (encList encBits) (encOption eBest)
-  let encAcc := encPair (encPair encUnary encUnary) encRest
-  let encIn := encPair (encPair encNat encAcc) encNat
-  have hs := ComputableInPolyTime.fst (encPair encNat encAcc) encNat
-  have hval := ComputableInPolyTime.snd (encPair encNat encAcc) encNat
-  have hacc := (ComputableInPolyTime.snd encNat encAcc).comp hs
-  have hmP := (ComputableInPolyTime.fst (encPair encUnary encUnary) encRest).comp hacc
-  have hrest := (ComputableInPolyTime.snd (encPair encUnary encUnary) encRest).comp hacc
-  have hrows := (ComputableInPolyTime.fst (encList encBits) (encOption eBest)).comp hrest
-  have hbestOpt := (ComputableInPolyTime.snd (encList encBits) (encOption eBest)).comp hrest
-  have hsomeCand := (ComputableInPolyTime.optionSome eBest).comp ((hcand0.comp hs).prod hval)
-  refine hmP.prod (hrows.prod
-    (ComputableInPolyTime.optionElimWithInput hbestOpt hsomeCand ?_))
-  have hq_in := ComputableInPolyTime.fst encIn eBest
-  have hq_best := ComputableInPolyTime.snd encIn eBest
-  exact (ComputableInPolyTime.binary_lt' (hval.comp hq_in)
-    ((ComputableInPolyTime.snd encBits encNat).comp hq_best)).ite (hsomeCand.comp hq_in)
-      ((ComputableInPolyTime.optionSome eBest).comp hq_best)
-
 private def augment (s : ℕ × C × SelectBestAcc) : C × List (List Bool) :=
   (s.2.1, augCandidateRows (s.1, s.2.2))
 
@@ -316,21 +256,6 @@ theorem count_greedy_eq_card_sat {V : Type*} [Fintype V] [DecidableEq V]
       #{σ : V → Bool | φ.eval σ = true} :=
   countSys_greedyParityRows_eq_card_sat φ hn hP hinit_len hcount hinit
 
-private theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) :
-    ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ ∀ a, u a ≤ p (size a) := by
-  obtain ⟨c, d, h⟩ := hu.exists_le
-  exact ⟨fun n => c * (n + 1) ^ d, by fun_prop,
-    fun _ _ hxy => Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) d), h⟩
-
-private theorem exists_mono_poly_cert {α β : Type} {f : α → β}
-    {ei : α ↪ List Bool} {eo : β ↪ List Bool} (hf : ComputableInPolyTime f ei eo) :
-    ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧
-      ∀ a, (NativeCertificate.ofPolyTime hf).time a ≤ p (ei a).length ∧
-        (NativeCertificate.ofPolyTime hf).space a ≤ p (ei a).length := by
-  have hc := NativeCertificate.ofPolyTime_isPolynomial hf
-  obtain ⟨p, hp, hmono, hle⟩ := exists_mono_poly (hc.1.add hc.2)
-  exact ⟨p, hp, hmono, fun a => ⟨by have := hle a; omega, by have := hle a; omega⟩⟩
-
 private theorem input_le (c : C) (m P : ℕ) (rows : List (List Bool)) :
     (encC c).length ≤ (encInput encC (c, m, P, rows)).length ∧
     m ≤ (encInput encC (c, m, P, rows)).length ∧