Proofs take/drop/head -map-commute added to Data.List.Properties (#1986)

Author: Sofia-Insa

CHANGELOG.md

@@ -2200,6 +2200,10 @@ 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-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

src/Data/List/Properties.agda

@@ -21,7 +21,7 @@ open import Data.List.Base as List
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
@@ -44,6 +44,7 @@ open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_
 open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)
 
+
 open ≡-Reasoning
 
 private
@@ -761,6 +762,12 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
+-- Take commutes with map.
+take-map : ∀ {f : A → B} (n : ℕ) xs → take n (map f xs) ≡ map f (take n xs)
+take-map zero xs = refl
+take-map (suc s) [] = refl
+take-map (suc s) (a ∷ xs) = cong (_ ∷_) (take-map s 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
@@ -791,12 +798,17 @@ length-drop zero    xs       = refl
 length-drop (suc n) []       = refl
 length-drop (suc n) (x ∷ xs) = length-drop n xs
 
+-- Drop commutes with map.
+drop-map : ∀ {f : A → B} (n : ℕ) xs → drop n (map f xs) ≡ map f (drop n xs)
+drop-map zero xs = refl
+drop-map (suc n) [] = refl
+drop-map (suc n) (a ∷ xs) = drop-map n xs
+
 -- Dropping from an empty list does nothing.
 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
@@ -1118,6 +1130,17 @@ module _ {x y : A} where
 
 
 
+------------------------------------------------------------------------
+-- head
+
+-- 'commute' List.head and List.map to obtain a Maybe.map and List.head.
+head-map : ∀ {f : A → B} xs → head (map f xs) ≡ Maybe.map f (head xs)
+head-map [] = refl
+head-map (_ ∷ _) = refl
+
+
+
+
 ------------------------------------------------------------------------
 -- DEPRECATED
 ------------------------------------------------------------------------