Lists: lemmas about deduplicate

Author: omelkonian

CHANGELOG.md

@@ -98,6 +98,11 @@ New modules
   Data.List.Relation.Unary.All.Properties.Core
   ```
 
+* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
+
+* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
+
 Additions to existing modules
 -----------------------------
 
@@ -142,6 +147,7 @@ Additions to existing modules
   ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
   ∈-concatMap⁺  : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
   ∈-concatMap⁻  : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∈-++          : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
@@ -194,6 +200,24 @@ Additions to existing modules
   []⊆-universal : Universal ([] ⊆_)
   ```
 
+* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
+  ```
+
+* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
+  ```agda
+  dedup-++-↭ : Disjoint xs ys →
+               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
+  ```
+
 * In `Data.Maybe.Properties`:
   ```agda
   maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)

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

@@ -33,7 +33,7 @@ open import Effect.Monad using (RawMonad)
 open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_)
 open import Function.Definitions using (Injective)
 import Function.Related.Propositional as Related
-open import Function.Bundles using (_↔_; _↣_; Injection)
+open import Function.Bundles using (_↔_; _↣_; Injection; _⇔_; mk⇔)
 open import Function.Related.TypeIsomorphisms using (×-comm; ∃∃↔∃∃)
 open import Function.Construct.Identity using (↔-id)
 open import Level using (Level)
@@ -123,6 +123,9 @@ module _ {v : A} where
   ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
   ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A)
 
+  ∈-++ : ∀ {xs ys} → v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ∈-++ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
+
   ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
 

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

@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of disjoint lists (propositional equality)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Disjoint.Propositional.Properties where
+
+open import Level using (Level)
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_)
+open import Data.List.Base
+open import Data.List.Relation.Binary.Disjoint.Propositional
+import Data.List.Relation.Unary.Any as Any
+open import Data.List.Relation.Unary.All as All
+open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
+open import Data.List.Relation.Unary.Any.Properties using (++⁻)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Product.Base as Product using (_,_)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Nullary.Negation using (¬_)
+
+import Data.List.Relation.Binary.Disjoint.Setoid.Properties as S
+
+module _ {a} {A : Set a} where
+
+  private
+    Sᴬ = setoid A
+    variable
+      x : A
+      xs ys vs : List A
+      xss : List (List A)
+
+  ------------------------------------------------------------------------
+  -- Relational properties
+  ------------------------------------------------------------------------
+
+  sym : Symmetric Disjoint
+  sym = S.sym Sᴬ
+
+  ------------------------------------------------------------------------
+  -- Relationship with other predicates
+  ------------------------------------------------------------------------
+
+  Disjoint⇒AllAll : Disjoint xs ys → All (λ x → All (λ y → ¬ x ≡ y) ys) xs
+  Disjoint⇒AllAll = S.Disjoint⇒AllAll Sᴬ
+
+  ------------------------------------------------------------------------
+  -- Introduction (⁺) and elimination (⁻) rules for list operations
+  ------------------------------------------------------------------------
+  -- concat
+
+  concat⁺ʳ : All (Disjoint vs) xss → Disjoint vs (concat xss)
+  concat⁺ʳ = S.concat⁺ʳ (setoid _)
+
+  -- deduplicate
+  module _ (_≟_ : DecidableEquality A) where
+    private dedup≡ = deduplicate _≟_
+
+    deduplicate⁺ : Disjoint xs ys → Disjoint (dedup≡ xs) (dedup≡ ys)
+    deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_
+
+    ∈-dedup : x ∈ xs ⇔ x ∈ dedup≡ xs
+    ∈-dedup = S.∈-dedup Sᴬ _≟_

src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda

@@ -8,49 +8,65 @@
 
 module Data.List.Relation.Binary.Disjoint.Setoid.Properties where
 
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_; mk⇔)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Disjoint.Setoid
 import Data.List.Relation.Unary.Any as Any
 open import Data.List.Relation.Unary.All as All
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
-open import Data.Product.Base using (_,_)
+import Data.List.Membership.Setoid.Properties as Mem
+open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (Symmetric)
+open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 
-------------------------------------------------------------------------
--- Relational properties
-------------------------------------------------------------------------
-
 module _ {c ℓ} (S : Setoid c ℓ) where
 
-  sym : Symmetric (Disjoint S)
-  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)
+  open Setoid S using (_≈_; reflexive) renaming (Carrier to A)
 
-------------------------------------------------------------------------
--- Relationship with other predicates
-------------------------------------------------------------------------
+  ------------------------------------------------------------------------
+  -- Relational properties
+  ------------------------------------------------------------------------
 
-module _ {c ℓ} (S : Setoid c ℓ) where
+  sym : Symmetric (Disjoint S)
+  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)
 
-  open Setoid S
+  ------------------------------------------------------------------------
+  -- Relationship with other predicates
+  ------------------------------------------------------------------------
 
   Disjoint⇒AllAll : ∀ {xs ys} → Disjoint S xs ys →
                     All (λ x → All (λ y → ¬ x ≈ y) ys) xs
   Disjoint⇒AllAll xs#ys = All.map (¬Any⇒All¬ _)
     (All.tabulate (λ v∈xs v∈ys → xs#ys (Any.map reflexive v∈xs , v∈ys)))
 
-------------------------------------------------------------------------
--- Introduction (⁺) and elimination (⁻) rules for list operations
-------------------------------------------------------------------------
--- concat
-
-module _ {c ℓ} (S : Setoid c ℓ) where
+  ------------------------------------------------------------------------
+  -- Introduction (⁺) and elimination (⁻) rules for list operations
+  ------------------------------------------------------------------------
+  -- concat
 
   concat⁺ʳ : ∀ {vs xss} → All (Disjoint S vs) xss → Disjoint S vs (concat xss)
   concat⁺ʳ {xss = xs ∷ xss} (vs#xs ∷ vs#xss) (v∈vs , v∈xs++concatxss)
     with ++⁻ xs v∈xs++concatxss
   ... | inj₁ v∈xs  = vs#xs (v∈vs , v∈xs)
   ... | inj₂ v∈xss = concat⁺ʳ vs#xss (v∈vs , v∈xss)
+
+  -- deduplicate
+  module _ (_≟_ : DecidableEquality A) where
+
+    open import Data.List.Membership.Setoid S using (_∈_)
+
+    private
+      dedup≡   = deduplicate _≟_
+      ∈-dedup⁺ = Mem.∈-deduplicate⁺ S _≟_
+      ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_
+
+    deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys → Disjoint S (dedup≡ xs) (dedup≡ ys)
+    deduplicate⁺ = _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _)
+
+    ∈-dedup : ∀ {x xs} → x ∈ xs ⇔ x ∈ dedup≡ xs
+    ∈-dedup = mk⇔ (∈-dedup⁺ λ where _≡_.refl x≈ → x≈) (∈-dedup⁻ _)

src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda

@@ -0,0 +1,62 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of permutation (with K)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --with-K #-}
+
+module Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK where
+
+open import Function.Base using (_$_)
+open import Function.Bundles using (_⇔_; mk⇔)
+open import Function.Related.Propositional using (SK-sym; module EquationalReasoning)
+
+open import Data.List.Base using (deduplicate; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties
+  using (∈-++⁻; ∈-++⁺ˡ; ∈-++⁺ʳ; ∈-++; ∈-deduplicate⁻)
+open import Data.List.Membership.Propositional.Properties.WithK
+  using (unique∧set⇒bag)
+open import Data.List.Relation.Unary.Unique.Propositional.Properties using (++⁺)
+open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint)
+open import Data.List.Relation.Binary.Disjoint.Propositional.Properties
+  using (deduplicate⁺; ∈-dedup)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
+open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭)
+
+open import Data.Sum as Sum using (_⊎_)
+open import Data.Sum.Function.Propositional using (_⊎-cong_)
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+------------------------------------------------------------------------
+-- deduplicate
+
+module _ {a}{A : Set a} (_≟_ : DecidableEquality A) where
+
+  private
+    dedup≡   = deduplicate _≟_
+    ∈-dedup≡ = ∈-dedup     _≟_
+
+  open import Data.List.Relation.Unary.Unique.DecPropositional.Properties _≟_
+    using (deduplicate-!)
+
+  dedup-++-↭ : ∀ {xs ys} → Disjoint xs ys → dedup≡ (xs ++ ys) ↭ dedup≡ xs ++ dedup≡ ys
+  dedup-++-↭ {xs}{ys} disj
+    = ∼bag⇒↭
+    $ unique∧set⇒bag
+        (deduplicate-! _)
+        (++⁺ (deduplicate-! _) (deduplicate-! _) (deduplicate⁺ _≟_ disj))
+    λ {x} →
+    begin
+      x ∈ dedup≡ (xs ++ ys)
+    ∼⟨ SK-sym ∈-dedup≡ ⟩
+      x ∈ xs ++ ys
+    ∼⟨ ∈-++ ⟩
+      (x ∈ xs ⊎ x ∈ ys)
+    ∼⟨ ∈-dedup≡ ⊎-cong ∈-dedup≡ ⟩
+      (x ∈ dedup≡ xs ⊎ x ∈ dedup≡ ys)
+    ∼⟨ SK-sym ∈-++ ⟩
+      x ∈ dedup≡ xs ++ dedup≡ ys
+    ∎ where open EquationalReasoning