[ refactor ] more general version of _--_ et al. (#598)

Author: gallais

CHANGELOG.md

@@ -288,6 +288,8 @@ Non-backwards compatible changes
 * The proofs `toList⁺` and `toList⁻` in `Data.Vec.Relation.Unary.All.Properties` have been swapped
   as they were the opposite way round to similar properties in the rest of the library.
 
+* The functions `_∷=_` and `_─_` have been removed from `Data.List.Membership.Setoid` as they are subsumed by the more general versions now part of `Data.List.Any`.
+
 * Changed the type of `≡-≟-identity` to make use of the fact that equality
   being decidable implies UIP.
 
@@ -654,14 +656,11 @@ Other minor additions
   forM      : All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
   ```
 
-* Added new operators to `Data.List.Base`:
+* Added new proofs to `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  _[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
-  _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
-  _─_     : (xs : List A) → Fin (length xs) → List A
-
-  reverseAcc : List A → List A → List A
+  respects : P Respects _≈_ → (All P) Respects _≋_
   ```
+
   A generalization of single point overwrite `_[_]≔_`
   to single-point modification `_[_]%=_`
   (alias with different argument order: `updateAt`):
@@ -678,13 +677,28 @@ Other minor additions
 * Added new proofs to `Data.List.Relation.Unary.All.Properties`:
   ```agda
   respects : P Respects _≈_ → (All P) Respects _≋_
+  ─⁺       : All Q xs → All Q (xs Any.─ p)
+  ─⁻       : Q (Any.lookup p) → All Q (xs Any.─ p) → All Q xs
+  ```
+
+* Added new functions to `Data.List.Relation.Unary.Any`:
+  ```agda
+  lookup : Any P xs → A
+  _∷=_   : Any P xs → A → List A
+  _─_    : ∀ xs → Any P xs → List A
   ```
 
 * Added new functions to `Data.List.Base`:
   ```agda
   intercalate       : List A → List (List A) → List A
   partitionSumsWith : (A → B ⊎ C) → List A → List B × List C
   partitionSums     : List (A ⊎ B) → List A × List B
+
+  _[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
+  _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
+  _─_     : (xs : List A) → Fin (length xs) → List A
+
+  reverseAcc : List A → List A → List A
   ```
 
 * Added new proofs to `Data.List.Membership.Propositional.Properties`:

src/Data/List/Membership/Setoid.agda

@@ -13,14 +13,16 @@ module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 open import Function using (_∘_; id; flip)
 open import Data.Fin using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
-open import Data.List.Relation.Unary.Any as Any
+open import Data.List.Relation.Unary.Any
   using (Any; index; map; here; there)
 open import Data.Product as Prod using (∃; _×_; _,_)
 open import Relation.Unary using (Pred)
 open import Relation.Nullary using (¬_)
 
 open Setoid S renaming (Carrier to A)
 
+open Data.List.Relation.Unary.Any using (_∷=_; _─_) public
+
 ------------------------------------------------------------------------
 -- Definitions
 
@@ -40,13 +42,6 @@ mapWith∈ : ∀ {b} {B : Set b}
 mapWith∈ []       f = []
 mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
-_∷=_ : ∀ {xs x} → x ∈ xs → A → List A
-_∷=_ {xs} x∈xs v = xs List.[ index x∈xs ]∷= v
-
-infixl 4 _─_
-_─_ : ∀ xs {x} → x ∈ xs → List A
-xs ─ x∈xs = xs List.─ index x∈xs
-
 ------------------------------------------------------------------------
 -- Finding and losing witnesses
 

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

@@ -15,7 +15,7 @@ open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
 open import Data.List.Base
 open import Data.List.Membership.Propositional
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
-open import Data.List.Relation.Unary.Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 import Data.List.Relation.Binary.Equality.Setoid as ListEq using (_≋_; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
@@ -217,6 +217,19 @@ module _ {a p} {A : Set a} {P : A → Set p} where
   tabulate⁻ {suc n} (px ∷ _) fzero    = px
   tabulate⁻ {suc n} (_ ∷ pf) (fsuc i) = tabulate⁻ pf i
 
+------------------------------------------------------------------------
+-- remove
+
+module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where
+
+  ─⁺ : ∀ {xs} (p : Any P xs) → All Q xs → All Q (xs Any.─ p)
+  ─⁺ (here px) (_ ∷ qs) = qs
+  ─⁺ (there p) (q ∷ qs) = q ∷ ─⁺ p qs
+
+  ─⁻ : ∀ {xs} (p : Any P xs) → Q (Any.lookup p) → All Q (xs Any.─ p) → All Q xs
+  ─⁻ (here px) q qs        = q ∷ qs
+  ─⁻ (there p) q (q′ ∷ qs) = q′ ∷ ─⁻ p q qs
+
 ------------------------------------------------------------------------
 -- filter
 

src/Data/List/Relation/Unary/Any.agda

@@ -43,10 +43,22 @@ map : ∀ {p q} {P : A → Set p} {Q : A → Set q} → P ⊆ Q → Any P ⊆ An
 map g (here px)   = here (g px)
 map g (there pxs) = there (map g pxs)
 
--- `index x∈xs` is the list position (zero-based) which `x∈xs` points to.
-index : ∀ {p} {P : A → Set p} {xs} → Any P xs → Fin (List.length xs)
-index (here  px)  = zero
-index (there pxs) = suc (index pxs)
+module _ {p} {P : A → Set p} where
+
+  -- `index x∈xs` is the list position (zero-based) which `x∈xs` points to.
+  index : ∀ {xs} → Any P xs → Fin (List.length xs)
+  index (here  px)  = zero
+  index (there pxs) = suc (index pxs)
+
+  lookup : ∀ {xs} → Any P xs → A
+  lookup {xs} p = List.lookup xs (index p)
+
+  _∷=_ : ∀ {xs} → Any P xs → A → List A
+  _∷=_ {xs} x∈xs v = xs List.[ index x∈xs ]∷= v
+
+  infixl 4 _─_
+  _─_ : ∀ xs → Any P xs → List A
+  xs ─ x∈xs = xs List.─ index x∈xs
 
 -- If any element satisfies P, then P is satisfied.
 satisfied : ∀ {p} {P : A → Set p} {xs} → Any P xs → ∃ P