From 23a00fde9fda4b7005c94160f2f8802c0f8e7d56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9?= <2206578+carlostome@users.noreply.github.com> Date: Thu, 28 Nov 2024 21:32:06 +0100 Subject: [PATCH] Add `partition-is-foldr` to `Data.List.Properties` (#2505) * Add partition-is-foldr * Update src/Data/List/Properties.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 4 ++++ src/Data/List/Properties.agda | 8 ++++++++ 2 files changed, 12 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f3e17fa961..a58227662c 100644 --- 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 index ab5aff8904..274b684a8d 100644 --- 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 + ------------------------------------------------------------------------ -- _ʳ++_