Final overhaul of list membership and associated relations (#271)

CHANGELOG.md

@@ -8,6 +8,53 @@ Important changes since 0.15:
 Non-backwards compatible changes
 --------------------------------
 
+#### Final overhaul of list membership
+
+* The aim of this final rearrangement of list membership is to create a better interface for
+  the different varieties of membership, and make it easier to predict where certain
+  proofs are found. Each of the new membership modules are parameterised by the relevant types
+  so as to allow easy access to the infix  `_∈_` and `_∈?_` operators. It also increases
+  the discoverability of the modules by new users of the library.
+
+* The following re-organisation of list membership modules has occurred:
+  ```agda
+  Data.List.Any.BagAndSetEquality        ↦ Data.List.Relation.BagAndSetEquality
+  Data.List.Any.Membership               ↦ Data.List.Membership.Setoid
+                                         ↘ Data.List.Membership.DecSetoid
+                                         ↘ Data.List.Relation.Sublist.Setoid
+  Data.List.Any.Membership.Propositional ↦ Data.List.Membership.Propositional
+                                         ↘ Data.List.Membership.DecPropositional
+                                         ↘ Data.List.Relation.Sublist.Propositional
+  ```
+
+* The `_⊆_` relation has been moved out of the `Membership` modules to new
+  modules `List.Relation.Sublist.(Setoid/Propositional)`. Consequently the `mono`
+  proofs that were in `Membership.Propositional.Properties` have been moved to
+  `Relation.Sublist.Propositional.Properties`.
+
+* The following proofs have been moved from `Any.Properties` to
+  `Membership.Propositional.Properties.Core`:
+  ```agda
+  map∘find, find∘map, find-∈, lose∘find, find∘lose, ∃∈-Any, Any↔
+  ```
+
+* The following terms have been moved out of `Membership.Propositional` into
+  `Relation.BagAndSetEquality`:
+  ```agda
+  Kind, Symmetric-kind
+  set, subset, superset, bag, subbag, superbag
+  [_]-Order, [_]-Equality, _∼[_]_
+  ```
+
+* The type of the proof of `∈-resp-≈` in `Membership.Setoid.Properties` has changed from:
+  ```agda
+  ∈-resp-≈ : ∀ {x} → (x ≈_) Respects _≈_
+  ```
+  to
+  ```agda
+  ∈-resp-≈ : ∀ {xs} → (_∈ xs) Respects _≈_
+  ```
+
 #### Upgrade of `Algebra.Operations`
 
 * Previously `Algebra.Operations` was parameterised by a semiring, however several of the
@@ -92,11 +139,21 @@ anticipated any time soon, they may eventually be removed in some future release
   isDecTotalOrder⟶isStrictTotalOrder  ↦ <-isStrictTotalOrder₂
   ```
 
-* In `IsStrictPartialOrder` in `Relation.Binary`:
+* In `IsStrictPartialOrder` record in `Relation.Binary`:
   ```agda
   asymmetric ↦ asym
   ```
 
+* In `Data.List.Membership.Propositional`:
+  ```agda
+  filter-∈ ↦ ∈-filter⁺
+  ```
+
+* In `Data.List.Membership.Setoid`:
+  ```agda
+  map-with-∈ ↦ mapWith∈
+  ```
+
 Removed features
 ----------------
 
@@ -148,12 +205,54 @@ Backwards compatible changes
   unzip : All (P ∩ Q) ⊆ All P ∩ All Q
   ```
 
+* Added new proofs to `Data.List.Membership.(Setoid/Propositional).Properties`:
+  ```agda
+  ∉-resp-≈      : ∀ {xs} → (_∉ xs) Respects _≈_
+  ∉-resp-≋      : ∀ {x}  → (x ∉_)  Respects _≋_
+
+  mapWith∈≗map  : mapWith∈ xs (λ {x} _ → f x) ≡ map f xs
+  mapWith∈-cong : (∀ x∈xs → f x∈xs ≡ g x∈xs) → mapWith∈ xs f ≡ map-with-∈ xs g
+
+  ∈-++⁺ˡ        : v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ʳ        : v ∈ ys → v ∈ xs ++ ys
+  ∈-++⁻         : v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
+
+  ∈-concat⁺     : Any (v ∈_) xss → v ∈ concat xss
+  ∈-concat⁻     : v ∈ concat xss → Any (v ∈_) xss
+  ∈-concat⁺′    : v ∈ vs → vs ∈ xss → v ∈ concat xss
+  ∈-concat⁻′    : v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ xss
+
+  ∈-applyUpTo⁺  : i < n → f i ∈ applyUpTo f n
+  ∈-applyUpTo⁻  : v ∈ applyUpTo f n → ∃ λ i → i < n × v ≈ f i
+
+  ∈-tabulate⁺   : f i ∈ tabulate f
+  ∈-tabulate⁻   : v ∈ tabulate f → ∃ λ i → v ≈ f i
+
+  ∈-filter⁺     : P v → v ∈ xs → v ∈ filter P? xs
+  ∈-filter⁻     : v ∈ filter P? xs → v ∈ xs × P v
+
+  ∈-length      : x ∈ xs → 1 ≤ length xs
+  ∈-lookup      : lookup xs i ∈ xs
+
+  foldr-selective : Selective _≈_ _•_ → (foldr _•_ e xs ≈ e) ⊎ (foldr _•_ e xs ∈ xs)
+  ```
+
 * Added new proofs to `Data.List.Properties`:
   ```agda
-  tabulate-cong : f ≗ g → tabulate f ≡ tabulate g
+  tabulate-cong   : f ≗ g → tabulate f ≡ tabulate g
   tabulate-lookup : tabulate (lookup xs) ≡ xs
   ```
 
+* Added new proofs to `Data.List.Relation.Sublist.(Setoid/Propositional).Properties`:
+  ```agda
+  ⊆-reflexive  : _≋_ ⇒ _⊆_
+  ⊆-refl       : Reflexive _⊆_
+  ⊆-trans      : Transitive _⊆_
+  ⊆-isPreorder : IsPreorder _≋_ _⊆_
+
+  filter⁺      : ∀ xs → filter P? xs ⊆ xs
+  ```
+
 * Added new modules `Data.List.Zipper` and `Data.List.Zipper.Properties`.
 
 * Added new proofs to `Data.Nat.Properties`:
@@ -217,7 +316,7 @@ Backwards compatible changes
   P Respectsʳ _∼_ = ∀ {x} → (P x)      Respects _∼_
   P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_
   ```
-  Records in `Relation.Binary` export these in addition to the standard `Respects₂` proofs.
+  Records in `Relation.Binary` now export these in addition to the standard `Respects₂` proofs.
   e.g. `IsStrictPartialOrder` exports:
   ```agda
   <-respˡ-≈ : _<_ Respectsˡ _≈_

src/Data/List/All.agda

@@ -8,7 +8,7 @@ module Data.List.All where
 
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Any as Any using (here; there)
-open import Data.List.Any.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional using (_∈_)
 open import Data.Product as Prod using (_,_)
 open import Function
 open import Level

src/Data/List/All/Properties.agda

@@ -11,10 +11,11 @@ open import Data.Bool.Properties
 open import Data.Empty
 open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
 open import Data.List.Base
-open import Data.List.Any.Membership.Propositional
+open import Data.List.Membership.Propositional
 open import Data.List.All as All using (All; []; _∷_)
 open import Data.List.Any using (Any; here; there)
 open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Sublist.Propositional using (_⊆_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing)
 open import Data.Nat using (zero; suc; z≤n; s≤s; _<_)
 open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
@@ -28,7 +29,8 @@ open import Relation.Nullary
 open import Relation.Unary
   using (Decidable; Universal) renaming (_⊆_ to _⋐_)
 
------------------------------------------------------------------------- Basic properties of All
+----------------------------------------------------------------------
+-- Basic properties of All
 
 module _ {a p} {A : Set a} {P : A → Set p} where