Add drop-drop in Data.List.Properties

CHANGELOG.md

@@ -1080,12 +1080,14 @@ Deprecated names
  ```agda
  map-identity ↦ map-id
  map-fusion ↦ map-∘
+ drop-fusion ↦ drop-drop
  ```
 
 * In `Codata.Sized.Colist.Properties`:
  ```agda
- map-identity ↦ map-id
- map-map-fusion ↦ map-∘
+ map-identity ↦ map-id
+ map-map-fusion ↦ map-∘
+ drop-drop-fusion ↦ drop-drop
  ```
 
 * In `Codata.Sized.Covec.Properties`:
@@ -2216,24 +2218,26 @@ Other minor changes
  concatMap-map : concatMap g (map f xs) ≡ concatMap (g ∘′ f) xs
  map-concatMap : map f ∘′ concatMap g ≗ concatMap (map f ∘′ g)
 
- length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
+ length-isMagmaHomomorphism  : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
  length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
  
  take-map : take n (map f xs) ≡ map f (take n xs)
  drop-map : drop n (map f xs) ≡ map f (drop n xs)
  head-map : head (map f xs) ≡ Maybe.map f (head xs)
 
- take-suc : (o : Fin (length xs)) → let m = toℕ o in take (suc m) xs ≡ take m xs ∷ʳ lookup xs o
- take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o
- drop-take-suc : (o : Fin (length xs)) → let m = toℕ o in drop m (take (suc m) xs) ≡ [ lookup xs o ]
- drop-take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in drop m (take (suc m) (tabulate f)) ≡ [ f o ]
+ take-suc  : take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
+ take-suc-tabulate  : take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
+ drop-take-suc  : drop m (take (suc m) xs) ≡ [ lookup xs i ]
+ drop-take-suc-tabulate : drop m (take (suc m) (tabulate f)) ≡ [ f i ]
 
  take-all : n ≥ length xs → take n xs ≡ xs
 
- take-[] : ∀ m → take  m [] ≡ []
- drop-[] : ∀ m → drop  m [] ≡ []
+ take-[] : take m [] ≡ []
+ drop-[] : drop m [] ≡ []
 
  map-replicate : map f (replicate n x) ≡ replicate n (f x)
+
+ drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
  ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:

src/Codata/Guarded/Stream/Properties.agda

@@ -268,9 +268,9 @@ take-zipWith (suc n) f as bs =
 ------------------------------------------------------------------------
 -- Properties of drop
 
-drop-fusion : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as
-drop-fusion zero n as = P.refl
-drop-fusion (suc m) n as = drop-fusion m n (as .tail)
+drop-drop : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as
+drop-drop zero n as = P.refl
+drop-drop (suc m) n as = drop-drop m n (as .tail)
 
 drop-zipWith : ∀ n (f : A → B → C) as bs →
  drop n (zipWith f as bs) ≡ zipWith f (drop n as) (drop n bs)
@@ -331,3 +331,9 @@ map-fusion = map-∘
 "Warning: map-fusion was deprecated in v2.0.
 Please use map-∘ instead."
 #-}
+
+drop-fusion = drop-drop
+{-# WARNING_ON_USAGE drop-fusion
+"Warning: drop-fusion was deprecated in v2.0.
+Please use drop-drop instead."
+#-}

src/Codata/Sized/Colist/Properties.agda

@@ -197,11 +197,11 @@ drop-nil : ∀ m → i ⊢ drop {A = A} m [] ≈ []
 drop-nil zero = []
 drop-nil (suc m) = []
 
-drop-drop-fusion : ∀ m n (as : Colist A ∞) →
+drop-drop : ∀ m n (as : Colist A ∞) →
  i ⊢ drop n (drop m as) ≈ drop (m ℕ.+ n) as
-drop-drop-fusion zero n as = refl
-drop-drop-fusion (suc m) n [] = drop-nil n
-drop-drop-fusion (suc m) n (a ∷ as) = drop-drop-fusion m n (as .force)
+drop-drop zero n as = refl
+drop-drop (suc m) n [] = drop-nil n
+drop-drop (suc m) n (a ∷ as) = drop-drop m n (as .force)
 
 map-drop : ∀ (f : A → B) m as → i ⊢ map f (drop m as) ≈ drop m (map f as)
 map-drop f zero as = refl
@@ -351,3 +351,9 @@ map-map-fusion = map-∘
 "Warning: map-map-fusion was deprecated in v2.0.
 Please use map-∘ instead."
 #-}
+
+drop-drop-fusion = drop-drop
+{-# WARNING_ON_USAGE drop-drop-fusion
+"Warning: drop-drop-fusion was deprecated in v2.0.
+Please use drop-drop instead."
+#-}

src/Data/List/Properties.agda

@@ -784,7 +784,7 @@ take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym
 
 -- If you take at least as many elements from a list as it has, you get
 -- the whole list.
-take-all :(n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs
+take-all : (n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs
 take-all zero [] _ = refl
 take-all (suc _) [] _ = refl
 take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf)
@@ -828,6 +828,12 @@ drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ
 drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
  = drop-take-suc (tabulate f) (cast _ i)
 
+-- Dropping m elements and then n elements is same as dropping m+n elements
+drop-drop : (m n : ℕ) → (xs : List A) → drop n (drop m xs) ≡ drop (m + n) xs
+drop-drop zero n xs = refl
+drop-drop (suc m) n [] = drop-[] n
+drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs
+
 ------------------------------------------------------------------------
 -- splitAt