sum as an accumulating fold; sum-++ by way of fold-++

src/Data/Vec/Base.agda

@@ -218,8 +218,11 @@ foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs
 
 -- Special folds
 
+fold-sum : ℕ → Vec ℕ n → ℕ
+fold-sum n = foldr′ _+_ n
+
 sum : Vec ℕ n → ℕ
-sum = foldr _ _+_ 0
+sum = fold-sum 0
 
 count : ∀ {P : Pred A p} → Decidable P → Vec A n → ℕ
 count P? []       = zero

src/Data/Vec/Properties.agda

@@ -857,12 +857,18 @@ map-ʳ++ {ys = ys} f xs = begin
 ------------------------------------------------------------------------
 -- sum
 
+sum-fold-sum : ∀ (xs : Vec ℕ m) n → fold-sum n xs ≡ sum xs + n
+sum-fold-sum []       n = refl
+sum-fold-sum (x ∷ xs) n = begin
+  x + fold-sum n xs ≡⟨  cong (x +_) (sum-fold-sum xs n) ⟩
+  x + (sum xs + n)  ≡˘⟨ +-assoc x (sum xs) n ⟩
+  sum (x ∷ xs) + n  ∎
+
 sum-++ : ∀ (xs : Vec ℕ m) → sum (xs ++ ys) ≡ sum xs + sum ys
-sum-++ {_}       []       = refl
-sum-++ {ys = ys} (x ∷ xs) = begin
-  x + sum (xs ++ ys)     ≡⟨  cong (x +_) (sum-++ xs) ⟩
-  x + (sum xs + sum ys)  ≡˘⟨ +-assoc x (sum xs) (sum ys) ⟩
-  sum (x ∷ xs) + sum ys  ∎
+sum-++ {ys = ys} xs = begin
+  sum (xs ++ ys)       ≡⟨  foldr-++ _ _+_ xs ⟩
+  fold-sum (sum ys) xs ≡⟨ sum-fold-sum xs (sum ys) ⟩
+  sum xs + sum ys  ∎
 
 ------------------------------------------------------------------------
 -- replicate