From af77fc9185d4786e907a1451a5725f82220b8dfb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Sun, 24 Nov 2024 11:48:12 +0100 Subject: [PATCH 1/2] Add partition-is-foldr --- 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..81a39692f1 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 + ------------------------------------------------------------------------ -- _ʳ++_ From cce7aed76a9ac7ab756139de7c35fc81c0563cc1 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 10:05:58 +0100 Subject: [PATCH 2/2] Update src/Data/List/Properties.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/List/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 81a39692f1..274b684a8d 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -1294,9 +1294,9 @@ 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 : 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