From a01a0ae38af0ba49ba54301ebba9a51effcfabb9 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 30 Jun 2024 01:15:41 +0200
Subject: [PATCH 1/5] Vec.Properties: drop eq parameter when it is a property
 (fixes #2421)

---
 src/Data/Vec/Properties.agda | 162 ++++++++++++++++++++++++++---------
 1 file changed, 121 insertions(+), 41 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index bea3cfea95..c245bd323b 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -17,7 +17,7 @@ import Data.List.Properties as List
 open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_;
   s≤s⁻¹; z≤n)
 open import Data.Nat.Properties
-  using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc)
+  using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc; +-identityʳ)
 open import Data.Product.Base as Product
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -38,6 +38,10 @@ open import Relation.Nullary.Decidable.Core using (Dec; does; yes; _×-dec_; map
 open import Relation.Nullary.Negation.Core using (contradiction)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
+private
+  m+n+o≡n+[m+o] : ∀ m n o → m + n + o ≡ n + (m + o)
+  m+n+o≡n+[m+o] m n o = trans (cong (_+ o) (+-comm m n)) (+-assoc n m o)
+
 private
   variable
     a b c d p : Level
@@ -464,14 +468,14 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 ++-injective ws xs eq =
   (++-injectiveˡ ws xs eq , ++-injectiveʳ ws xs eq)
 
-++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
-           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-++-assoc eq []       ys zs = cast-is-id eq (ys ++ zs)
-++-assoc eq (x ∷ xs) ys zs = cong (x ∷_) (++-assoc (cong pred eq) xs ys zs)
+++-assoc′ : ∀ (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) → let eq = +-assoc m n o in
+            cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+++-assoc′ []       ys zs = cast-is-id refl (ys ++ zs)
+++-assoc′ (x ∷ xs) ys zs = cong (x ∷_) (++-assoc′ xs ys zs)
 
-++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
-++-identityʳ eq []       = refl
-++-identityʳ eq (x ∷ xs) = cong (x ∷_) (++-identityʳ (cong pred eq) xs)
+++-identityʳ′ : ∀ (xs : Vec A n) → cast (+-identityʳ n) (xs ++ []) ≡ xs
+++-identityʳ′ []       = refl
+++-identityʳ′ (x ∷ xs) = cong (x ∷_) (++-identityʳ′ xs)
 
 cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
            cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
@@ -865,9 +869,9 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
 
 -- snoc is snoc
 
-unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
-unfold-∷ʳ eq x []       = refl
-unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs)
+unfold-∷ʳ′ : ∀ x (xs : Vec A n) → cast (+-comm 1 n) (xs ∷ʳ x) ≡ xs ++ [ x ]
+unfold-∷ʳ′ x []       = refl
+unfold-∷ʳ′ x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ′ x xs)
 
 ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
 ∷ʳ-injective []       []        refl = (refl , refl)
@@ -915,16 +919,16 @@ cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq
 
 -- _++_ and _∷ʳ_
 
-++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
-        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
-++-∷ʳ {m = zero}  eq z []       []       = refl
-++-∷ʳ {m = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
-++-∷ʳ {m = suc m} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
+++-∷ʳ′ : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
+         cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ′ {m = zero}  z []       []       = refl
+++-∷ʳ′ {m = zero}  z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ′ z [] ys)
+++-∷ʳ′ {m = suc m} z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ′ z xs ys)
 
-∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
-        cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
-∷ʳ-++ eq a []       {ys} = cong (a ∷_) (cast-is-id (cong pred eq) ys)
-∷ʳ-++ eq a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++ (cong pred eq) a xs)
+∷ʳ-++′ : ∀ a (xs : Vec A n) {ys : Vec A m} → let eq = sym (+-suc n m) in
+         cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
+∷ʳ-++′ a []       {ys} = cong (a ∷_) (cast-is-id refl ys)
+∷ʳ-++′ a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++′ a xs)
 
 ------------------------------------------------------------------------
 -- reverse
@@ -1010,14 +1014,14 @@ map-reverse f (x ∷ xs) = begin
 
 -- append and reverse
 
-reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
-             cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ {m = zero}  {n = n} eq []       ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
-reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
+reverse-++′ : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
+              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
+reverse-++′ {m = zero}  {n = n} []       ys = ≈-sym (++-identityʳ′ (reverse ys))
+reverse-++′ {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-++ _ xs ys) ⟩
-  (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
+                                                (reverse-++′ xs ys) ⟩
+  (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ′ x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
   reverse ys ++ (reverse (x ∷ xs))    ∎
   where open CastReasoning
@@ -1061,37 +1065,37 @@ map-ʳ++ {ys = ys} f xs = begin
   map f xs ʳ++ map f ys          ∎
   where open ≡-Reasoning
 
-∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
-        cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++ eq a xs {ys} = begin
+∷-ʳ++′ : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
+         cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+∷-ʳ++′ a xs {ys} = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++′ a (reverse xs) ⟩
   reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨
   xs ʳ++ (a ∷ ys)         ∎
   where open CastReasoning
 
-++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
-         cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
+++-ʳ++′ : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
+          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
+++-ʳ++′ {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-++ (+-comm m n) xs ys) ⟩
-  (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩
+                                             (reverse-++′ xs ys) ⟩
+  (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc′ (reverse ys) (reverse xs) zs ⟩
   reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
   reverse ys ++ (xs ʳ++ zs)        ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
   ys ʳ++ (xs ʳ++ zs)               ∎
   where open CastReasoning
 
-ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
-          cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
+ʳ++-ʳ++′ : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
+           cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
+ʳ++-ʳ++′ {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-++ (+-comm m n) (reverse xs) ys) ⟩
+                                                       (reverse-++′ (reverse xs) ys) ⟩
   (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
-  (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
+  (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc′ (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
   ys ʳ++ (xs ++ zs)                          ∎
   where open CastReasoning
@@ -1318,7 +1322,7 @@ fromList-reverse List.[] = refl
 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-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨
+  fromList (List.reverse xs) ++ [ x ]           ≈⟨ unfold-∷ʳ′ x (fromList (List.reverse xs)) ⟨
   fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _)
                                                           (fromList-reverse xs) ⟩
   reverse (fromList xs) ∷ʳ x                    ≂⟨ reverse-∷ x (fromList xs) ⟨
@@ -1326,6 +1330,82 @@ fromList-reverse (x List.∷ xs) = begin
   reverse (fromList (x List.∷ xs))              ∎
   where open CastReasoning
 
+------------------------------------------------------------------------
+-- DEPRECATED STATEMENTS
+------------------------------------------------------------------------
+-- Please use the new proofs, which do not require an `eq` parameter.
+-- The next breaking version will replace `name′` with `name`.
+
+++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
+           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+++-assoc _ = ++-assoc′
+{-# WARNING_ON_USAGE ++-assoc
+"Warning: ++-assoc was deprecated in v2.2.
+Please use ++-assoc′ instead, which does not take eq."
+#-}
+
+++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
+++-identityʳ _ = ++-identityʳ′
+{-# WARNING_ON_USAGE ++-identityʳ
+"Warning: ++-identityʳ was deprecated in v2.2.
+Please use ++-identityʳ′ instead, which does not take eq."
+#-}
+
+unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
+unfold-∷ʳ _ = unfold-∷ʳ′
+{-# WARNING_ON_USAGE unfold-∷ʳ
+"Warning: unfold-∷ʳ was deprecated in v2.2.
+Please use unfold-∷ʳ′ instead, which does not take eq."
+#-}
+
+++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
+        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ _ = ++-∷ʳ′
+{-# WARNING_ON_USAGE ++-∷ʳ
+"Warning: ++-∷ʳ was deprecated in v2.2.
+Please use ++-∷ʳ′ instead, which does not take eq."
+#-}
+
+∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
+        cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
+∷ʳ-++ _ = ∷ʳ-++′
+{-# WARNING_ON_USAGE ∷ʳ-++
+"Warning: ∷ʳ-++ was deprecated in v2.2.
+Please use ∷ʳ-++′ instead, which does not take eq."
+#-}
+
+reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
+             cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
+reverse-++ _ = reverse-++′
+{-# WARNING_ON_USAGE reverse-++
+"Warning: reverse-++ was deprecated in v2.2.
+Please use reverse-++′ instead, which does not take eq."
+#-}
+
+∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
+        cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+∷-ʳ++ _ = ∷-ʳ++′
+{-# WARNING_ON_USAGE ∷-ʳ++
+"Warning: ∷-ʳ++ was deprecated in v2.2.
+Please use ∷-ʳ++′ instead, which does not take eq."
+#-}
+
+++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
+         cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
+++-ʳ++ _ = ++-ʳ++′
+{-# WARNING_ON_USAGE ++-ʳ++
+"Warning: ++-ʳ++ was deprecated in v2.2.
+Please use ++-ʳ++′ instead, which does not take eq."
+#-}
+
+ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
+          cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
+ʳ++-ʳ++ _ = ʳ++-ʳ++′
+{-# WARNING_ON_USAGE ʳ++-ʳ++
+"Warning: ʳ++-ʳ++ was deprecated in v2.2.
+Please use ʳ++-ʳ++′ instead, which does not take eq."
+#-}
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

From e6c7bf3928f5a5c1bc2d09e506fac7cda1d4c3e7 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Mon, 1 Jul 2024 14:21:10 +0200
Subject: [PATCH 2/5] remove deprecated usages

---
 .../Vec/Relation/Binary/Equality/Cast.agda     | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
index e06cdb49f0..c6f5073f86 100644
--- a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -92,7 +92,7 @@ example1a-fromList-∷ʳ x xs eq = begin
   cast eq₂ (cast eq₁ (fromList (xs List.++ List.[ x ])))
     ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
   cast eq₂ (fromList xs ++ [ x ])
-    ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
+    ≡⟨ ≈-sym (unfold-∷ʳ′ x (fromList xs)) ⟩
   fromList xs ∷ʳ x
     ∎
   where
@@ -114,7 +114,7 @@ example1b-fromList-∷ʳ x xs eq = begin
   fromList (xs List.++ List.[ x ])
     ≈⟨ fromList-++ xs ⟩
   fromList xs ++ [ x ]
-    ≈⟨ unfold-∷ʳ (+-comm 1 (List.length xs)) x (fromList xs) ⟨
+    ≈⟨ unfold-∷ʳ′ x (fromList xs) ⟨
   fromList xs ∷ʳ x
     ∎
   where open CastReasoning
@@ -138,8 +138,8 @@ example1b-fromList-∷ʳ x xs eq = begin
 example2a : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
             cast eq ((reverse xs ∷ʳ a) ++ ys) ≡ reverse xs ++ (a ∷ ys)
 example2a eq xs a ys = begin
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n
-  reverse xs ++ (a ∷ ys)  ∎                            -- index: m + suc n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++′ a (reverse xs) ⟩ -- index: suc m + n
+  reverse xs ++ (a ∷ ys)  ∎                          -- index: m + suc n
   where open CastReasoning
 
 -- To interoperate with `_≡_`, this library provides `_≂⟨_⟩_` (\-~) for
@@ -158,7 +158,7 @@ example2b : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
 example2b eq xs a ys = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩          -- index: suc m + n
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩  -- index: suc m + n
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩         -- index: suc m + n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++′ a (reverse xs) ⟩           -- index: suc m + n
   reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨          -- index: m + suc n
   xs ʳ++ (a ∷ ys)         ∎                                    -- index: m + suc n
   where open CastReasoning
@@ -220,9 +220,9 @@ 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-∷ʳ _ a xs)) ⟨
+                                                     (unfold-∷ʳ′ a xs)) ⟨
   reverse ((xs ∷ʳ a) ++ ys)
-    ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
+    ≈⟨ reverse-++′ (xs ∷ʳ a) ys ⟩
   reverse ys ++ reverse (xs ∷ʳ a)
     ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
   ys ʳ++ reverse (xs ∷ʳ a)
@@ -264,9 +264,9 @@ example6a-reverse-∷ʳ {n = n} x xs = begin-≡
   reverse (xs ∷ʳ x)
     ≡⟨ ≈-reflexive refl ⟨
   reverse (xs ∷ʳ x)
-    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
+    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ′ x xs) ⟩
   reverse (xs ++ [ x ])
-    ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
+    ≈⟨ reverse-++′ xs [ x ] ⟩
   x ∷ reverse xs
     ∎
   where open CastReasoning

From 03baf8bd3919e68ec3adeb23674e0caff669a367 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Fri, 5 Jul 2024 16:52:02 +0200
Subject: [PATCH 3/5] use '-eqFree' as suffix instead of a prime

---
 .../Vec/Relation/Binary/Equality/Cast.agda    |  18 +--
 src/Data/Vec/Properties.agda                  | 121 +++++++++---------
 2 files changed, 70 insertions(+), 69 deletions(-)

diff --git a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
index c6f5073f86..0852f68166 100644
--- a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -92,7 +92,7 @@ example1a-fromList-∷ʳ x xs eq = begin
   cast eq₂ (cast eq₁ (fromList (xs List.++ List.[ x ])))
     ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
   cast eq₂ (fromList xs ++ [ x ])
-    ≡⟨ ≈-sym (unfold-∷ʳ′ x (fromList xs)) ⟩
+    ≡⟨ ≈-sym (unfold-∷ʳ-eqFree x (fromList xs)) ⟩
   fromList xs ∷ʳ x
     ∎
   where
@@ -114,7 +114,7 @@ example1b-fromList-∷ʳ x xs eq = begin
   fromList (xs List.++ List.[ x ])
     ≈⟨ fromList-++ xs ⟩
   fromList xs ++ [ x ]
-    ≈⟨ unfold-∷ʳ′ x (fromList xs) ⟨
+    ≈⟨ unfold-∷ʳ-eqFree x (fromList xs) ⟨
   fromList xs ∷ʳ x
     ∎
   where open CastReasoning
@@ -138,8 +138,8 @@ example1b-fromList-∷ʳ x xs eq = begin
 example2a : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
             cast eq ((reverse xs ∷ʳ a) ++ ys) ≡ reverse xs ++ (a ∷ ys)
 example2a eq xs a ys = begin
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++′ a (reverse xs) ⟩ -- index: suc m + n
-  reverse xs ++ (a ∷ ys)  ∎                          -- index: m + suc n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩ -- index: suc m + n
+  reverse xs ++ (a ∷ ys)  ∎                                -- index: m + suc n
   where open CastReasoning
 
 -- To interoperate with `_≡_`, this library provides `_≂⟨_⟩_` (\-~) for
@@ -158,7 +158,7 @@ example2b : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
 example2b eq xs a ys = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩          -- index: suc m + n
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩  -- index: suc m + n
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++′ a (reverse xs) ⟩           -- index: suc m + n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩     -- index: suc m + n
   reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨          -- index: m + suc n
   xs ʳ++ (a ∷ ys)         ∎                                    -- index: m + suc n
   where open CastReasoning
@@ -220,9 +220,9 @@ 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-∷ʳ′ a xs)) ⟨
+                                                     (unfold-∷ʳ-eqFree a xs)) ⟨
   reverse ((xs ∷ʳ a) ++ ys)
-    ≈⟨ reverse-++′ (xs ∷ʳ a) ys ⟩
+    ≈⟨ reverse-++-eqFree (xs ∷ʳ a) ys ⟩
   reverse ys ++ reverse (xs ∷ʳ a)
     ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
   ys ʳ++ reverse (xs ∷ʳ a)
@@ -264,9 +264,9 @@ example6a-reverse-∷ʳ {n = n} x xs = begin-≡
   reverse (xs ∷ʳ x)
     ≡⟨ ≈-reflexive refl ⟨
   reverse (xs ∷ʳ x)
-    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ′ x xs) ⟩
+    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ-eqFree x xs) ⟩
   reverse (xs ++ [ x ])
-    ≈⟨ reverse-++′ xs [ x ] ⟩
+    ≈⟨ reverse-++-eqFree xs [ x ] ⟩
   x ∷ reverse xs
     ∎
   where open CastReasoning
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index c245bd323b..2151c49463 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -468,14 +468,14 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 ++-injective ws xs eq =
   (++-injectiveˡ ws xs eq , ++-injectiveʳ ws xs eq)
 
-++-assoc′ : ∀ (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) → let eq = +-assoc m n o in
-            cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-++-assoc′ []       ys zs = cast-is-id refl (ys ++ zs)
-++-assoc′ (x ∷ xs) ys zs = cong (x ∷_) (++-assoc′ xs ys zs)
+++-assoc-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) → let eq = +-assoc m n o in
+                  cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+++-assoc-eqFree []       ys zs = cast-is-id refl (ys ++ zs)
+++-assoc-eqFree (x ∷ xs) ys zs = cong (x ∷_) (++-assoc-eqFree xs ys zs)
 
-++-identityʳ′ : ∀ (xs : Vec A n) → cast (+-identityʳ n) (xs ++ []) ≡ xs
-++-identityʳ′ []       = refl
-++-identityʳ′ (x ∷ xs) = cong (x ∷_) (++-identityʳ′ xs)
+++-identityʳ-eqFree : ∀ (xs : Vec A n) → cast (+-identityʳ n) (xs ++ []) ≡ xs
+++-identityʳ-eqFree []       = refl
+++-identityʳ-eqFree (x ∷ xs) = cong (x ∷_) (++-identityʳ-eqFree xs)
 
 cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
            cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
@@ -869,9 +869,9 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
 
 -- snoc is snoc
 
-unfold-∷ʳ′ : ∀ x (xs : Vec A n) → cast (+-comm 1 n) (xs ∷ʳ x) ≡ xs ++ [ x ]
-unfold-∷ʳ′ x []       = refl
-unfold-∷ʳ′ x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ′ x xs)
+unfold-∷ʳ-eqFree : ∀ x (xs : Vec A n) → cast (+-comm 1 n) (xs ∷ʳ x) ≡ xs ++ [ x ]
+unfold-∷ʳ-eqFree x []       = refl
+unfold-∷ʳ-eqFree x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ-eqFree x xs)
 
 ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
 ∷ʳ-injective []       []        refl = (refl , refl)
@@ -919,16 +919,16 @@ cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq
 
 -- _++_ and _∷ʳ_
 
-++-∷ʳ′ : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
-         cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
-++-∷ʳ′ {m = zero}  z []       []       = refl
-++-∷ʳ′ {m = zero}  z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ′ z [] ys)
-++-∷ʳ′ {m = suc m} z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ′ z xs ys)
+++-∷ʳ-eqFree : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
+               cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ-eqFree {m = zero}  z []       []       = refl
+++-∷ʳ-eqFree {m = zero}  z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ-eqFree z [] ys)
+++-∷ʳ-eqFree {m = suc m} z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ-eqFree z xs ys)
 
-∷ʳ-++′ : ∀ a (xs : Vec A n) {ys : Vec A m} → let eq = sym (+-suc n m) in
-         cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
-∷ʳ-++′ a []       {ys} = cong (a ∷_) (cast-is-id refl ys)
-∷ʳ-++′ a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++′ a xs)
+∷ʳ-++-eqFree : ∀ a (xs : Vec A n) {ys : Vec A m} → let eq = sym (+-suc n m) in
+               cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
+∷ʳ-++-eqFree a []       {ys} = cong (a ∷_) (cast-is-id refl ys)
+∷ʳ-++-eqFree a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++-eqFree a xs)
 
 ------------------------------------------------------------------------
 -- reverse
@@ -1014,14 +1014,14 @@ map-reverse f (x ∷ xs) = begin
 
 -- append and reverse
 
-reverse-++′ : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
-              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++′ {m = zero}  {n = n} []       ys = ≈-sym (++-identityʳ′ (reverse ys))
-reverse-++′ {m = suc m} {n = n} (x ∷ xs) ys = begin
+reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
+                    cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
+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-++′ xs ys) ⟩
-  (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ′ x (reverse ys) (reverse xs) ⟩
+                                                (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
@@ -1065,37 +1065,37 @@ map-ʳ++ {ys = ys} f xs = begin
   map f xs ʳ++ map f ys          ∎
   where open ≡-Reasoning
 
-∷-ʳ++′ : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
-         cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++′ a xs {ys} = begin
+∷-ʳ++-eqFree : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
+               cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+∷-ʳ++-eqFree a xs {ys} = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++′ a (reverse xs) ⟩
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩
   reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨
   xs ʳ++ (a ∷ ys)         ∎
   where open CastReasoning
 
-++-ʳ++′ : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
-          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++′ {m = m} {n} {o} xs {ys} {zs} = begin
+++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
+                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-++′ xs ys) ⟩
-  (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc′ (reverse ys) (reverse xs) 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) ⟨
   ys ʳ++ (xs ʳ++ zs)               ∎
   where open CastReasoning
 
-ʳ++-ʳ++′ : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
-           cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++′ {m = m} {n} {o} xs {ys} {zs} = begin
+ʳ++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
+                 cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
+ʳ++-ʳ++-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-++′ (reverse xs) ys) ⟩
+                                                       (reverse-++-eqFree (reverse xs) ys) ⟩
   (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
-  (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc′ (reverse ys) xs zs ⟩
+  (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc-eqFree (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
   ys ʳ++ (xs ++ zs)                          ∎
   where open CastReasoning
@@ -1322,7 +1322,7 @@ fromList-reverse List.[] = refl
 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-∷ʳ′ 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) ⟩
   reverse (fromList xs) ∷ʳ x                    ≂⟨ reverse-∷ x (fromList xs) ⟨
@@ -1331,79 +1331,80 @@ fromList-reverse (x List.∷ xs) = begin
   where open CastReasoning
 
 ------------------------------------------------------------------------
--- DEPRECATED STATEMENTS
+-- TRANSITION TO EQ-FREE LEMMA
 ------------------------------------------------------------------------
 -- Please use the new proofs, which do not require an `eq` parameter.
--- The next breaking version will replace `name′` with `name`.
+-- In v3, `name` will be changed to be the same lemma as `name-eqFree`,
+-- and `name-eqFree` will be deprecated.
 
 ++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
            cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-++-assoc _ = ++-assoc′
+++-assoc _ = ++-assoc-eqFree
 {-# WARNING_ON_USAGE ++-assoc
 "Warning: ++-assoc was deprecated in v2.2.
-Please use ++-assoc′ instead, which does not take eq."
+Please use ++-assoc-eqFree instead, which does not take eq."
 #-}
 
 ++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
-++-identityʳ _ = ++-identityʳ′
+++-identityʳ _ = ++-identityʳ-eqFree
 {-# WARNING_ON_USAGE ++-identityʳ
 "Warning: ++-identityʳ was deprecated in v2.2.
-Please use ++-identityʳ′ instead, which does not take eq."
+Please use ++-identityʳ-eqFree instead, which does not take eq."
 #-}
 
 unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
-unfold-∷ʳ _ = unfold-∷ʳ′
+unfold-∷ʳ _ = unfold-∷ʳ-eqFree
 {-# WARNING_ON_USAGE unfold-∷ʳ
 "Warning: unfold-∷ʳ was deprecated in v2.2.
-Please use unfold-∷ʳ′ instead, which does not take eq."
+Please use unfold-∷ʳ-eqFree instead, which does not take eq."
 #-}
 
 ++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
         cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
-++-∷ʳ _ = ++-∷ʳ′
+++-∷ʳ _ = ++-∷ʳ-eqFree
 {-# WARNING_ON_USAGE ++-∷ʳ
 "Warning: ++-∷ʳ was deprecated in v2.2.
-Please use ++-∷ʳ′ instead, which does not take eq."
+Please use ++-∷ʳ-eqFree instead, which does not take eq."
 #-}
 
 ∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
         cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
-∷ʳ-++ _ = ∷ʳ-++′
+∷ʳ-++ _ = ∷ʳ-++-eqFree
 {-# WARNING_ON_USAGE ∷ʳ-++
 "Warning: ∷ʳ-++ was deprecated in v2.2.
-Please use ∷ʳ-++′ instead, which does not take eq."
+Please use ∷ʳ-++-eqFree instead, which does not take eq."
 #-}
 
 reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ _ = reverse-++′
+reverse-++ _ = reverse-++-eqFree
 {-# WARNING_ON_USAGE reverse-++
 "Warning: reverse-++ was deprecated in v2.2.
-Please use reverse-++′ instead, which does not take eq."
+Please use reverse-++-eqFree instead, which does not take eq."
 #-}
 
 ∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
         cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++ _ = ∷-ʳ++′
+∷-ʳ++ _ = ∷-ʳ++-eqFree
 {-# WARNING_ON_USAGE ∷-ʳ++
 "Warning: ∷-ʳ++ was deprecated in v2.2.
-Please use ∷-ʳ++′ instead, which does not take eq."
+Please use ∷-ʳ++-eqFree instead, which does not take eq."
 #-}
 
 ++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++ _ = ++-ʳ++′
+++-ʳ++ _ = ++-ʳ++-eqFree
 {-# WARNING_ON_USAGE ++-ʳ++
 "Warning: ++-ʳ++ was deprecated in v2.2.
-Please use ++-ʳ++′ instead, which does not take eq."
+Please use ++-ʳ++-eqFree instead, which does not take eq."
 #-}
 
 ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
           cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++ _ = ʳ++-ʳ++′
+ʳ++-ʳ++ _ = ʳ++-ʳ++-eqFree
 {-# WARNING_ON_USAGE ʳ++-ʳ++
 "Warning: ʳ++-ʳ++ was deprecated in v2.2.
-Please use ʳ++-ʳ++′ instead, which does not take eq."
+Please use ʳ++-ʳ++-eqFree instead, which does not take eq."
 #-}
 
 ------------------------------------------------------------------------

From 8693e3ec8b23424c4f607d8debd4339b5b968350 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Fri, 5 Jul 2024 17:16:48 +0200
Subject: [PATCH 4/5] rename 'name-eqFree' to 'name'

(while leaving 'name-eqFree' as a deprecated synonym)
---
 .../Vec/Relation/Binary/Equality/Cast.agda    |  18 +-
 src/Data/Vec/Properties.agda                  | 205 ++++++++----------
 2 files changed, 97 insertions(+), 126 deletions(-)

diff --git a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
index 0852f68166..97849fe20a 100644
--- a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -92,7 +92,7 @@ example1a-fromList-∷ʳ x xs eq = begin
   cast eq₂ (cast eq₁ (fromList (xs List.++ List.[ x ])))
     ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
   cast eq₂ (fromList xs ++ [ x ])
-    ≡⟨ ≈-sym (unfold-∷ʳ-eqFree x (fromList xs)) ⟩
+    ≡⟨ ≈-sym (unfold-∷ʳ x (fromList xs)) ⟩
   fromList xs ∷ʳ x
     ∎
   where
@@ -114,7 +114,7 @@ example1b-fromList-∷ʳ x xs eq = begin
   fromList (xs List.++ List.[ x ])
     ≈⟨ fromList-++ xs ⟩
   fromList xs ++ [ x ]
-    ≈⟨ unfold-∷ʳ-eqFree x (fromList xs) ⟨
+    ≈⟨ unfold-∷ʳ x (fromList xs) ⟨
   fromList xs ∷ʳ x
     ∎
   where open CastReasoning
@@ -138,8 +138,8 @@ example1b-fromList-∷ʳ x xs eq = begin
 example2a : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
             cast eq ((reverse xs ∷ʳ a) ++ ys) ≡ reverse xs ++ (a ∷ ys)
 example2a eq xs a ys = begin
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩ -- index: suc m + n
-  reverse xs ++ (a ∷ ys)  ∎                                -- index: m + suc n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ a (reverse xs) ⟩ -- index: suc m + n
+  reverse xs ++ (a ∷ ys)  ∎                         -- index: m + suc n
   where open CastReasoning
 
 -- To interoperate with `_≡_`, this library provides `_≂⟨_⟩_` (\-~) for
@@ -158,7 +158,7 @@ example2b : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
 example2b eq xs a ys = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩          -- index: suc m + n
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩  -- index: suc m + n
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩     -- index: suc m + n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ a (reverse xs) ⟩            -- index: suc m + n
   reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨          -- index: m + suc n
   xs ʳ++ (a ∷ ys)         ∎                                    -- index: m + suc n
   where open CastReasoning
@@ -220,9 +220,9 @@ 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)) ⟨
+                                                     (unfold-∷ʳ a xs)) ⟨
   reverse ((xs ∷ʳ a) ++ ys)
-    ≈⟨ reverse-++-eqFree (xs ∷ʳ a) ys ⟩
+    ≈⟨ reverse-++ (xs ∷ʳ a) ys ⟩
   reverse ys ++ reverse (xs ∷ʳ a)
     ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
   ys ʳ++ reverse (xs ∷ʳ a)
@@ -264,9 +264,9 @@ 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 (cast-reverse _ _) (unfold-∷ʳ x xs) ⟩
   reverse (xs ++ [ x ])
-    ≈⟨ reverse-++-eqFree xs [ x ] ⟩
+    ≈⟨ reverse-++ xs [ x ] ⟩
   x ∷ reverse xs
     ∎
   where open CastReasoning
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 2151c49463..c6e058a48a 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -468,14 +468,14 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 ++-injective ws xs eq =
   (++-injectiveˡ ws xs eq , ++-injectiveʳ ws xs eq)
 
-++-assoc-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) → let eq = +-assoc m n o in
-                  cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-++-assoc-eqFree []       ys zs = cast-is-id refl (ys ++ zs)
-++-assoc-eqFree (x ∷ xs) ys zs = cong (x ∷_) (++-assoc-eqFree xs ys zs)
+++-assoc : ∀ (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) → let eq = +-assoc m n o in
+           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+++-assoc []       ys zs = cast-is-id refl (ys ++ zs)
+++-assoc (x ∷ xs) ys zs = cong (x ∷_) (++-assoc xs ys zs)
 
-++-identityʳ-eqFree : ∀ (xs : Vec A n) → cast (+-identityʳ n) (xs ++ []) ≡ xs
-++-identityʳ-eqFree []       = refl
-++-identityʳ-eqFree (x ∷ xs) = cong (x ∷_) (++-identityʳ-eqFree xs)
+++-identityʳ : ∀ (xs : Vec A n) → cast (+-identityʳ n) (xs ++ []) ≡ xs
+++-identityʳ []       = refl
+++-identityʳ (x ∷ xs) = cong (x ∷_) (++-identityʳ xs)
 
 cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
            cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
@@ -869,9 +869,9 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
 
 -- snoc is snoc
 
-unfold-∷ʳ-eqFree : ∀ x (xs : Vec A n) → cast (+-comm 1 n) (xs ∷ʳ x) ≡ xs ++ [ x ]
-unfold-∷ʳ-eqFree x []       = refl
-unfold-∷ʳ-eqFree x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ-eqFree x xs)
+unfold-∷ʳ : ∀ x (xs : Vec A n) → cast (+-comm 1 n) (xs ∷ʳ x) ≡ xs ++ [ x ]
+unfold-∷ʳ x []       = refl
+unfold-∷ʳ x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ x xs)
 
 ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
 ∷ʳ-injective []       []        refl = (refl , refl)
@@ -919,16 +919,16 @@ cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq
 
 -- _++_ and _∷ʳ_
 
-++-∷ʳ-eqFree : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
-               cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
-++-∷ʳ-eqFree {m = zero}  z []       []       = refl
-++-∷ʳ-eqFree {m = zero}  z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ-eqFree z [] ys)
-++-∷ʳ-eqFree {m = suc m} z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ-eqFree z xs ys)
+++-∷ʳ : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
+        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ {m = zero}  z []       []       = refl
+++-∷ʳ {m = zero}  z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ z [] ys)
+++-∷ʳ {m = suc m} z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ z xs ys)
 
-∷ʳ-++-eqFree : ∀ a (xs : Vec A n) {ys : Vec A m} → let eq = sym (+-suc n m) in
-               cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
-∷ʳ-++-eqFree a []       {ys} = cong (a ∷_) (cast-is-id refl ys)
-∷ʳ-++-eqFree a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++-eqFree a xs)
+∷ʳ-++ : ∀ a (xs : Vec A n) {ys : Vec A m} → let eq = sym (+-suc n m) in
+        cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
+∷ʳ-++ a []       {ys} = cong (a ∷_) (cast-is-id refl ys)
+∷ʳ-++ a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++ a xs)
 
 ------------------------------------------------------------------------
 -- reverse
@@ -1014,14 +1014,14 @@ map-reverse f (x ∷ xs) = begin
 
 -- append and reverse
 
-reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
-                    cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++-eqFree {m = zero}  {n = n} []       ys = ≈-sym (++-identityʳ-eqFree (reverse ys))
-reverse-++-eqFree {m = suc m} {n = n} (x ∷ xs) ys = begin
+reverse-++ : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
+             cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
+reverse-++ {m = zero}  {n = n} []       ys = ≈-sym (++-identityʳ (reverse ys))
+reverse-++ {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 ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ-eqFree x (reverse ys) (reverse xs) ⟩
+                                                (reverse-++ xs ys) ⟩
+  (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
   reverse ys ++ (reverse (x ∷ xs))    ∎
   where open CastReasoning
@@ -1065,37 +1065,37 @@ map-ʳ++ {ys = ys} f xs = begin
   map f xs ʳ++ map f ys          ∎
   where open ≡-Reasoning
 
-∷-ʳ++-eqFree : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
-               cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++-eqFree a xs {ys} = begin
+∷-ʳ++ : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in
+        cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+∷-ʳ++ a xs {ys} = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
-  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ a (reverse xs) ⟩
   reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨
   xs ʳ++ (a ∷ ys)         ∎
   where open CastReasoning
 
-++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
-                cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
+++-ʳ++ : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
+         cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
+++-ʳ++ {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 ys ++ reverse xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) (reverse xs) zs ⟩
+                                             (reverse-++ xs ys) ⟩
+  (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (reverse ys) (reverse xs) zs ⟩
   reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
   reverse ys ++ (xs ʳ++ zs)        ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
   ys ʳ++ (xs ʳ++ zs)               ∎
   where open CastReasoning
 
-ʳ++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
-                 cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
+ʳ++-ʳ++ : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
+          cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
+ʳ++-ʳ++ {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) ⟩
   (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                   ≈⟨ ++-assoc (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
   ys ʳ++ (xs ++ zs)                          ∎
   where open CastReasoning
@@ -1322,7 +1322,7 @@ fromList-reverse List.[] = refl
 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 ]           ≈⟨ unfold-∷ʳ x (fromList (List.reverse xs)) ⟨
   fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _)
                                                           (fromList-reverse xs) ⟩
   reverse (fromList xs) ∷ʳ x                    ≂⟨ reverse-∷ x (fromList xs) ⟨
@@ -1330,83 +1330,6 @@ fromList-reverse (x List.∷ xs) = begin
   reverse (fromList (x List.∷ xs))              ∎
   where open CastReasoning
 
-------------------------------------------------------------------------
--- TRANSITION TO EQ-FREE LEMMA
-------------------------------------------------------------------------
--- Please use the new proofs, which do not require an `eq` parameter.
--- In v3, `name` will be changed to be the same lemma as `name-eqFree`,
--- and `name-eqFree` will be deprecated.
-
-++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
-           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-++-assoc _ = ++-assoc-eqFree
-{-# WARNING_ON_USAGE ++-assoc
-"Warning: ++-assoc was deprecated in v2.2.
-Please use ++-assoc-eqFree instead, which does not take eq."
-#-}
-
-++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
-++-identityʳ _ = ++-identityʳ-eqFree
-{-# WARNING_ON_USAGE ++-identityʳ
-"Warning: ++-identityʳ was deprecated in v2.2.
-Please use ++-identityʳ-eqFree instead, which does not take eq."
-#-}
-
-unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
-unfold-∷ʳ _ = unfold-∷ʳ-eqFree
-{-# WARNING_ON_USAGE unfold-∷ʳ
-"Warning: unfold-∷ʳ was deprecated in v2.2.
-Please use unfold-∷ʳ-eqFree instead, which does not take eq."
-#-}
-
-++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
-        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
-++-∷ʳ _ = ++-∷ʳ-eqFree
-{-# WARNING_ON_USAGE ++-∷ʳ
-"Warning: ++-∷ʳ was deprecated in v2.2.
-Please use ++-∷ʳ-eqFree instead, which does not take eq."
-#-}
-
-∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
-        cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
-∷ʳ-++ _ = ∷ʳ-++-eqFree
-{-# WARNING_ON_USAGE ∷ʳ-++
-"Warning: ∷ʳ-++ was deprecated in v2.2.
-Please use ∷ʳ-++-eqFree instead, which does not take eq."
-#-}
-
-reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
-             cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ _ = reverse-++-eqFree
-{-# WARNING_ON_USAGE reverse-++
-"Warning: reverse-++ was deprecated in v2.2.
-Please use reverse-++-eqFree instead, which does not take eq."
-#-}
-
-∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
-        cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++ _ = ∷-ʳ++-eqFree
-{-# WARNING_ON_USAGE ∷-ʳ++
-"Warning: ∷-ʳ++ was deprecated in v2.2.
-Please use ∷-ʳ++-eqFree instead, which does not take eq."
-#-}
-
-++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
-         cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++ _ = ++-ʳ++-eqFree
-{-# WARNING_ON_USAGE ++-ʳ++
-"Warning: ++-ʳ++ was deprecated in v2.2.
-Please use ++-ʳ++-eqFree instead, which does not take eq."
-#-}
-
-ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
-          cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++ _ = ʳ++-ʳ++-eqFree
-{-# WARNING_ON_USAGE ʳ++-ʳ++
-"Warning: ʳ++-ʳ++ was deprecated in v2.2.
-Please use ʳ++-ʳ++-eqFree instead, which does not take eq."
-#-}
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
@@ -1532,3 +1455,51 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin
 "Warning: lookup-inject≤-take was deprecated in v2.0.
 Please use lookup-take-inject≤ or lookup-truncate, take≡truncate instead."
 #-}
+
+-- Version 3.0
+
+++-assoc-eqFree = ++-assoc
+{-# WARNING_ON_USAGE ++-assoc-eqFree
+"Warning: ++-assoc-eqFree was deprecated in v3.0.
+Please use ++-assoc instead."
+#-}
+++-identityʳ-eqFree = ++-identityʳ
+{-# WARNING_ON_USAGE ++-identityʳ-eqFree
+"Warning: ++-identityʳ-eqFree was deprecated in v3.0.
+Please use ++-identityʳ instead."
+#-}
+unfold-∷ʳ-eqFree = unfold-∷ʳ
+{-# WARNING_ON_USAGE unfold-∷ʳ-eqFree
+"Warning: unfold-∷ʳ-eqFree was deprecated in v3.0.
+Please use unfold-∷ʳ instead."
+#-}
+++-∷ʳ-eqFree = ++-∷ʳ
+{-# WARNING_ON_USAGE ++-∷ʳ-eqFree
+"Warning: ++-∷ʳ-eqFree was deprecated in v3.0.
+Please use ++-∷ʳ instead."
+#-}
+∷ʳ-++-eqFree = ∷ʳ-++
+{-# WARNING_ON_USAGE ∷ʳ-++-eqFree
+"Warning: ∷ʳ-++-eqFree was deprecated in v3.0.
+Please use ∷ʳ-++ instead."
+#-}
+reverse-++-eqFree = reverse-++
+{-# WARNING_ON_USAGE reverse-++-eqFree
+"Warning: reverse-++-eqFree was deprecated in v3.0.
+Please use reverse-++ instead."
+#-}
+∷-ʳ++-eqFree = ∷-ʳ++
+{-# WARNING_ON_USAGE ∷-ʳ++-eqFree
+"Warning: ∷-ʳ++-eqFree was deprecated in v3.0.
+Please use ∷-ʳ++ instead."
+#-}
+++-ʳ++-eqFree = ++-ʳ++
+{-# WARNING_ON_USAGE ++-ʳ++-eqFree
+"Warning: ++-ʳ++-eqFree was deprecated in v3.0.
+Please use ++-ʳ++ instead."
+#-}
+ʳ++-ʳ++-eqFree = ʳ++-ʳ++
+{-# WARNING_ON_USAGE ʳ++-ʳ++-eqFree
+"Warning: ʳ++-ʳ++-eqFree was deprecated in v3.0.
+Please use ʳ++-ʳ++ instead."
+#-}

From 1dfdc694a29e48e8e80032d729fb3a404c1a175e Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 7 Jul 2024 23:25:53 +0200
Subject: [PATCH 5/5] add changelog entry

---
 CHANGELOG.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d5851dde0d..aea84b26d5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -148,6 +148,19 @@ Deprecated names
   toDec    ↦  Relation.Nullary.Decidable.Core.fromSum
   ```
 
+* In `Data.Vec.Properties`:
+  ```agda
+  ++-assoc-eqFree      ↦  ++-assoc
+  ++-identityʳ-eqFree  ↦  ++-identityʳ
+  unfold-∷ʳ-eqFree     ↦  unfold-∷ʳ
+  ++-∷ʳ-eqFree         ↦  ++-∷ʳ
+  ∷ʳ-++-eqFree         ↦  ∷ʳ-++
+  reverse-++-eqFree    ↦  reverse-++
+  ∷-ʳ++-eqFree         ↦  ∷-ʳ++
+  ++-ʳ++-eqFree        ↦  ++-ʳ++
+  ʳ++-ʳ++-eqFree       ↦  ʳ++-ʳ++
+  ```
+
 * In `IO.Base`:
   ```agda
   untilRight  ↦  untilInj₂