Add drop-drop in Data.List.Properties

CHANGELOG.md

@@ -2205,15 +2205,17 @@ Other minor changes
   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 : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
+  take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
+  drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in drop m (take (suc m) xs) ≡ [ lookup xs i ]
+  drop-take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ]
+
+  drop-drop : drop n (drop m x) ≡ drop (n + m) x
 
   take-all : n ≥ length xs → take n xs ≡ xs
 
-  take-[] : ∀ m → take  m [] ≡ []
-  drop-[] : ∀ m → drop  m [] ≡ []
+  take-[] : take  m [] ≡ []
+  drop-[] : drop  m [] ≡ []
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:

src/Data/List/Properties.agda

@@ -780,7 +780,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)
@@ -824,6 +824,13 @@ 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 n+m elements
+drop-drop : (n m : ℕ) → (x : List A) → drop n (drop m x) ≡ drop (n + m) x
+drop-drop zero    m       x                          = refl
+drop-drop (suc n) zero    x rewrite +-identityʳ n    = refl
+drop-drop (suc n) (suc m) []                         = refl
+drop-drop (suc n) (suc m) (x ∷ xs) rewrite +-suc n m = drop-drop (suc n) m xs
+
 ------------------------------------------------------------------------
 -- splitAt