Add deduplicate, derun functions and Grouped property for lists (#1081)

Author: uzytkownik

CHANGELOG.md

@@ -294,6 +294,8 @@ Other major additions
   Codata.Cowriter.Bisimilarity
 
   Data.Erased
+  Data.List.Relation.Unary.Grouped
+  Data.List.Relation.Unary.Grouped.Properties
   Data.Product.Relation.Unary.All
   Data.Refinement
   Data.Refinement.Relation.Unary.All
@@ -603,6 +605,12 @@ Other minor additions
   map-just    : ma ≡ just a → map f ma ≡ just (f a)
   ```
 
+* Added new functions to `Data.List`:
+  ``agda
+  derun : B.Decidable R → List A → List A
+  deduplicate : Decidable _R_ → List A → List A
+  ```
+
 * Added new proofs to `Data.List.Relation.Binary.Equality.Setoid`:
   ```agda
   Any-resp-≋      : P Respects _≈_ → (Any P) Respects _≋_
@@ -643,13 +651,49 @@ Other minor additions
   rectangleᶜ : Char → Char → Vec String n → Vec String n
   ```
 
+* Added new proofs to `Data.List.Membership.Propositional.Properties`:
+  ```agda
+  ∈-derun⁺ : z ∈ xs → z ∈ derun R? xs
+  ∈-deduplicate⁺ : z ∈ xs → z ∈ deduplicate _≟_ xs
+  ∈-derun⁻ : z ∈ derun R? xs → z ∈ xs
+  ∈-deduplicate⁻ : z ∈ deduplicate R? xs → z ∈ xs
+  ```
+
+* Added new proofs to `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  ∈-derun⁺ : _≈_ Respectsʳ R → z ∈ xs → z ∈ derun R? xs
+  ∈-deduplicate⁺ : _≈_ Respectsʳ (flip R) → z ∈ xs → z ∈ deduplicate R? xs
+  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
+  ∈-deduplicate⁻ : z ∈ deduplicate R? xs → z ∈ xs
+  ```
+
 * Added new proofs to `Data.List.Relation.Binary.Pointwise`:
   ```agda
   Any-resp-Pointwise      : P Respects _∼_ → (Any P) Respects (Pointwise _∼_)
   All-resp-Pointwise      : P Respects _∼_ → (All P) Respects (Pointwise _∼_)
   AllPairs-resp-Pointwise : R Respects₂ _∼_ → (AllPairs R) Respects (Pointwise _∼_)
   ```
 
+* Added new proofs to `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  derun⁺ : All P xs → All P (derun Q? xs)
+  deduplicate⁺ : All P xs → All P (deduplicate Q? xs)
+  filter⁻ : All Q (filter P? xs) → All Q (filter (¬? ∘ P?) xs) → All Q xs
+  derun⁻ : All P (derun Q? xs) → All P xs
+  deduplicate⁻ : All P (deduplicate Q? xs) → All P xs
+  ```
+
+* Added new proofs to `Data.List.Relation.Unary.Any.Properties`:
+  ```agda
+  lookup-result : (p : Any P xs) → P (lookup p)
+  filter⁺ : (p : Any P xs) → Any P (filter Q? xs) ⊎ ¬ Q (Any.lookup p)
+  derun⁺ : P Respects Q → Any P xs → Any P (derun Q? xs)
+  deduplicate⁺ : P Respects (flip Q) → Any P xs → Any P (deduplicate Q? xs)
+  filter⁻ : Any P (filter Q? xs) → Any P xs
+  derun⁻ : Any P (derun Q? xs) → Any P xs
+  deduplicate⁻ : Any P (deduplicate Q? xs) → Any P xs
+  ```
+
 * Added new functions to `Data.List.Relation.Binary.Permutation.Setoid`:
   ```agda
   ↭-prep : xs ↭ ys → x ∷ xs ↭ x ∷ ys
@@ -894,4 +938,4 @@ Version 2.6.1 changes
 * Added new definitions in `Relation.Binary.Core`:
   ```agda
   DecidableEquality A = Decidable {A = A} _≡_
-  ```
+  ```

src/Data/List/Base.agda

@@ -22,8 +22,10 @@ open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (id; _∘_ ; _∘′_; const; flip)
 open import Level using (Level)
 open import Relation.Nullary using (does)
+open import Relation.Nullary.Negation using (¬?)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Unary.Properties using (∁?)
+open import Relation.Binary as B using (Rel)
 
 private
   variable
@@ -292,6 +294,17 @@ span P? (x ∷ xs) with does (P? x)
 break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
 break P? = span (∁? P?)
 
+derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A
+derun R? [] = []
+derun R? (x ∷ []) = x ∷ []
+derun R? (x ∷ y ∷ xs) with does (R? x y) | derun R? (y ∷ xs)
+... | true  | ys = ys
+... | false | ys = x ∷ ys
+
+deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A
+deduplicate R? [] = []
+deduplicate R? (x ∷ xs) = x ∷ filter (¬? ∘ R? x) (deduplicate R? xs)
+
 ------------------------------------------------------------------------
 -- Actions on single elements
 

src/Data/List/Membership/Propositional/Properties.agda

@@ -34,13 +34,13 @@ open import Function.Inverse as Inv using (_↔_; module Inverse)
 import Function.Related as Related
 open import Function.Related.TypeIsomorphisms
 open import Level using (Level)
-open import Relation.Binary hiding (Decidable)
+open import Relation.Binary as B hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Unary using (_⟨×⟩_; Decidable)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; Dec; does; yes; no)
+open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
 open import Relation.Nullary.Negation
 
 private
@@ -179,6 +179,25 @@ module _ {p} {P : A → Set p} (P? : Decidable P) where
   ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
   ∈-filter⁻ = Membershipₛ.∈-filter⁻ (P.setoid A) P? (P.subst P)
 
+------------------------------------------------------------------------
+-- derun and deduplicate
+
+module _ {r} {R : Rel A r} (R? : B.Decidable R) where
+
+  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
+  ∈-derun⁻ xs z∈derun[R,xs] = Membershipₛ.∈-derun⁻ (P.setoid A) R? xs z∈derun[R,xs]
+
+  ∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
+  ∈-deduplicate⁻ xs z∈dedup[R,xs] = Membershipₛ.∈-deduplicate⁻ (P.setoid A) R? xs z∈dedup[R,xs]
+
+module _ (_≈?_ : B.Decidable {A = A} _≡_) where
+
+  ∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs
+  ∈-derun⁺ z∈xs = Membershipₛ.∈-derun⁺ (P.setoid A) _≈?_ (flip trans) z∈xs
+
+  ∈-deduplicate⁺ : ∀ {xs z} → z ∈ xs → z ∈ deduplicate _≈?_ xs
+  ∈-deduplicate⁺ z∈xs = Membershipₛ.∈-deduplicate⁺ (P.setoid A) _≈?_ (λ c≡b a≡b → trans a≡b (sym c≡b)) z∈xs
+
 ------------------------------------------------------------------------
 -- _>>=_
 

src/Data/List/Membership/Setoid/Properties.agda

@@ -20,15 +20,15 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 open import Data.Nat.Base using (suc; z≤n; s≤s; _≤_; _<_)
 open import Data.Nat.Properties using (≤-trans; n≤1+n)
-open import Data.Product as Prod using (∃; _×_; _,_ ; ∃₂)
+open import Data.Product as Prod using (∃; _×_; _,_ ; ∃₂; proj₁)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function using (_$_; flip; _∘_; id)
 open import Relation.Binary as B hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Unary as U using (Decidable; Pred)
+open import Relation.Nullary using (¬_; does; _because_; yes; no)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; does; _because_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation using (¬?; contradiction)
 open Setoid using (Carrier)
 
 ------------------------------------------------------------------------
@@ -243,6 +243,26 @@ module _ {c ℓ p} (S : Setoid c ℓ) {P : Pred (Carrier S) p}
   ...   | here  v≈x   = here v≈x , resp (sym v≈x) (invert [Px])
   ...   | there v∈fxs = Prod.map there id (∈-filter⁻ v∈fxs)
 
+------------------------------------------------------------------------
+-- derun and deduplicate
+
+module _ {c ℓ r} (S : Setoid c ℓ) {R : Rel (Carrier S) r} (R? : B.Decidable R) where
+
+  open Setoid S using (_≈_)
+  open Membership S using (_∈_)
+
+  ∈-derun⁺ : _≈_ Respectsʳ R → ∀ {xs z} → z ∈ xs → z ∈ derun R? xs
+  ∈-derun⁺ ≈-resp-R z∈xs = Any.derun⁺ R? ≈-resp-R z∈xs
+
+  ∈-deduplicate⁺ : _≈_ Respectsʳ (flip R) → ∀ {xs z} → z ∈ xs → z ∈ deduplicate R? xs
+  ∈-deduplicate⁺ ≈-resp-R z∈xs = Any.deduplicate⁺ R? ≈-resp-R z∈xs
+
+  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
+  ∈-derun⁻ xs z∈derun[R,xs] = Any.derun⁻ R? z∈derun[R,xs]
+
+  ∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
+  ∈-deduplicate⁻ xs z∈dedup[R,xs] = Any.deduplicate⁻ R? z∈dedup[R,xs]
+
 ------------------------------------------------------------------------
 -- length
 

src/Data/List/Properties.agda

@@ -15,7 +15,7 @@ open import Algebra.Bundles
 open import Algebra.Definitions as AlgebraicDefinitions using (Involutive)
 import Algebra.Structures as AlgebraicStructures
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
-open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
+open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁)
 open import Data.List.Base as List
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
@@ -30,9 +30,10 @@ open import Level using (Level)
 open import Relation.Binary as B using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P hiding ([_])
+open import Relation.Binary as B using (Rel)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation using (contradiction; ¬?)
 open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋)
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Unary using (Pred; Decidable; ∁)
@@ -752,6 +753,38 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | true  = cong (x ∷_) (filter-++ xs ys)
   ... | false = filter-++ xs ys
 
+------------------------------------------------------------------------
+-- derun and deduplicate
+
+module _ {R : Rel A p} (R? : B.Decidable R) where
+
+  length-derun : ∀ xs → length (derun R? xs) ≤ length xs
+  length-derun [] = ≤-refl
+  length-derun (x ∷ []) = ≤-refl
+  length-derun (x ∷ y ∷ xs) with does (R? x y) | length-derun (y ∷ xs)
+  ... | true  | r = ≤-step r
+  ... | false | r = s≤s r
+
+  length-deduplicate : ∀ xs → length (deduplicate R? xs) ≤ length xs
+  length-deduplicate [] = z≤n
+  length-deduplicate (x ∷ xs) = ≤-begin
+    1 + length (filter (¬? ∘ R? x) r) ≤⟨ s≤s (length-filter (¬? ∘ R? x) r) ⟩
+    1 + length r                      ≤⟨ s≤s (length-deduplicate xs) ⟩
+    1 + length xs                     ≤-∎
+    where
+    open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)
+    r = deduplicate R? xs
+
+  derun-reject : ∀ {x y} xs → R x y → derun R? (x ∷ y ∷ xs) ≡ derun R? (y ∷ xs)
+  derun-reject {x} {y} xs Rxy with R? x y
+  ... | yes _    = refl
+  ... | no  ¬Rxy = contradiction Rxy ¬Rxy
+
+  derun-accept : ∀ {x y} xs → ¬ R x y → derun R? (x ∷ y ∷ xs) ≡ x ∷ derun R? (y ∷ xs)
+  derun-accept {x} {y} xs ¬Rxy with R? x y
+  ... | yes Rxy = contradiction Rxy ¬Rxy
+  ... | no  _   = refl
+
 ------------------------------------------------------------------------
 -- partition
 

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -15,7 +15,7 @@ open import Category.Monad
 open import Data.Bool.Base using (Bool; true; false; T)
 open import Data.List.Base
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.List.Relation.Unary.Any.Properties
+open import Data.List.Relation.Unary.Any.Properties hiding (filter⁺)
 open import Data.List.Categorical
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties

src/Data/List/Relation/Unary/All/Properties.agda

@@ -16,7 +16,7 @@ open import Data.Fin.Base using (Fin) renaming (zero to fzero; suc to fsuc)
 open import Data.List.Base as List using
   ( List; []; _∷_; [_]; _∷ʳ_; fromMaybe; null; _++_; concat; map; mapMaybe
   ; inits; tails; drop; take; applyUpTo; applyDownFrom; replicate; tabulate
-  ; filter; zipWith; all
+  ; filter; zipWith; all; derun; deduplicate
   )
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
@@ -40,17 +40,18 @@ open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
 open import Function.Inverse using (_↔_; inverse)
 open import Function.Surjection using (_↠_; surjection)
 open import Level using (Level)
-open import Relation.Binary using (REL; Setoid; _Respects_)
+open import Relation.Binary as B using (REL; Setoid; _Respects_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; cong₂; _≗_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
+open import Relation.Nullary.Negation using (¬?; contradiction; decidable-stable)
 open import Relation.Unary
   using (Decidable; Pred; Universal) renaming (_⊆_ to _⋐_)
 
 private
   variable
-    a b c p q ℓ : Level
+    a b c p q r ℓ : Level
     A : Set a
     B : Set b
     C : Set c
@@ -505,6 +506,48 @@ module _ {P : A → Set p} {Q : A → Set q} (P? : Decidable P) where
   ... | false = filter⁺ Qxs
   ... | true  = Qx ∷ filter⁺ Qxs
 
+  filter⁻ : ∀ {xs} → All Q (filter P? xs) → All Q (filter (¬? ∘ P?) xs) → All Q xs
+  filter⁻ {[]}         []          []                           = []
+  filter⁻ {x ∷ xs}       all⁺        all⁻ with P? x  | ¬? (P? x)
+  filter⁻ {x ∷ xs}       all⁺        all⁻  | yes  Px | yes  ¬Px = contradiction Px ¬Px
+  filter⁻ {x ∷ xs} (qx ∷ all⁺)       all⁻  | yes  Px | no  ¬¬Px = qx ∷ filter⁻ all⁺ all⁻
+  filter⁻ {x ∷ xs}       all⁺  (qx ∷ all⁻) | no    _ | yes  ¬Px = qx ∷ filter⁻ all⁺ all⁻
+  filter⁻ {x ∷ xs}       all⁺        all⁻  | no  ¬Px | no  ¬¬Px = contradiction ¬Px ¬¬Px
+
+------------------------------------------------------------------------
+-- derun and deduplicate
+
+module _ {P : A → Set p} {R : A → A → Set q} (R? : B.Decidable R) where
+
+  derun⁺ : ∀ {xs} → All P xs → All P (derun R? xs)
+  derun⁺ {[]} [] = []
+  derun⁺ {x ∷ []} (px ∷ []) = px ∷ []
+  derun⁺ {x ∷ y ∷ xs} (px ∷ all[P,y∷xs]) with does (R? x y)
+  ... | false = px ∷ derun⁺ all[P,y∷xs]
+  ... | true  = derun⁺ all[P,y∷xs]
+
+  deduplicate⁺ : ∀ {xs} → All P xs → All P (deduplicate R? xs)
+  deduplicate⁺ [] = []
+  deduplicate⁺ {x ∷ _} (px ∷ all[P,xs]) = px ∷ filter⁺ (¬? ∘ R? x) (deduplicate⁺ all[P,xs])
+
+  derun⁻ : P B.Respects (flip R) → ∀ xs → All P (derun R? xs) → All P xs
+  derun⁻ P-resp-R []       []          = []
+  derun⁻ P-resp-R (x ∷ xs) all[P,x∷xs] = aux x xs all[P,x∷xs] where
+    aux : ∀ x xs → All P (derun R? (x ∷ xs)) → All P (x ∷ xs)
+    aux x []       (px ∷ []) = px ∷ []
+    aux x (y ∷ xs) all[P,x∷y∷xs] with R? x y
+    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy with aux y xs all[P,y∷xs]
+    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy | r@(py ∷ _) = P-resp-R Rxy py ∷ r
+    aux x (y ∷ xs) (px ∷ all[P,y∷xs]) | no _ = px ∷ aux y xs all[P,y∷xs]
+
+  module _ (P-resp-R : P B.Respects R) where
+
+    deduplicate⁻ : ∀ xs → All P (deduplicate R? xs) → All P xs
+    deduplicate⁻ [] [] = []
+    deduplicate⁻ (x ∷ xs) (px ∷ app[P,dedup[xs]]) = px ∷ deduplicate⁻ xs (filter⁻ (¬? ∘ R? x) app[P,dedup[xs]] (All.tabulate aux)) where
+      aux : ∀ {z} → z ∈ filter (¬? ∘ ¬? ∘ R? x) (deduplicate R? xs) → P z
+      aux {z} z∈filter = P-resp-R (decidable-stable (R? x z) (Prod.proj₂ (∈-filter⁻ (¬? ∘ ¬? ∘ R? x) {z} {deduplicate R? xs} z∈filter))) px
+
 ------------------------------------------------------------------------
 -- zipWith