Weakened pre-conditions of grouped map lemmas (#2108)

Author: MatthewDaggitt

CHANGELOG.md

@@ -851,6 +851,10 @@ Non-backwards compatible changes
   found in `Data.List.NonEmpty.Properties` under the names `groupSeqs-groups`
   and `ungroupSeqs` and `groupSeqs`.
 
+* In `Data.List.Relation.Unary.Grouped.Properties` the proofs `map⁺` and `map⁻`
+  have had their preconditions weakened so the equivalences no longer require congruence
+  proofs.
+
 * The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer
   exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)`
   directly to use them.
@@ -1349,6 +1353,11 @@ Deprecated names
   map-with-∈↔  ↦  mapWith∈↔
   ```
 
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```
+  gmap  ↦  gmap⁺
+  ```
+
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
@@ -3462,6 +3471,11 @@ This is a full list of proofs that have changed form to use irrelevant instance
   #-congˡ       : y ≈ z → x # y → x # z
   ```
 
+* Added new proof to `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  gmap⁻ : Q ∘ f ⋐ P → All Q ∘ map f ⋐ All P
+  ```
+
 * Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties`
   and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`.
   ```agda
@@ -3484,4 +3498,4 @@ This is a full list of proofs that have changed form to use irrelevant instance
       b #⟨ b#c ⟩
       c ≈⟨ c≈d ⟩
       d ∎
-    ```
+    ```

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

@@ -371,8 +371,11 @@ map⁻ {xs = _ ∷ _} (p ∷ ps) = p ∷ map⁻ ps
 
 -- A variant of All.map.
 
-gmap : ∀ {f : A → B} → P ⋐ Q ∘ f → All P ⋐ All Q ∘ map f
-gmap g = map⁺ ∘ All.map g
+gmap⁺ : ∀ {f : A → B} → P ⋐ Q ∘ f → All P ⋐ All Q ∘ map f
+gmap⁺ g = map⁺ ∘ All.map g
+
+gmap⁻ : ∀ {f : A → B} → Q ∘ f ⋐ P → All Q ∘ map f ⋐ All P
+gmap⁻ g = All.map g ∘ map⁻
 
 ------------------------------------------------------------------------
 -- mapMaybe
@@ -679,7 +682,7 @@ replicate⁻ (px ∷ _) = px
 
 inits⁺ : All P xs → All (All P) (inits xs)
 inits⁺ []         = [] ∷ []
-inits⁺ (px ∷ pxs) = [] ∷ gmap (px ∷_) (inits⁺ pxs)
+inits⁺ (px ∷ pxs) = [] ∷ gmap⁺ (px ∷_) (inits⁺ pxs)
 
 inits⁻ : ∀ xs → All (All P) (inits xs) → All P xs
 inits⁻ []               pxs                   = []
@@ -773,3 +776,9 @@ updateAt-cong-relative = updateAt-cong-local
 "Warning: updateAt-cong-relative was deprecated in v2.0.
 Please use updateAt-cong-local instead."
 #-}
+
+gmap = gmap⁺
+{-# WARNING_ON_USAGE gmap
+"Warning: gmap was deprecated in v2.0.
+Please use gmap⁺ instead."
+#-}

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

@@ -14,10 +14,10 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
 open import Data.List.Relation.Unary.Grouped
-open import Function.Base using (_∘_)
-open import Function.Bundles using (module Equivalence; _⇔_)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_; _on_)
 open import Relation.Binary.Definitions as B
-open import Relation.Binary.Core using (REL; Rel)
+open import Relation.Binary.Core using (_⇔_; REL; Rel)
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
@@ -26,31 +26,23 @@ open import Level
 private
   variable
     a b c p q : Level
-    A : Set a
-    B : Set b
-    C : Set c
+    A B C : Set a
 
 ------------------------------------------------------------------------
 -- map
 
 module _ (P : Rel A p) (Q : Rel B q) where
 
-  map⁺ : ∀ {f xs} → (∀ {x y} → P x y ⇔ Q (f x) (f y)) → Grouped P xs → Grouped Q (map f xs)
-  map⁺ {f} {[]} P⇔Q [] = []
-  map⁺ {f} {x ∷ xs} P⇔Q (all[¬Px,xs] ∷≉ g) = aux all[¬Px,xs] ∷≉ map⁺ P⇔Q g where
-    aux : ∀ {ys} → All (λ y → ¬ P x y) ys → All (λ y → ¬ Q (f x) y) (map f ys)
-    aux [] = []
-    aux (py ∷ pys) = py ∘ Equivalence.from P⇔Q ∷ aux pys
-  map⁺ {f} {x₁ ∷ x₂ ∷ xs} P⇔Q (Px₁x₂ ∷≈ g) = Equivalence.to P⇔Q Px₁x₂ ∷≈ map⁺ P⇔Q g
+  map⁺ : ∀ {f xs} → P ⇔ (Q on f) → Grouped P xs → Grouped Q (map f xs)
+  map⁺ P⇔Q            []                      = []
+  map⁺ P⇔Q@(_ , Q⇒P) (all[¬Px,xs] ∷≉ g[xs]) = All.gmap⁺ (_∘ Q⇒P) all[¬Px,xs] ∷≉ map⁺ P⇔Q g[xs]
+  map⁺ P⇔Q@(P⇒Q , _) (Px₁x₂ ∷≈ g[xs])       = P⇒Q Px₁x₂ ∷≈ map⁺ P⇔Q g[xs]
 
-  map⁻ : ∀ {f xs} → (∀ {x y} → P x y ⇔ Q (f x) (f y)) → Grouped Q (map f xs) → Grouped P xs
-  map⁻ {f} {[]} P⇔Q [] = []
-  map⁻ {f} {x ∷ []} P⇔Q ([] ∷≉ []) = [] ∷≉ []
-  map⁻ {f} {x₁ ∷ x₂ ∷ xs} P⇔Q (all[¬Qx,xs] ∷≉ g) = aux all[¬Qx,xs] ∷≉ map⁻ P⇔Q g where
-    aux : ∀ {ys} → All (λ y → ¬ Q (f x₁) y) (map f ys) → All (λ y → ¬ P x₁ y) ys
-    aux {[]} [] = []
-    aux {y ∷ ys} (py ∷ pys) = py ∘ Equivalence.to P⇔Q ∷ aux pys
-  map⁻ {f} {x₁ ∷ x₂ ∷ xs} P⇔Q (Qx₁x₂ ∷≈ g) = Equivalence.from P⇔Q Qx₁x₂ ∷≈ map⁻ P⇔Q g
+  map⁻ : ∀ {f xs} → P ⇔ (Q on f) → Grouped Q (map f xs) → Grouped P xs
+  map⁻ {xs = []}          P⇔Q            []                  = []
+  map⁻ {xs = _ ∷ []}     P⇔Q            ([] ∷≉ [])         = [] ∷≉ []
+  map⁻ {xs = _ ∷ _ ∷ _} P⇔Q@(P⇒Q , _) (all[¬Qx,xs] ∷≉ g) = All.gmap⁻ (_∘ P⇒Q) all[¬Qx,xs] ∷≉ map⁻ P⇔Q g
+  map⁻ {xs = _ ∷ _ ∷ _} P⇔Q@(_ , Q⇒P) (Qx₁x₂ ∷≈ g)       = Q⇒P Qx₁x₂ ∷≈ map⁻ P⇔Q g
 
 ------------------------------------------------------------------------
 -- [_]