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

A useful improvement to consistency of names,

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."
+#-}