Vec.Properties: introduce ≈-cong′ (#2424)

* Vec.Properties: introduce `≈-cong′`

* derive cast-* lemmas from it

* use it in proofs

* match m and n before the Vecs

* convert Cast's implicit module param to variable

(needed for next commit)

* move ≈-cong′ to Cast

* add changelog entry

* implement suggested changes

- do not export lemma from Vec.Properties
- use Function.Base rather than Function

Author: mildsunrise

CHANGELOG.md

@@ -545,6 +545,13 @@ Additions to existing modules
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)
   ```
 
+* New lemma in `Data.Vec.Relation.Binary.Equality.Cast`:
+  ```agda
+  ≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n))
+    {m n} {xs : Vec A m} {ys : Vec A n} .{eq} →
+    xs ≈[ eq ] ys → f xs ≈[ _ ] f ys
+  ```
+
 * In `Data.Vec.Relation.Binary.Equality.DecPropositional`:
   ```agda
   _≡?_ : DecidableEquality (Vec A n)

doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -20,6 +20,7 @@ open import Data.Nat.Properties
 open import Data.Vec.Base
 open import Data.Vec.Properties
 open import Data.Vec.Relation.Binary.Equality.Cast
+open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; module ≡-Reasoning)
 
@@ -187,7 +188,7 @@ example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin
   fromList (xs List.++ ys List.++ zs)
     ≈⟨ fromList-++ xs ⟩
   fromList xs ++ fromList (ys List.++ zs)
-    ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (List.length-++ ys) (fromList xs)) (fromList-++ ys) ⟩
+    ≈⟨ ≈-cong′ (fromList xs ++_) (fromList-++ ys) ⟩
   fromList xs ++ fromList ys ++ fromList zs
     ∎
   where open CastReasoning
@@ -218,9 +219,7 @@ example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys →
           cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
 example4-cong² {m = m} {n} eq a xs ys = begin
   reverse ((xs ++ [ a ]) ++ ys)
-    ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
-                                             (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
-                                                     (unfold-∷ʳ-eqFree a xs)) ⟨
+    ≈⟨ ≈-cong′ (reverse ∘ (_++ ys)) (unfold-∷ʳ-eqFree a xs) ⟨
   reverse ((xs ∷ʳ a) ++ ys)
     ≈⟨ reverse-++-eqFree (xs ∷ʳ a) ys ⟩
   reverse ys ++ reverse (xs ∷ʳ a)
@@ -264,7 +263,7 @@ example6a-reverse-∷ʳ {n = n} x xs = begin-≡
   reverse (xs ∷ʳ x)
     ≡⟨ ≈-reflexive refl ⟨
   reverse (xs ∷ʳ x)
-    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ-eqFree x xs) ⟩
+    ≈⟨ ≈-cong′ reverse (unfold-∷ʳ-eqFree x xs) ⟩
   reverse (xs ++ [ x ])
     ≈⟨ reverse-++-eqFree xs [ x ] ⟩
   x ∷ reverse xs

src/Data/Vec/Properties.agda

@@ -375,6 +375,8 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 open VecCast public
   using (cast-is-id; cast-trans)
 
+open VecCast using (≈-cong′)
+
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
 
@@ -398,9 +400,7 @@ map-const (_ ∷ xs) y = cong (y ∷_) (map-const xs y)
 
 map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) →
            map f (cast eq xs) ≡ cast eq (map f xs)
-map-cast {n = zero}  f eq []       = refl
-map-cast {n = suc _} f eq (x ∷ xs)
-  = cong (f x ∷_) (map-cast f (suc-injective eq) xs)
+map-cast f _ _ = sym (≈-cong′ (map f) refl)
 
 map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
          map f (xs ++ ys) ≡ map f xs ++ map f ys
@@ -494,13 +494,11 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 
 cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
            cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
-cast-++ˡ {o = zero}  eq []       {ys} = cast-is-id refl (cast eq [] ++ ys)
-cast-++ˡ {o = suc o} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ˡ (cong pred eq) xs)
+cast-++ˡ _ _ {ys} = ≈-cong′ (_++ ys) refl
 
 cast-++ʳ : ∀ .(eq : n ≡ o) (xs : Vec A m) {ys : Vec A n} →
            cast (cong (m +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys
-cast-++ʳ {m = zero}  eq []       {ys} = refl
-cast-++ʳ {m = suc m} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ʳ eq xs)
+cast-++ʳ _ xs = ≈-cong′ (xs ++_) refl
 
 lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i<m : toℕ i < m) →
@@ -929,8 +927,7 @@ map-∷ʳ f x (y ∷ xs) = cong (f y ∷_) (map-∷ʳ f x xs)
 
 cast-∷ʳ : ∀ .(eq : suc n ≡ suc m) x (xs : Vec A n) →
           cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
-cast-∷ʳ {m = zero}  eq x []       = refl
-cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq) x xs)
+cast-∷ʳ _ x _ = ≈-cong′ (_∷ʳ x) refl
 
 -- _++_ and _∷ʳ_
 
@@ -1034,23 +1031,14 @@ reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
 reverse-++-eqFree {m = zero}  {n = n} []       ys = ≈-sym (++-identityʳ-eqFree (reverse ys))
 reverse-++-eqFree {m = suc m} {n = n} (x ∷ xs) ys = begin
   reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
-  reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys)))
-                                                (reverse-++-eqFree xs ys) ⟩
+  reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong′ (_∷ʳ x) (reverse-++-eqFree xs ys) ⟩
   (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ-eqFree x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
   reverse ys ++ (reverse (x ∷ xs))    ∎
   where open CastReasoning
 
 cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
-cast-reverse {n = zero}  eq []       = refl
-cast-reverse {n = suc n} eq (x ∷ xs) = begin
-  reverse (x ∷ xs)           ≂⟨ reverse-∷ x xs ⟩
-  reverse xs ∷ʳ x            ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ eq x (reverse xs))
-                                       (cast-reverse (cong pred eq) xs) ⟩
-  reverse (cast _ xs) ∷ʳ x   ≂⟨ reverse-∷ x (cast (cong pred eq) xs) ⟨
-  reverse (x ∷ cast _ xs)    ≈⟨⟩
-  reverse (cast eq (x ∷ xs)) ∎
-  where open CastReasoning
+cast-reverse _ _ = ≈-cong′ reverse refl
 
 ------------------------------------------------------------------------
 -- _ʳ++_
@@ -1094,8 +1082,7 @@ map-ʳ++ {ys = ys} f xs = begin
                 cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
 ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
   ((xs ++ ys) ʳ++ zs)              ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
-  reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys)))
-                                             (reverse-++-eqFree xs ys) ⟩
+  reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong′ (_++ zs) (reverse-++-eqFree xs ys) ⟩
   (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) (reverse xs) zs ⟩
   reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
   reverse ys ++ (xs ʳ++ zs)        ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
@@ -1107,8 +1094,7 @@ map-ʳ++ {ys = ys} f xs = begin
 ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
   (xs ʳ++ ys) ʳ++ zs                         ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
   (reverse xs ++ ys) ʳ++ zs                  ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
-  reverse (reverse xs ++ ys) ++ zs           ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys)))
-                                                       (reverse-++-eqFree (reverse xs) ys) ⟩
+  reverse (reverse xs ++ ys) ++ zs           ≈⟨ ≈-cong′ (_++ zs) (reverse-++-eqFree (reverse xs) ys) ⟩
   (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
   (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc-eqFree (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
@@ -1338,8 +1324,7 @@ fromList-reverse (x List.∷ xs) = begin
   fromList (List.reverse (x List.∷ xs))         ≈⟨ cast-fromList (List.ʳ++-defn xs) ⟩
   fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
   fromList (List.reverse xs) ++ [ x ]           ≈⟨ unfold-∷ʳ-eqFree x (fromList (List.reverse xs)) ⟨
-  fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _)
-                                                          (fromList-reverse xs) ⟩
+  fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong′ (_∷ʳ x) (fromList-reverse xs) ⟩
   reverse (fromList xs) ∷ʳ x                    ≂⟨ reverse-∷ x (fromList xs) ⟨
   reverse (x ∷ fromList xs)                     ≈⟨⟩
   reverse (fromList (x List.∷ xs))              ∎

src/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -10,8 +10,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.Vec.Relation.Binary.Equality.Cast {a} {A : Set a} where
+module Data.Vec.Relation.Binary.Equality.Cast where
 
+open import Level using (Level)
+open import Function.Base using (_∘_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Vec.Base
@@ -24,6 +26,8 @@ open import Relation.Binary.PropositionalEquality.Properties
 
 private
   variable
+    a b : Level
+    A B : Set a
     l m n o : ℕ
     xs ys zs : Vec A n
 
@@ -41,31 +45,38 @@ cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
 
 infix 3 _≈[_]_
 
-_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set a
+_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set _
 xs ≈[ eq ] ys = cast eq xs ≡ ys
 
 ------------------------------------------------------------------------
 -- _≈[_]_ is ‘reflexive’, ‘symmetric’ and ‘transitive’
 
-≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys)
+≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {A = A} {n} xs refl ys)
 ≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq
 
-≈-sym : .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_
+≈-sym : .{m≡n : m ≡ n} → Sym {A = Vec A m} _≈[ m≡n ]_ _≈[ sym m≡n ]_
 ≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin
   cast (sym m≡n) ys             ≡⟨ cong (cast (sym m≡n)) xs≈ys ⟨
   cast (sym m≡n) (cast m≡n xs)  ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩
   cast (trans m≡n (sym m≡n)) xs ≡⟨ cast-is-id (trans m≡n (sym m≡n)) xs ⟩
   xs                            ∎
   where open ≡-Reasoning
 
-≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
+≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} →
+          Trans {A = Vec A m} _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
 ≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin
   cast (trans m≡n n≡o) xs ≡⟨ cast-trans m≡n n≡o xs ⟨
   cast n≡o (cast m≡n xs)  ≡⟨ cong (cast n≡o) xs≈ys ⟩
   cast n≡o ys             ≡⟨ ys≈zs ⟩
   zs                      ∎
   where open ≡-Reasoning
 
+≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n))
+          {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys →
+          f xs ≈[ cong f-len eq ] f ys
+≈-cong′ f {m = zero}  {n = zero}  {xs = []}     {ys = []}     refl = cast-is-id refl (f [])
+≈-cong′ f {m = suc m} {n = suc n} {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl
+
 ------------------------------------------------------------------------
 -- Reasoning combinators