Added foldr of permutation of Commutative Monoid

CHANGELOG.md

@@ -3361,6 +3361,11 @@ This is a full list of proofs that have changed form to use irrelevant instance
  <-weakInduction-startingFrom : P i → (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j
  ```
 
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+ ```agda
+ foldr-commMonoid : xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
+ ```
+
 * Added new module to `Data.Rational.Unnormalised.Properties`
  ```agda
  module ≃-Reasoning = SetoidReasoning ≃-setoid
@@ -3442,4 +3447,4 @@ This is a full list of proofs that have changed form to use irrelevant instance
  b #⟨ b#c ⟩
  c ≈⟨ c≈d ⟩
  d ∎
- ```
+ ```

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -16,6 +16,7 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
  where
 
 open import Algebra
+import Algebra.Properties.CommutativeMonoid as ACM
 open import Data.Bool.Base using (true; false)
 open import Data.List.Base as List hiding (head; tail)
 open import Data.List.Relation.Binary.Pointwise as Pointwise
@@ -36,6 +37,7 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
 open import Function.Base using (_∘_; _⟨_⟩_; flip)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; Decidable)
+import Relation.Binary.Reasoning.Setoid as RelSetoid
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡
  using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_)
@@ -474,3 +476,30 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
 ++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
 ++↭ʳ++ [] ys = ↭-refl
 ++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
+
+------------------------------------------------------------------------
+-- foldr of Commutative Monoid
+
+module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
+ open module CM = IsCommutativeMonoid isCmonoid
+
+ private
+ module S = RelSetoid setoid
+
+ cmonoid : CommutativeMonoid _ _
+ cmonoid = record { isCommutativeMonoid = isCmonoid }
+
+ open ACM cmonoid
+
+ foldr-commMonoid : ∀ {xs ys} → xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
+ foldr-commMonoid (refl []) = CM.refl
+ foldr-commMonoid (refl (x≈y ∷ xs≈ys)) = ∙-cong x≈y (foldr-commMonoid (Permutation.refl xs≈ys))
+ foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys)
+ foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = S.begin
+ x ∙ (y ∙ foldr _∙_ ε xs) S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩
+ x ∙ (y ∙ foldr _∙_ ε ys) S.≈˘⟨ assoc x y (foldr _∙_ ε ys) ⟩
+ (x ∙ y) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (comm x y) ⟩
+ (y ∙ x) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩
+ (y′ ∙ x′) ∙ foldr _∙_ ε ys S.≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩
+ y′ ∙ (x′ ∙ foldr _∙_ ε ys) S.∎
+ foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)