Added foldr of permutation of Commutative Monoid

CHANGELOG.md

@@ -3027,3 +3027,8 @@ This is a full list of proofs that have changed form to use irrelevant instance
  ```agda
  <-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
+ ```

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

@@ -13,6 +13,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
@@ -35,6 +36,7 @@ open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (inverse)
 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 as ≡
  using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect)
@@ -473,3 +475,34 @@ 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 ∙ fεxs) S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩
+ x ∙ (y ∙ fεys) S.≈˘⟨ assoc x y fεys ⟩
+ (x ∙ y) ∙ fεys S.≈⟨ ∙-congʳ (comm x y) ⟩
+ (y ∙ x) ∙ fεys S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩
+ (y′ ∙ x′) ∙ fεys S.≈⟨ assoc y′ x′ fεys ⟩
+ y′ ∙ (x′ ∙ fεys) S.∎
+ where
+ fε = foldr _∙_ ε
+ fεxs = fε xs
+ fεys = fε ys
+ foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)