Refactor List.Membership.* and List.Relation.Unary.Any (#2324)

* `contradiction` against `⊥-elim`

* tightened `import`s

* added two operations `∃∈` and `∀∈`

* added to `CHANGELOG`

* knock-on for the `Propositional` case

* refactor `lose∘find` and `find∘lose` in terms of new lemmas `∃∈-Any∘find` and `find∘∃∈-Any`

* `CHANGELOG`

* reorder

* knock-on viscosity

* knock-on viscosity; plus refactoring of `×↔` for intelligibility

* knock-on viscosity

* tightened `import`s

* misc. import and other tweaks

* misc. import and other tweaks

* misc. import and other tweaks

* removed spurious module name

* better definition of `find`

* make intermediate terms explicit in proof of `to∘from`

* tweaks

* Update Setoid.agda

Remove redundant import of `index` from `Any`

* Update Setoid.agda

Removed more redundant `import`ed operations

* Update Properties.agda

Another redundant `import`

* Update Properties.agda

Another redundant `import`ed operation

* `with` into `let`

* `with` into `let`

* `with` into `let`

* `with` into `let`

* indentation

* fix `universal-U`

* added `map-cong`

* deprecate `map-compose` in favour of `map-∘`

* explicit `let` in statement of `find∘map`

* knock-on viscosity: hide `map-cong`

* use of `Product.map₁`

* revert use of `Product.map₁`

* inlined lemmas!

* alpha conversion and further inlining!

* correctted use of `Product.map₂`

* added `syntax` declarations for the new combinators

* remove`⊥-elim`

* reordered `CHANGELOG`

* revise combinator names

* tighten `import`s

* tighten `import`s

* fixed merge conflict bug

* removed new syntax

* knock-on

Author: jamesmckinna

CHANGELOG.md

@@ -82,16 +82,9 @@ Deprecated names
   scanl-defn  ↦  Data.List.Scans.Properties.scanl-defn
   ```
 
-* In `Data.List.NonEmpty.Base`:
-  ```agda
-  inits : List A → List⁺ (List A)
-  tails : List A → List⁺ (List A)
-  ```
-
-* In `Data.List.NonEmpty.Properties`:
+* In `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  toList-inits : toList ∘ List⁺.inits ≗ List.inits
-  toList-tails : toList ∘ List⁺.tails ≗ List.tails
+  map-compose  ↦  map-∘
   ```
 
 * In `Data.Nat.Divisibility.Core`:
@@ -412,6 +405,12 @@ Additions to existing modules
   tail∘tails : List A → List (List A)
   ```
 
+* In `Data.List.Membership.Propositional.Properties.Core`:
+  ```agda
+  find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p
+  ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
+  ```
+
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
   reverse⁺ : x ∈ xs → x ∈ reverse xs
@@ -424,6 +423,12 @@ Additions to existing modules
   tails : List A → List⁺ (List A)
   ```
 
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-inits : toList ∘ List⁺.inits ≗ List.inits
+  toList-tails : toList ∘ List⁺.tails ≗ List.tails
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   length-catMaybes       : length (catMaybes xs) ≤ length xs
@@ -477,6 +482,21 @@ Additions to existing modules
   mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ []
   ```
 
+* In `Data.List.Relation.Binary.Pointwise.Base`:
+  ```agda
+  unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
+  ```
+
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+  ```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Setoid`:
+  ```agda
+  ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
+  ```
+
 * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
   ```agda
   ⊆-trans-idˡ   : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) →
@@ -498,6 +518,11 @@ Additions to existing modules
   reverse⁻            : reverse as ⊆ reverse bs → as ⊆ bs
   ```
 
+* In `Data.List.Relation.Unary.All`:
+  ```agda
+  universal-U : Universal (All U)
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
@@ -510,6 +535,12 @@ Additions to existing modules
   tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
   ```
 
+* In `Data.List.Relation.Unary.Any.Properties`:
+  ```agda
+  map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) →
+             (p : Any P xs) → Any.map f p ≡ Any.map g p
+  ```
+
 * In `Data.List.Relation.Ternary.Appending.Setoid.Properties`:
   ```agda
   through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
@@ -536,21 +567,6 @@ Additions to existing modules
                          ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
   ```
 
-* In `Data.List.Relation.Binary.Pointwise.Base`:
-  ```agda
-  unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
-  ```
-
-* In `Data.Maybe.Relation.Binary.Pointwise`:
-  ```agda
-  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Setoid`:
-  ```agda
-  ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
-  ```
-
 * In `Data.Nat.Divisibility`:
   ```agda
   quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient

src/Data/List/Membership/Propositional.agda

@@ -10,7 +10,7 @@
 module Data.List.Membership.Propositional {a} {A : Set a} where
 
 open import Data.List.Relation.Unary.Any using (Any)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp; subst)
 open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 import Data.List.Membership.Setoid as SetoidMembership
@@ -32,4 +32,4 @@ _≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs
 -- Other operations
 
 lose : ∀ {p} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
-lose = SetoidMembership.lose (setoid A) (subst _)
+lose = SetoidMembership.lose (setoid A) (resp _)

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

@@ -10,26 +10,26 @@ module Data.List.Membership.Propositional.Properties where
 
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Selective)
-open import Effect.Monad using (RawMonad)
-open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
-open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
-open import Data.List.Relation.Unary.Any.Properties
-  using (map↔; concat↔; >>=↔; ⊛↔; Any-cong; ⊗↔′; ¬Any[])
+open import Data.List.Effectful using (monad)
 open import Data.List.Membership.Propositional
   using (_∈_; _∉_; mapWith∈; _≢∈_)
 import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Binary.Equality.Propositional
   using (_≋_; ≡⇒≋; ≋⇒≡)
-open import Data.List.Effectful using (monad)
-open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_)
-open import Data.Nat.Properties using (_≤?_; m≤n⇒m≤1+n; ≤ᵇ-reflects-≤; <⇒≢; ≰⇒>)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties
+  using (map↔; concat↔; >>=↔; ⊛↔; Any-cong; ⊗↔′; ¬Any[])
+open import Data.Nat.Base using (ℕ; suc; s≤s; _≤_; _<_; _≰_)
+open import Data.Nat.Properties
+  using (suc-injective; m≤n⇒m≤1+n; _≤?_; <⇒≢; ≰⇒>)
 open import Data.Product.Base using (∃; ∃₂; _×_; _,_)
 open import Data.Product.Properties using (×-≡,≡↔≡)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+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
@@ -40,15 +40,14 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_)
+  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
-open import Relation.Unary using (_⟨×⟩_; Decidable)
-import Relation.Nullary.Reflects as Reflects
+open import Relation.Nullary.Decidable.Core
+  using (Dec; yes; no; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
+open import Relation.Unary using (_⟨×⟩_; Decidable)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
@@ -128,8 +127,9 @@ module _ {v : A} where
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
 
   ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
-  ∈-∃++ v∈xs with Membership.∈-∃++ (≡.setoid A) v∈xs
-  ... | ys , zs , _ , refl , eq = ys , zs , ≋⇒≡ eq
+  ∈-∃++ v∈xs
+    with ys , zs , _ , refl , eq ← Membership.∈-∃++ (≡.setoid A) v∈xs
+    = ys , zs , ≋⇒≡ eq
 
 ------------------------------------------------------------------------
 -- concat
@@ -147,8 +147,9 @@ module _ {v : A} where
     Membership.∈-concat⁺′ (≡.setoid A) v∈vs (Any.map ≡⇒≋ vs∈xss)
 
   ∈-concat⁻′ : ∀ xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ xss
-  ∈-concat⁻′ xss v∈c with Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
-  ... | xs , v∈xs , xs∈xss = xs , v∈xs , Any.map ≋⇒≡ xs∈xss
+  ∈-concat⁻′ xss v∈c =
+    let xs , v∈xs , xs∈xss = Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
+    in xs , v∈xs , Any.map ≋⇒≡ xs∈xss
 
   concat-∈↔ : ∀ {xss : List (List A)} →
               (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
@@ -183,8 +184,9 @@ module _ (f : A → B → C) where
 
 ∈-cartesianProduct⁻ : ∀ xs ys {xy@(x , y) : A × B} →
                       xy ∈ cartesianProduct xs ys → x ∈ xs × y ∈ ys
-∈-cartesianProduct⁻ xs ys xy∈p[xs,ys] with ∈-cartesianProductWith⁻ _,_ xs ys xy∈p[xs,ys]
-... | (x , y , x∈xs , y∈ys , refl) = x∈xs , y∈ys
+∈-cartesianProduct⁻ xs ys xy∈p[xs,ys]
+  with _ , _ , x∈xs , y∈ys , refl ← ∈-cartesianProductWith⁻ _,_ xs ys xy∈p[xs,ys]
+  = x∈xs , y∈ys
 
 ------------------------------------------------------------------------
 -- applyUpTo
@@ -205,8 +207,7 @@ module _ (f : ℕ → A) where
 ∈-upTo⁺ = ∈-applyUpTo⁺ id
 
 ∈-upTo⁻ : ∀ {n i} → i ∈ upTo n → i < n
-∈-upTo⁻ p with ∈-applyUpTo⁻ id p
-... | _ , i<n , refl = i<n
+∈-upTo⁻ p with _ , i<n , refl ← ∈-applyUpTo⁻ id p = i<n
 
 ------------------------------------------------------------------------
 -- applyDownFrom
@@ -227,8 +228,7 @@ module _ (f : ℕ → A) where
 ∈-downFrom⁺ i<n = ∈-applyDownFrom⁺ id i<n
 
 ∈-downFrom⁻ : ∀ {n i} → i ∈ downFrom n → i < n
-∈-downFrom⁻ p with ∈-applyDownFrom⁻ id p
-... | _ , i<n , refl = i<n
+∈-downFrom⁻ p with _ , i<n , refl ← ∈-applyDownFrom⁻ id p = i<n
 
 ------------------------------------------------------------------------
 -- tabulate
@@ -247,10 +247,10 @@ module _ {n} {f : Fin n → A} where
 module _ {p} {P : A → Set p} (P? : Decidable P) where
 
   ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs
-  ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (subst P)
+  ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.resp P)
 
   ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
-  ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (subst P)
+  ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.resp P)
 
 ------------------------------------------------------------------------
 -- derun and deduplicate
@@ -310,7 +310,7 @@ module _ (_≈?_ : DecidableEquality A) where
 ------------------------------------------------------------------------
 -- length
 
-∈-length : ∀ {x : A} {xs} → x ∈ xs → 1 ≤ length xs
+∈-length : ∀ {x : A} {xs} → x ∈ xs → 0 < length xs
 ∈-length = Membership.∈-length (≡.setoid _)
 
 ------------------------------------------------------------------------
@@ -365,28 +365,27 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper
   helper (yes (i , fᵢ≡x)) = finite f′-inj xs f′ⱼ∈xs
     where
     f′ : ℕ → _
-    f′ j with does (i ≤? j)
-    ... | true  = f (suc j)
-    ... | false = f j
+    f′ j with i ≤? j
+    ... | yes _ = f (suc j)
+    ... | no  _ = f j
 
     ∈-if-not-i : ∀ {j} → i ≢ j → f j ∈ xs
     ∈-if-not-i i≢j = not-x (i≢j ∘ f-inj ∘ trans fᵢ≡x ∘ sym)
 
-    lemma : ∀ {k j} → i ≤ j → ¬ (i ≤ k) → suc j ≢ k
+    lemma : ∀ {k j} → i ≤ j → i ≰ k → suc j ≢ k
     lemma i≤j i≰1+j refl = i≰1+j (m≤n⇒m≤1+n i≤j)
 
     f′ⱼ∈xs : ∀ j → f′ j ∈ xs
-    f′ⱼ∈xs j with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
-    ... | true  | p = ∈-if-not-i (<⇒≢ (s≤s p))
-    ... | false | p = ∈-if-not-i (<⇒≢ (≰⇒> p) ∘ sym)
+    f′ⱼ∈xs j with i ≤? j
+    ... | yes i≤j = ∈-if-not-i (<⇒≢ (s≤s i≤j))
+    ... | no  i≰j = ∈-if-not-i (<⇒≢ (≰⇒> i≰j) ∘ sym)
 
     f′-injective′ : Injective _≡_ _≡_ f′
-    f′-injective′ {j} {k} eq with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
-                                | i ≤ᵇ k | Reflects.invert (≤ᵇ-reflects-≤ i k)
-    ... | true  | p | true  | q = ≡.cong pred (f-inj eq)
-    ... | true  | p | false | q = contradiction (f-inj eq) (lemma p q)
-    ... | false | p | true  | q = contradiction (f-inj eq) (lemma q p ∘ sym)
-    ... | false | p | false | q = f-inj eq
+    f′-injective′ {j} {k} eq with i ≤? j | i ≤? k
+    ... | yes i≤j | yes i≤k = suc-injective (f-inj eq)
+    ... | yes i≤j | no  i≰k = contradiction (f-inj eq) (lemma i≤j i≰k)
+    ... | no  i≰j | yes i≤k = contradiction (f-inj eq) (lemma i≤k i≰j ∘ sym)
+    ... | no  i≰j | no  i≰k = f-inj eq
 
     f′-inj : ℕ ↣ _
     f′-inj = record