From 2a66ee734e5961602a32beb06d41f896c0eee5c4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 11 Feb 2022 12:12:58 +0000 Subject: [PATCH] sum as an accumulating fold; sum-++ by way of fold-++ --- src/Data/Vec/Base.agda | 5 ++++- src/Data/Vec/Properties.agda | 16 +++++++++++----- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 2554d488db..2e399d1331 100644 --- a/src/Data/Vec/Base.agda +++ b/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 diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index e6d83aef35..f3a925838d 100644 --- a/src/Data/Vec/Properties.agda +++ b/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