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]>
agda · Nov 28, 2024 · 23a00fd · 23a00fd
1 parent f35135d
commit 23a00fd
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/CHANGELOG.md b/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`:

diff --git a/src/Data/List/Properties.agda b/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
+
 ------------------------------------------------------------------------
 -- _ʳ++_