refactor(List): reuse core maximum bounds in sparse counters

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean

@@ -1341,9 +1341,15 @@ public theorem exists_boundedIncidenceBranchCertificate_time_bound
       simp only [Rat.cast_natCast, Rat.cast_mul, Rat.cast_ofNat,
         ReplacementParams.cast_tauRat] at hrat_r
       exact (Nat.cast_le.mpr hc_le).trans hrat_r
-    · unfold d_max maxAllGroupDim; refine foldl_max_le (Nat.zero_le _) fun x hx => ?_
+    · unfold d_max maxAllGroupDim
+      refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+      simp only [List.mem_cons, forall_eq_or_imp]
+      refine ⟨Nat.zero_le _, fun x hx => ?_⟩
       obtain ⟨t, ht_mem, rfl⟩ := List.mem_map.mp hx; have ht : t < Q := List.mem_range.mp ht_mem
-      unfold maxGroupDim; refine foldl_max_le (Nat.zero_le _) fun y hy => ?_
+      unfold maxGroupDim
+      refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+      simp only [List.mem_cons, forall_eq_or_imp]
+      refine ⟨Nat.zero_le _, fun y hy => ?_⟩
       obtain ⟨g, hg_mem, rfl⟩ := List.mem_map.mp hy; have hg : g < r := List.mem_range.mp hg_mem
       refine (Nat.min_le_right _ _).trans ?_; have hgrp := (href.2.2.1 ⟨t, ht⟩ ⟨g, hg⟩).2.1
       dsimp only [data, mkDesignPair, mkDesignFromScheds, prepScheduleParams,

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean

@@ -1090,7 +1090,8 @@ theorem evalBoundedIncidenceBranch_eq_rootCount {N₀_branch n' : ℕ}
   let P_eq : Fin eqs'.length → Finset (Finset (Fin n')) := fun f =>
     HeavyBranchFold.toFinsetEquation n' eqs'[f]
   have hk_list : ∀ eq ∈ eqs', ∀ m ∈ eq, m.length ≤ k' := fun eq heq m hm =>
-    le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩))
+    List.le_max_of_mem
+      (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩)))
   have hk_fin : ∀ f ∈ (univ : Finset (Fin eqs'.length)), ∀ M ∈ P_eq f, #M ≤ k' := by
     intro f _ M hM
     simp only [P_eq, HeavyBranchFold.toFinsetEquation, List.mem_toFinset, List.mem_map] at hM

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean

@@ -472,7 +472,8 @@ private theorem varIncidence_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : Lis
         ← (List.ofFn_eq_map.symm.trans (List.ofFn_getElem (xs := scopes))), List.countP_map]
     exact List.countP_congr fun i _ => by simp only [Function.comp_apply, Fin.getElem_fin]
   rw [hdeg]
-  exact le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_range.mpr v.isLt))
+  exact List.le_max_of_mem (l := 0 :: (List.range n').map (varDegree · eqs'))
+    (List.mem_cons_of_mem 0 (List.mem_map_of_mem (List.mem_range.mpr v.isLt)))
 
 private theorem card_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : List (List (List ℕ))) :
     let augScopes := withNeutralScopesList (eqs'.map equationVars) n'
@@ -489,7 +490,7 @@ private theorem card_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : List (List
     have hsc := listScopeFamily_map_equationVars n' eqs' ⟨g.1, hg⟩
     change listScopeFamily n' scopes g = _ at hsc
     rw [hsc, card_equationScope_toFinsetEquation, branchMaxFactorWidth]
-    exact le_foldl_max_of_mem (List.mem_map_of_mem (List.getElem_mem hg))
+    exact List.le_max_of_mem (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.getElem_mem hg)))
   · dsimp only [withNeutralScope]
     rw [card_singleton]
     exact one_le_branchMaxFactorWidth n' eqs'

Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean

@@ -579,12 +579,16 @@ def maxAllGroupDim (n' Q_u r_u : ℕ) (varGroups : List (List (List ℕ))) : ℕ
 private theorem min_length_le_maxGroupDim {n' r_u g : ℕ} {vGroups_t : List (List ℕ)}
     (hg : g < r_u) :
     min (2 * n') (vGroups_t.getD g []).length ≤ maxGroupDim n' r_u vGroups_t :=
-  le_foldl_max_of_mem (List.mem_map.mpr ⟨g, List.mem_range.mpr hg, rfl⟩)
+  List.le_max_of_mem
+    (l := 0 :: (List.range r_u).map (fun g => min (2 * n') (vGroups_t.getD g []).length))
+    (List.mem_cons_of_mem _ (List.mem_map.mpr ⟨g, List.mem_range.mpr hg, rfl⟩))
 
 private theorem maxGroupDim_le_maxAllGroupDim {n' Q_u r_u t : ℕ}
     {varGroups : List (List (List ℕ))} (ht : t < Q_u) :
     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⟩)
+  List.le_max_of_mem
+    (l := 0 :: (List.range Q_u).map (fun t => maxGroupDim n' r_u (varGroups.getD t [])))
+    (List.mem_cons_of_mem _ (List.mem_map.mpr ⟨t, List.mem_range.mpr ht, rfl⟩))
 
 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) :

Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean

@@ -219,23 +219,6 @@ def branchNeutralScope (n' : ℕ) (eqs' : List (List (List ℕ))) :
     Fin eqs'.length ⊕ Fin n' → Finset (Fin n') :=
   withNeutralScope fun i => equationScope (HeavyBranchFold.toFinsetEquation n' eqs'[i])
 
-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]
-
-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
-
-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 ℕ))} :
     checkVarsLt n sys = true ↔ ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n := by
   simp only [checkVarsLt, List.all_eq_true, decide_eq_true_eq]
@@ -309,19 +292,22 @@ theorem card_equationScope_toFinsetEquation (n : ℕ) (eq : List (List ℕ)) :
 
 theorem length_mem_le_sysMaxDegree {sys : List (List (List ℕ))} {eq : List (List ℕ)}
     (heq : eq ∈ sys) {m : List ℕ} (hm : m ∈ eq) : m.length ≤ sysMaxDegree sys :=
-  le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩))
+  List.le_max_of_mem
+    (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩)))
 
 theorem sysMaxDegree_le_iff {sys : List (List (List ℕ))} {k : ℕ} :
     sysMaxDegree sys ≤ k ↔ ∀ eq ∈ sys, ∀ m ∈ eq, m.length ≤ k := by
-  simp only [sysMaxDegree, foldl_max_le_iff, Nat.zero_le, true_and, List.mem_map, List.mem_flatten]
+  change (0 :: sys.flatten.map List.length).max (by simp) ≤ k ↔ _
+  simp only [List.max_le_iff, List.mem_cons, forall_eq_or_imp, Nat.zero_le, true_and,
+    List.mem_map, List.mem_flatten]
   exact ⟨fun h eq heq m hm => h m.length ⟨m, ⟨eq, heq, hm⟩, rfl⟩,
     fun h _ ⟨m, ⟨eq, heq, hm⟩, hm_eq⟩ => hm_eq ▸ h eq heq m hm⟩
 
 theorem one_le_branchMaxFactorIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) :
     1 ≤ branchMaxFactorIncidence n' eqs' := Nat.succ_pos _
 
 theorem one_le_branchMaxFactorWidth (n' : ℕ) (eqs' : List (List (List ℕ))) :
-    1 ≤ branchMaxFactorWidth n' eqs' := le_foldl_max_init 1 _
+    1 ≤ branchMaxFactorWidth n' eqs' := List.le_max_of_mem List.mem_cons_self
 
 theorem le_branchAugmentedIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) :
     n' ≤ branchAugmentedIncidence n' eqs' := Nat.le_add_left _ _
@@ -362,22 +348,26 @@ theorem varIncidence_branchNeutralScope_le (n' : ℕ) (eqs' : List (List (List 
       (branchNeutralScope n' eqs') v ≤ _
   rw [← withNeutralFactors_univ, branchNeutralScope, varIncidence_withNeutralFactors,
     varIncidence_toFinsetEquation_eq_varDegree, branchMaxFactorIncidence]
-  exact Nat.succ_le_succ (le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_range.mpr v.isLt)))
+  apply Nat.succ_le_succ
+  exact List.le_max_of_mem (l := 0 :: (List.range n').map (varDegree · eqs'))
+    (List.mem_cons_of_mem 0 (List.mem_map_of_mem (List.mem_range.mpr v.isLt)))
 
 theorem card_branchNeutralScope_le (n' : ℕ) (eqs' : List (List (List ℕ)))
     (f : Fin eqs'.length ⊕ Fin n') :
     #(branchNeutralScope n' eqs' f) ≤ branchMaxFactorWidth n' eqs' :=
   card_withNeutralScope_le (one_le_branchMaxFactorWidth n' eqs')
     (fun i : Fin eqs'.length => (card_equationScope_toFinsetEquation n' eqs'[i]).trans_le
-      (le_foldl_max_of_mem (List.mem_map_of_mem (List.getElem_mem i.isLt)))) f
+      (List.le_max_of_mem
+        (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.getElem_mem i.isLt))))) f
 
 theorem branchAugmentedIncidence_le_mul (n' : ℕ) (eqs' : List (List (List ℕ))) :
     branchAugmentedIncidence n' eqs' ≤ branchMaxFactorIncidence n' eqs' * n' := by
   have hle := totalIncidence_withNeutralFactors_le (I := (univ : Finset (Fin eqs'.length)))
     (scope := fun i => equationScope (HeavyBranchFold.toFinsetEquation n' eqs'[i]))
     (b₀ := ((List.range n').map fun v => varDegree v eqs').foldl max 0)
     (fun v => (varIncidence_toFinsetEquation_eq_varDegree n' eqs' v).trans_le
-      (le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_range.mpr v.isLt))))
+      (List.le_max_of_mem (l := 0 :: (List.range n').map (varDegree · eqs'))
+        (List.mem_cons_of_mem 0 (List.mem_map_of_mem (List.mem_range.mpr v.isLt)))))
   rw [withNeutralFactors_univ, ← branchNeutralScope, Fintype.card_fin,
     ← branchMaxFactorIncidence, totalIncidence] at hle
   rwa [← sum_card_branchNeutralScope]
@@ -511,7 +501,9 @@ private theorem unaryFoldMax (init : ℕ) :
     id' (const init) (by fun_prop) (B := fun l => init + (encList encUnary l).length)
     ((PolyBounded.const init).add .self) (fun l i _ => ?_)
   simp only [encUnary_apply, List.length_replicate]
-  refine foldl_max_le_iff.mpr ⟨Nat.le_add_right _ _, fun x hx => ?_⟩
+  refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+  simp only [List.mem_cons, forall_eq_or_imp]
+  refine ⟨Nat.le_add_right _ _, fun x hx => ?_⟩
   have hsz := SizedListEncoding.length_elem_le (encA := encUnary) (encL := encList encUnary)
     l x (List.mem_of_mem_take hx)
   simp only [encUnary_apply, List.length_replicate] at hsz; omega
@@ -844,17 +836,23 @@ theorem reduced_branch_invariants {N₀_top : ℕ} {inp : SparseSystemInput} {va
   have hS_half := hS_le.trans (Nat.div_le_div_left hs2 (by omega))
   have hvd' := HeavyBranchFold.prepareBranch_reduced_varDegree_le hS_nd hSn
     (fun u hun huS => HeavyBranchFold.varDegree_le_of_not_mem_heavyVarList hun huS) hred
-  have hb' : branchMaxFactorIncidence n' sys' ≤ inp.2.1.2.2 + 1 :=
-    Nat.succ_le_succ (foldl_max_le_iff.mpr ⟨Nat.zero_le _, fun x hx => by
-      obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hx; exact hvd' v (List.mem_range.mp hv)⟩)
-  have hw' : branchMaxFactorWidth n' sys' ≤ branchMaxFactorWidth inp.1 inp.2.2 :=
-    foldl_max_le_iff.mpr ⟨one_le_branchMaxFactorWidth inp.1 inp.2.2, fun x hx => by
-      obtain ⟨eq', heq', rfl⟩ := List.mem_map.mp hx
-      obtain ⟨eq₀, heq₀, _, hsc⟩ :=
-        (HeavyBranchFold.prepareBranch_reduced_length_le hred).2 eq' heq'
-      rw [scopeWidthOn_eq_length_equationVars (hvars' eq' heq')]
-      exact (hsc.trans_eq (scopeWidthOn_eq_length_equationVars (hvars eq₀ heq₀)).symm).trans
-        (le_foldl_max_of_mem (List.mem_map_of_mem heq₀))⟩
+  have hb' : branchMaxFactorIncidence n' sys' ≤ inp.2.1.2.2 + 1 := by
+    apply Nat.succ_le_succ
+    refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+    simp only [List.mem_cons, forall_eq_or_imp]
+    refine ⟨Nat.zero_le _, fun x hx => ?_⟩
+    obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hx
+    exact hvd' v (List.mem_range.mp hv)
+  have hw' : branchMaxFactorWidth n' sys' ≤ branchMaxFactorWidth inp.1 inp.2.2 := by
+    refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+    simp only [List.mem_cons, forall_eq_or_imp]
+    refine ⟨one_le_branchMaxFactorWidth inp.1 inp.2.2, fun x hx => ?_⟩
+    obtain ⟨eq', heq', rfl⟩ := List.mem_map.mp hx
+    obtain ⟨eq₀, heq₀, _, hsc⟩ :=
+      (HeavyBranchFold.prepareBranch_reduced_length_le hred).2 eq' heq'
+    rw [scopeWidthOn_eq_length_equationVars (hvars' eq' heq')]
+    exact (hsc.trans_eq (scopeWidthOn_eq_length_equationVars (hvars eq₀ heq₀)).symm).trans
+      (List.le_max_of_mem (List.mem_cons_of_mem _ (List.mem_map_of_mem heq₀)))
   exact ⟨hn'_eq, by omega, hcan', hvars',
     HeavyBranchFold.prepareBranch_reduced_degree_le hdeg hred, hb', hw'⟩
 
@@ -947,14 +945,19 @@ private theorem le_maxReducedCost (cost : ℕ × List (List (List ℕ)) → ℕ)
     (hred : HeavyBranchFold.prepareBranch inp.1 inp.2.1 (lowBits inp.2.1.length idx) inp.2.2 =
       .reduced n' sys') : cost (n', sys') ≤ maxReducedCost cost inp := by
   unfold maxReducedCost
-  refine le_foldl_max_of_mem (List.mem_map.mpr ⟨idx, List.mem_range.mpr hidx, ?_⟩); rw [hred]
+  refine List.le_max_of_mem
+    (List.mem_cons_of_mem _ (List.mem_map.mpr ⟨idx, List.mem_range.mpr hidx, ?_⟩))
+  rw [hred]
 
 theorem maxReducedCost_le {cost : ℕ × List (List (List ℕ)) → ℕ}
     {inp : HeavyBranchFold.BranchInput} {B : ℕ}
     (hB : ∀ idx < 2 ^ inp.2.1.length, ∀ n' sys',
       HeavyBranchFold.prepareBranch inp.1 inp.2.1 (lowBits inp.2.1.length idx) inp.2.2 =
         .reduced n' sys' → cost (n', sys') ≤ B) : maxReducedCost cost inp ≤ B := by
-  unfold maxReducedCost; refine foldl_max_le_iff.mpr ⟨Nat.zero_le B, fun x hx => ?_⟩
+  unfold maxReducedCost
+  refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+  simp only [List.mem_cons, forall_eq_or_imp]
+  refine ⟨Nat.zero_le B, fun x hx => ?_⟩
   obtain ⟨idx, hidx, rfl⟩ := List.mem_map.mp hx
   cases hout : HeavyBranchFold.prepareBranch inp.1 inp.2.1 (lowBits inp.2.1.length idx) inp.2.2 with
   | contradiction | tautology _ => exact Nat.zero_le B

Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean

@@ -566,7 +566,9 @@ 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 (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_
+    refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+    simp only [List.mem_cons, forall_eq_or_imp]
+    refine ⟨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

ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean

@@ -75,13 +75,6 @@ example :
   simp only [← countSystemExhaustive_eq_rootCount]
   decide +kernel
 
-private theorem foldl_max_le_of_all {B : ℕ} :
-    ∀ (init : ℕ) (l : List ℕ), init ≤ B → (∀ x ∈ l, x ≤ B) → l.foldl max init ≤ B
-  | _, [], hi, _ => hi
-  | init, a :: as, hi, hall =>
-    foldl_max_le_of_all (max init a) as (Nat.max_le.mpr ⟨hi, hall a List.mem_cons_self⟩)
-      fun x hx => hall x (List.mem_cons_of_mem a hx)
-
 /-- Nonvacuous feasible witnesses for `evalBoundedIncidenceBranch_eq_rootCount`: there exists a
 concrete dimension `n' ≥ 20` on which both `(n', [])` and the nonlinear quadratic system
 `(n', [[[0, 1], []]])` pass `checkBranchFeasible 0` and execute the non-fallback branch evaluator
@@ -98,9 +91,13 @@ example : ∃ n' : ℕ, 20 ≤ n' ∧
   have hlam : 2 ≤ Nat.clog 2 N₁ :=
     (show 2 = Nat.clog 2 (2 ^ 2) from (Nat.clog_pow 2 2 Nat.one_lt_two).symm).trans_le
       (Nat.clog_mono_right 2 (by omega))
-  have hb0 : branchMaxFactorIncidence N₁ [] ≤ 2 :=
-    Nat.succ_le_succ (foldl_max_le_of_all 0 _ (Nat.zero_le 1) fun x hx => by
-      obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx; exact Nat.zero_le 1)
+  have hb0 : branchMaxFactorIncidence N₁ [] ≤ 2 := by
+    apply Nat.succ_le_succ
+    refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+    simp only [List.mem_cons, forall_eq_or_imp]
+    refine ⟨Nat.zero_le 1, fun x hx => ?_⟩
+    obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx
+    exact Nat.zero_le 1
   have hfeas0 : checkBranchFeasible 0 (N₁, []) = true :=
     (hth le_rfl (by simp only [List.not_mem_nil, IsEmpty.forall_iff, implies_true])
       (by simp only [List.not_mem_nil, IsEmpty.forall_iff, implies_true])
@@ -109,9 +106,14 @@ example : ∃ n' : ℕ, 20 ≤ n' ∧
     checkVarsLt_eq_true_iff.mp (by decide +kernel)
   have hvars1 : ∀ eq ∈ ([[[0, 1], []]] : List (List (List ℕ))), ∀ m ∈ eq, ∀ v ∈ m, v < N₁ :=
     fun eq heq m hm v hv => (hvars2 eq heq m hm v hv).trans_le (by omega)
-  have hb1 : branchMaxFactorIncidence N₁ [[[0, 1], []]] ≤ 2 :=
-    Nat.succ_le_succ (foldl_max_le_of_all 0 _ (Nat.zero_le 1) fun x hx => by
-      obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx; unfold varDegree; exact List.countP_le_length)
+  have hb1 : branchMaxFactorIncidence N₁ [[[0, 1], []]] ≤ 2 := by
+    apply Nat.succ_le_succ
+    refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_
+    simp only [List.mem_cons, forall_eq_or_imp]
+    refine ⟨Nat.zero_le 1, fun x hx => ?_⟩
+    obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx
+    unfold varDegree
+    exact List.countP_le_length
   have hw1 : branchMaxFactorWidth N₁ [[[0, 1], []]] = 2 := by
     unfold branchMaxFactorWidth
     simp only [List.map_cons, List.map_nil, List.foldl_cons, List.foldl_nil]