Add partition-is-foldr to Data.List.Properties (#2505)

* Add partition-is-foldr

* Update src/Data/List/Properties.agda

Co-authored-by: jamesmckinna <[email protected]>

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: carlostome

CHANGELOG.md

@@ -186,6 +186,10 @@ Additions to existing modules
   ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
   concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   filter-≐     : P ≐ Q → filter P? ≗ filter Q?
+
+  partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then Product.map₁ (x ∷_)
+                                                                  else Product.map₂ (x ∷_))
+                                            ([] , [])
   ```
 
 * In `Data.List.Relation.Unary.Any.Properties`:

src/Data/List/Properties.agda

@@ -1294,6 +1294,14 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ...  | true  = Product.map s≤s m≤n⇒m≤1+n ih
   ...  | false = Product.map m≤n⇒m≤1+n s≤s ih
 
+  partition-is-foldr : partition P? ≗ foldr
+    (λ x → if does (P? x) then Product.map₁ (x ∷_) else Product.map₂ (x ∷_))
+    ([] , [])
+  partition-is-foldr [] = refl
+  partition-is-foldr (x ∷ xs) with ih ← partition-is-foldr xs | does (P? x)
+  ... | true =  cong (Product.map₁ (x ∷_)) ih
+  ... | false = cong (Product.map₂ (x ∷_)) ih
+
 ------------------------------------------------------------------------
 -- _ʳ++_