Lists: porting several lemmas from other libraries

CHANGELOG.md

@@ -125,30 +125,32 @@ Additions to existing modules
 
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
-  Any-∈-swap    :  Any (_∈ ys) xs → Any (_∈ xs) ys
-  All-∉-swap    :  All (_∉ ys) xs → All (_∉ xs) ys
-  ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
-  ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ →
-                  ∃[ 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
-  ∉[]           : x ∉ []
+  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
+  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
+  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
+  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
+                   ∃[ 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
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
   ```
 
 * In `Data.List.Membership.Propositional.Properties`:
   ```agda
-  ∈-AllPairs₂   : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
-  ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
-  ∈-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)
-  []∉map∷       : [] ∉ map (x ∷_) xss
-  map∷-decomp∈  : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
-  map∷-decomp   : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
-  ∈-map∷⁻       : xs ∈ map (x ∷_) xss → x ∈ xs
-  ∉[]           : x ∉ []
+  ∈-AllPairs₂    : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ∈-map∘filter⁻  : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
+  ∈-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)
+  []∉map∷        : [] ∉ map (x ∷_) xss
+  map∷-decomp∈   : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
+  map∷-decomp    : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
+  ∈-map∷⁻        : xs ∈ map (x ∷_) xss → x ∈ xs
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
@@ -228,13 +230,11 @@ Additions to existing modules
 * 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`:

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

@@ -126,8 +126,8 @@ module _ {v : A} where
   ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
   ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A)
 
-  ∈-++ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
-  ∈-++ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
+  ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ++-∈⇔ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
 
   ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
@@ -299,8 +299,13 @@ module _ (_≈?_ : DecidableEquality A) where
   ∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs
   ∈-derun⁺ z∈xs = Membership.∈-derun⁺ (≡.setoid A) _≈?_ (flip trans) z∈xs
 
+  private resp≈ = λ {c b a : A} (c≡b : c ≡ b) (a≡b : a ≡ b) → trans a≡b (sym c≡b)
+
   ∈-deduplicate⁺ : ∀ {xs z} → z ∈ xs → z ∈ deduplicate _≈?_ xs
-  ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ (λ c≡b a≡b → trans a≡b (sym c≡b)) z∈xs
+  ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ resp≈ z∈xs
+
+  deduplicate-∈⇔ : ∀ {xs z} → z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
+  deduplicate-∈⇔ = Membership.deduplicate-∈⇔ (≡.setoid A) _≈?_ resp≈
 
 ------------------------------------------------------------------------
 -- _>>=_

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

@@ -25,7 +25,7 @@ open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂; ∃-syn
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
-open import Function.Bundles using (_↔_; mk↔)
+open import Function.Bundles using (_↔_; mk↔; _⇔_; mk⇔)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
@@ -426,16 +426,20 @@ module _ (S : Setoid c ℓ) {R : Rel (Carrier S) ℓ₂} (R? : Binary.Decidable
   ∈-derun⁺ : _≈_ Respectsʳ R → ∀ {xs z} → z ∈ xs → z ∈ derun R? xs
   ∈-derun⁺ ≈-resp-R z∈xs = Any.derun⁺ 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⁺ : _≈_ 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]
 
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → ∀ {xs z} →
+                   z ∈ xs ⇔ z ∈ deduplicate R? xs
+  deduplicate-∈⇔ p = mk⇔ (∈-deduplicate⁺ p) (∈-deduplicate⁻ _)
+
 ------------------------------------------------------------------------
 -- length
 

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

@@ -61,10 +61,5 @@ module _ {a} {A : Set a} where
 
   -- deduplicate
   module _ (_≟_ : DecidableEquality A) where
-    private dedup≡ = deduplicate _≟_
-
-    deduplicate⁺ : Disjoint xs ys → Disjoint (dedup≡ xs) (dedup≡ ys)
+    deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
     deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_
-
-    ∈-dedup : x ∈ xs ⇔ x ∈ dedup≡ xs
-    ∈-dedup = S.∈-dedup Sᴬ _≟_

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

@@ -58,15 +58,7 @@ module _ {c ℓ} (S : Setoid c ℓ) where
   -- 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⁻ _)
+    deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys →
+                   Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+    deduplicate⁺ = let ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_ in
+      _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _)

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

@@ -14,14 +14,12 @@ open import Function.Related.Propositional using (SK-sym; module EquationalReaso
 
 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.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)
+  using (deduplicate⁺)
 open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
 open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭)
 
@@ -36,27 +34,21 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
   private
-    dedup≡   = deduplicate _≟_
-    ∈-dedup≡ = ∈-dedup     _≟_
+    dedup≡   = deduplicate    _≟_
+    ∈-dedup≡ = deduplicate-∈⇔ _≟_
 
   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
+  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
+    λ {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