New functions take-drop-1 and take-one-more added to Data.List.Pr…

…operties (#1984)

CHANGELOG.md

@@ -2152,8 +2152,14 @@ Other minor changes
 
  length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
  length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
+
+ 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-all : n ≥ length xs → take n xs ≡ xs 
+ 
  take-[] : ∀ m → take m [] ≡ []
  drop-[] : ∀ m → drop m [] ≡ []
  ```
@@ -2887,7 +2893,7 @@ Other minor changes
  foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
  foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
  ```
-
+ 
 NonZero/Positive/Negative changes
 ---------------------------------
 

src/Data/List/Properties.agda

@@ -30,6 +30,7 @@ open import Data.Product.Base as Prod
 import Data.Product.Relation.Unary.All as Prod using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
+open import Data.Fin.Properties using (toℕ-cast)
 open import Function
 open import Level using (Level)
 open import Relation.Binary as B using (DecidableEquality)
@@ -759,6 +760,16 @@ length-take zero xs = refl
 length-take (suc n) [] = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
+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 (x ∷ xs) zero = refl
+take-suc (x ∷ xs) (suc i) = cong (x ∷_) (take-suc xs i)
+
+take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
+ take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
+take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
+ = take-suc (tabulate f) (cast _ i)
+
 -- 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 zero [] _ = refl
@@ -789,6 +800,16 @@ take++drop zero xs = refl
 take++drop (suc n) [] = refl
 take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop 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 ]
+drop-take-suc (x ∷ xs) zero = refl
+drop-take-suc (x ∷ xs) (suc i) = drop-take-suc xs i
+
+drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
+ drop m (take (suc m) (tabulate f)) ≡ [ f i ]
+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)
+
 ------------------------------------------------------------------------
 -- splitAt
 
@@ -1093,6 +1114,8 @@ module _ {x y : A} where
 ∷ʳ-++ : ∀ (xs : List A) (a : A) (ys : List A) → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
 ∷ʳ-++ xs a ys = ++-assoc xs [ a ] ys
 
+
+
 ------------------------------------------------------------------------
 -- DEPRECATED
 ------------------------------------------------------------------------