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

CHANGELOG.md

@@ -2053,6 +2053,12 @@ 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 ]
+
  ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2784,7 +2790,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

@@ -29,6 +29,7 @@ open import Data.Product as Prod hiding (map; zip)
 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)
@@ -758,6 +759,15 @@ 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) (o : Fin (length xs)) → let m = toℕ o in
+ take (suc m) xs ≡ take m xs ∷ʳ lookup xs o
+take-suc (x ∷ xs) zero = refl
+take-suc (x ∷ xs) (suc o) = cong (x ∷_) (take-suc xs o)
+
+take-suc-tabulate : ∀ {n} (f : Fin n → A) (o : Fin n) → let m = toℕ o in
+ take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o
+take-suc-tabulate f o rewrite sym (toℕ-cast (sym (length-tabulate f)) o) | sym (lookup-tabulate f o)
+ = take-suc (tabulate f) (cast _ o)
 ------------------------------------------------------------------------
 -- drop
 
@@ -771,6 +781,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) (o : Fin (length xs)) → let m = toℕ o in
+ drop m (take (suc m) xs) ≡ [ lookup xs o ]
+drop-take-suc (x ∷ xs) zero = refl
+drop-take-suc (x ∷ xs) (suc o) = drop-take-suc xs o
+
+drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (o : Fin n) → let m = toℕ o in
+ drop m (take (suc m) (tabulate f)) ≡ [ f o ]
+drop-take-suc-tabulate f o rewrite sym (toℕ-cast (sym (length-tabulate f)) o) | sym (lookup-tabulate f o)
+ = drop-take-suc (tabulate f) (cast _ o)
+
 ------------------------------------------------------------------------
 -- splitAt
 
@@ -1075,6 +1095,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
 ------------------------------------------------------------------------