Rename take-drop-id and take++drop (#2069)

A useful improvement to consistency of names,

Author: Saransh-cpp

CHANGELOG.md

@@ -1246,6 +1246,8 @@ Deprecated names
 
   zipWith-identityˡ  ↦  zipWith-zeroˡ
   zipWith-identityʳ  ↦  zipWith-zeroʳ
+
+  take++drop ↦ take++drop≡id
   ```
 
 * In `Data.List.NonEmpty.Properties`:
@@ -1401,6 +1403,8 @@ Deprecated names
   []≔-++-raise    ↦ []≔-++-↑ʳ
   idIsFold        ↦ id-is-foldr
   sum-++-commute  ↦ sum-++
+
+  take-drop-id ↦ take++drop≡id
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```

README/Data/List.agda

@@ -48,7 +48,7 @@ lem₅ = refl
 open import Data.List.Properties
 
 lem₆ : ∀ n (xs : List ℕ) → take n xs ++ drop n xs ≡ xs
-lem₆ = take++drop
+lem₆ = take++drop≡id
 
 lem₇ : ∀ (xs : List ℕ) → reverse (reverse xs) ≡ xs
 lem₇ = reverse-involutive

src/Data/List/Properties.agda

@@ -813,10 +813,10 @@ drop-[] : ∀ m → drop {A = A} m [] ≡ []
 drop-[] zero = refl
 drop-[] (suc m) = refl
 
-take++drop : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
-take++drop zero    xs       = refl
-take++drop (suc n) []       = refl
-take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
+take++drop≡id : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
+take++drop≡id zero    xs       = refl
+take++drop≡id (suc n) []       = refl
+take++drop≡id (suc n) (x ∷ xs) = cong (x ∷_) (take++drop≡id n xs)
 
 drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
            drop m (take (suc m) xs) ≡ [ lookup xs i ]
@@ -1212,3 +1212,9 @@ zipWith-identityʳ = zipWith-zeroʳ
 "Warning: zipWith-identityʳ was deprecated in v2.0.
 Please use zipWith-zeroʳ instead."
 #-}
+
+take++drop = take++drop≡id
+{-# WARNING_ON_USAGE take++drop
+"Warning: take++drop was deprecated in v2.0.
+Please use take++drop≡id instead."
+#-}

src/Data/Vec/Properties.agda

@@ -140,15 +140,15 @@ drop-distr-map f (suc m) (x ∷ xs) = begin
 ------------------------------------------------------------------------
 -- take and drop together
 
-take-drop-id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
-take-drop-id zero x = refl
-take-drop-id (suc m) (x ∷ xs) = begin
+take++drop≡id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
+take++drop≡id zero x = refl
+take++drop≡id (suc m) (x ∷ xs) = begin
     take (suc m) (x ∷ xs) ++ drop (suc m) (x ∷ xs)
   ≡⟨ cong₂ _++_ (unfold-take m x xs) (unfold-drop m x xs) ⟩
     (x ∷ take m xs) ++ (drop m xs)
   ≡⟨⟩
     x ∷ (take m xs ++ drop m xs)
-  ≡⟨ cong (x ∷_) (take-drop-id m xs) ⟩
+  ≡⟨ cong (x ∷_) (take++drop≡id m xs) ⟩
     x ∷ xs
   ∎
 
@@ -1186,3 +1186,9 @@ sum-++-commute = sum-++
 "Warning: sum-++-commute was deprecated in v2.0.
 Please use sum-++ instead."
 #-}
+
+take-drop-id = take++drop≡id
+{-# WARNING_ON_USAGE take-drop-id
+"Warning: take-drop-id was deprecated in v2.0.
+Please use take++drop≡id instead."
+#-}