Add proofs to Data.List.Properties

CHANGELOG.md

@@ -16,6 +16,9 @@ Bug-fixes
 * Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer
   exports the `Setoid` module under the alias `S`.
 
+* Remove unbound parameter from `Data.List.Properties.length-alignWith`,
+  `alignWith-map` and `map-alignWith`.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -281,6 +284,32 @@ Additions to existing modules
   reverse-upTo          : reverse (upTo n) ≡ downFrom n
   reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
   reverse-downFrom      : reverse (downFrom n) ≡ upTo n
+  mapMaybe-map          : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
+  map-mapMaybe          : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
+  align-map             : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys)
+  zip-map               : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys)
+  unzipWith-map         : unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
+  map-unzipWith         : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f)
+  unzip-map             : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip
+  splitAt-map           : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n
+  uncons-map            : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons
+  last-map              : last ∘ map f ≗ map f ∘ last
+  tail-map              : tail ∘ map f ≗ map (map f) ∘ tail
+  mapMaybe-cong         : f ≗ g → mapMaybe f ≗ mapMaybe g
+  zipWith-cong          : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
+  unzipWith-cong        : f ≗ g → unzipWith f ≗ unzipWith g
+  foldl-cong            : (∀ x y → f x y ≡ g x y) → d ≡ e → foldl f d ≗ foldl g e
+  alignWith-flip        : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
+  alignWith-comm        : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
+  align-flip            : align xs ys ≡ map swap (align ys xs)
+  zip-flip              : zip xs ys ≡ map swap (zip ys xs)
+  unzipWith-swap        : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f
+  unzip-swap            : unzip ∘ map swap ≗ swap ∘ unzip
+  take-take             : take n (take m xs) ≡ take (n ⊓ m) xs
+  take-drop             : take n (drop m xs) ≡ drop m (take (m + n) xs)
+  zip-unzip             : uncurry′ zip ∘ unzip ≗ id
+  unzipWith-zipWith     : length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys)
+  unzip-zip             : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:

src/Data/List/Properties.agda

@@ -122,6 +122,15 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
 ------------------------------------------------------------------------
 -- mapMaybe
 
+module _ {f g : A → Maybe B} where
+
+  mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
+  mapMaybe-cong f≗g [] = refl
+  mapMaybe-cong f≗g (x ∷ xs) rewrite f≗g x
+    with ih ← mapMaybe-cong f≗g xs | g x
+  ... | just y  = cong (y ∷_) ih
+  ... | nothing = ih
+
 mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
 mapMaybe-just []       = refl
 mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs)
@@ -145,6 +154,22 @@ module _ (f : A → Maybe B) where
   ... | just y  = s≤s ih
   ... | nothing = m≤n⇒m≤1+n ih
 
+module _ (f : B → Maybe C) (g : A → B) where
+
+  mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
+  mapMaybe-map []       = refl
+  mapMaybe-map (x ∷ xs) with ih ← mapMaybe-map xs | f (g x)
+  ... | just y  = cong (y ∷_) ih
+  ... | nothing = ih
+
+module _ (g : B → C) (f : A → Maybe B) where
+
+  map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
+  map-mapMaybe []       = refl
+  map-mapMaybe (x ∷ xs) with ih ← map-mapMaybe xs | f x
+  ... | just y  = cong (g y ∷_) ih
+  ... | nothing = ih
+
 ------------------------------------------------------------------------
 -- _++_
 
@@ -295,6 +320,8 @@ module _ {f g : These A B → C} where
   alignWith-cong f≗g (a ∷ as)   (b ∷ bs) =
     cong₂ _∷_ (f≗g (these a b)) (alignWith-cong f≗g as bs)
 
+module _ {f : These A B → C} where
+
   length-alignWith : ∀ xs ys →
                    length (alignWith f xs ys) ≡ length xs ⊔ length ys
   length-alignWith []         ys       = length-map (f ∘′ that) ys
@@ -317,18 +344,48 @@ module _ {f g : These A B → C} where
   map-alignWith g (x ∷ xs) (y ∷ ys) =
     cong₂ _∷_ refl (map-alignWith g xs ys)
 
+  alignWith-flip : ∀ xs ys →
+                 alignWith f xs ys ≡ alignWith (f ∘ These.swap) ys xs
+  alignWith-flip []       []       = refl
+  alignWith-flip []       (y ∷ ys) = refl
+  alignWith-flip (x ∷ xs) []       = refl
+  alignWith-flip (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (alignWith-flip xs ys)
+
+module _ {f : These A A → B} where
+
+  alignWith-comm : f ∘ These.swap ≗ f →
+                 ∀ xs ys → alignWith f xs ys ≡ alignWith f ys xs
+  alignWith-comm f-comm xs ys = trans
+    (alignWith-flip xs ys)
+    (alignWith-cong f-comm ys xs)
+
+------------------------------------------------------------------------
+-- align
+
+align-map : ∀ (f : A → B) (g : C → D) →
+            ∀ xs ys → align (map f xs) (map g ys) ≡
+                      map (These.map f g) (align xs ys)
+align-map f g xs ys = trans
+  (alignWith-map f g xs ys)
+  (sym (map-alignWith (These.map f g) xs ys))
+
+module _ (xs : List A) (ys : List B) where
+
+  align-flip : align xs ys ≡ map These.swap (align ys xs)
+  align-flip = trans
+    (alignWith-flip xs ys)
+    (sym (map-alignWith These.swap ys xs))
+
 ------------------------------------------------------------------------
 -- zipWith
 
-module _ (f : A → A → B) where
+module _ {f g : A → B → C} where
 
-  zipWith-comm : (∀ x y → f x y ≡ f y x) →
-                 ∀ xs ys → zipWith f xs ys ≡ zipWith f ys xs
-  zipWith-comm f-comm []       []       = refl
-  zipWith-comm f-comm []       (x ∷ ys) = refl
-  zipWith-comm f-comm (x ∷ xs) []       = refl
-  zipWith-comm f-comm (x ∷ xs) (y ∷ ys) =
-    cong₂ _∷_ (f-comm x y) (zipWith-comm f-comm xs ys)
+  zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
+  zipWith-cong f≗g []         bs       = refl
+  zipWith-cong f≗g as@(_ ∷ _) []       = refl
+  zipWith-cong f≗g (a ∷ as)   (b ∷ bs) =
+    cong₂ _∷_ (f≗g a b) (zipWith-cong f≗g as bs)
 
 module _ (f : A → B → C) where
 
@@ -347,7 +404,7 @@ module _ (f : A → B → C) where
   length-zipWith (x ∷ xs) []       = refl
   length-zipWith (x ∷ xs) (y ∷ ys) = cong suc (length-zipWith xs ys)
 
-  zipWith-map : ∀ {d e} {D : Set d} {E : Set e} (g : D → A) (h : E → B) →
+  zipWith-map : ∀ (g : D → A) (h : E → B) →
                 ∀ xs ys → zipWith f (map g xs) (map h ys) ≡
                           zipWith (λ x y → f (g x) (h y)) xs ys
   zipWith-map g h []       []       = refl
@@ -356,7 +413,7 @@ module _ (f : A → B → C) where
   zipWith-map g h (x ∷ xs) (y ∷ ys) =
     cong₂ _∷_ refl (zipWith-map g h xs ys)
 
-  map-zipWith : ∀ {d} {D : Set d} (g : C → D) → ∀ xs ys →
+  map-zipWith : ∀ (g : C → D) → ∀ xs ys →
                 map g (zipWith f xs ys) ≡
                 zipWith (λ x y → g (f x y)) xs ys
   map-zipWith g []       []       = refl
@@ -365,6 +422,37 @@ module _ (f : A → B → C) where
   map-zipWith g (x ∷ xs) (y ∷ ys) =
     cong₂ _∷_ refl (map-zipWith g xs ys)
 
+  zipWith-flip : ∀ xs ys → zipWith f xs ys ≡ zipWith (flip f) ys xs
+  zipWith-flip []       []       = refl
+  zipWith-flip []       (x ∷ ys) = refl
+  zipWith-flip (x ∷ xs) []       = refl
+  zipWith-flip (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (zipWith-flip xs ys)
+
+module _ (f : A → A → B) where
+
+  zipWith-comm : (∀ x y → f x y ≡ f y x) →
+                 ∀ xs ys → zipWith f xs ys ≡ zipWith f ys xs
+  zipWith-comm f-comm xs ys = trans
+    (zipWith-flip f xs ys)
+    (zipWith-cong (flip f-comm) ys xs)
+
+------------------------------------------------------------------------
+-- zip
+
+zip-map : ∀ (f : A → B) (g : C → D) →
+          ∀ xs ys → zip (map f xs) (map g ys) ≡
+                    map (Product.map f g) (zip xs ys)
+zip-map f g xs ys = trans
+  (zipWith-map _,_ f g xs ys)
+  (sym (map-zipWith _,_ (Product.map f g) xs ys))
+
+module _ (xs : List A) (ys : List B) where
+
+  zip-flip : zip xs ys ≡ map Product.swap (zip ys xs)
+  zip-flip = trans
+    (zipWith-flip _,_ xs ys)
+    (sym (map-zipWith _,_ Product.swap ys xs))
+
 ------------------------------------------------------------------------
 -- unalignWith
 
@@ -422,6 +510,13 @@ module _ (f : C → These A B) where
 ------------------------------------------------------------------------
 -- unzipWith
 
+module _ {f g : A → B × C} where
+
+  unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g
+  unzipWith-cong f≗g [] = refl
+  unzipWith-cong f≗g (x ∷ xs) =
+    cong₂ (Product.zip _∷_ _∷_) (f≗g x) (unzipWith-cong f≗g xs)
+
 module _ (f : A → B × C) where
 
   length-unzipWith₁ : ∀ xys →
@@ -436,9 +531,57 @@ module _ (f : A → B × C) where
 
   zipWith-unzipWith : (g : B → C → A) → uncurry′ g ∘ f ≗ id →
                       uncurry′ (zipWith g) ∘ (unzipWith f)  ≗ id
-  zipWith-unzipWith g f∘g≗id []       = refl
-  zipWith-unzipWith g f∘g≗id (x ∷ xs) =
-    cong₂ _∷_ (f∘g≗id x) (zipWith-unzipWith g f∘g≗id xs)
+  zipWith-unzipWith g g∘f≗id []       = refl
+  zipWith-unzipWith g g∘f≗id (x ∷ xs) =
+    cong₂ _∷_ (g∘f≗id x) (zipWith-unzipWith g g∘f≗id xs)
+
+  unzipWith-zipWith : (g : B → C → A) → f ∘ uncurry′ g ≗ id →
+                      ∀ xs ys → length xs ≡ length ys →
+                      unzipWith f (zipWith g xs ys) ≡ (xs , ys)
+  unzipWith-zipWith g f∘g≗id []       []       l≡l = refl
+  unzipWith-zipWith g f∘g≗id (x ∷ xs) (y ∷ ys) l≡l  =
+    cong₂ (Product.zip _∷_ _∷_) (f∘g≗id (x , y))
+          (unzipWith-zipWith g f∘g≗id xs ys (suc-injective l≡l))
+
+  unzipWith-map : (g : D → A) → unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
+  unzipWith-map g []       = refl
+  unzipWith-map g (x ∷ xs) =
+    cong (Product.zip _∷_ _∷_ (f (g x))) (unzipWith-map g xs)
+
+  map-unzipWith : (g : B → D) (h : C → E) →
+                  Product.map (map g) (map h) ∘ unzipWith f ≗
+                  unzipWith (Product.map g h ∘ f)
+  map-unzipWith g h []       = refl
+  map-unzipWith g h (x ∷ xs) =
+    cong (Product.zip _∷_ _∷_ _) (map-unzipWith g h xs)
+
+  unzipWith-swap : unzipWith (Product.swap ∘ f) ≗
+                   Product.swap ∘ unzipWith f
+  unzipWith-swap []       = refl
+  unzipWith-swap (x ∷ xs) =
+    cong (Product.zip _∷_ _∷_ _) (unzipWith-swap xs)
+
+------------------------------------------------------------------------
+-- unzip
+
+unzip-map : ∀ (f : A → B) (g : C → D) →
+            unzip ∘ map (Product.map f g) ≗
+            Product.map (map f) (map g) ∘ unzip
+unzip-map f g xs = trans
+  (unzipWith-map id (Product.map f g) xs)
+  (sym (map-unzipWith id f g xs))
+
+unzip-swap : unzip ∘ map Product.swap ≗ Product.swap ∘ unzip {A = A} {B = B}
+unzip-swap xs = trans
+  (unzipWith-map id Product.swap xs)
+  (unzipWith-swap id xs)
+
+zip-unzip : uncurry′ zip ∘ unzip ≗ id {A = List (A × B)}
+zip-unzip = zipWith-unzipWith id _,_ λ _ → refl
+
+unzip-zip : ∀ (xs : List A) (ys : List B) →
+            length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
+unzip-zip = unzipWith-zipWith id _,_ λ _ → refl
 
 ------------------------------------------------------------------------
 -- foldr
@@ -527,6 +670,12 @@ module _ {P : Pred A p} {f : A → A → A} where
 ------------------------------------------------------------------------
 -- foldl
 
+foldl-cong : ∀ {f g : B → A → B} {d e : B} →
+             (∀ x y → f x y ≡ g x y) → d ≡ e →
+             foldl f d ≗ foldl g e
+foldl-cong f≗g refl []      = refl
+foldl-cong f≗g d≡e (x ∷ xs) rewrite d≡e = foldl-cong f≗g (f≗g _ x) xs
+
 foldl-++ : ∀ (f : A → B → A) x ys zs →
            foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
 foldl-++ f x []       zs = refl
@@ -822,6 +971,21 @@ take-[] : ∀ m → take {A = A} m [] ≡ []
 take-[] zero = refl
 take-[] (suc m) = refl
 
+-- Taking twice takes the minimum of both counts.
+take-take : ∀ n m (xs : List A) → take n (take m xs) ≡ take (n ⊓ m) xs
+take-take zero    m       xs       = refl
+take-take (suc n) zero    xs       = refl
+take-take (suc n) (suc m) []       = refl
+take-take (suc n) (suc m) (x ∷ xs) = cong (x ∷_) (take-take n m xs)
+
+-- Dropping m elements and then taking n is the same as
+-- taking n + m elements and then dropping m.
+take-drop : ∀ n m (xs : List A) →
+            take n (drop m xs) ≡ drop m (take (m + n) xs)
+take-drop n zero    xs       = refl
+take-drop n (suc m) []       = take-[] n
+take-drop n (suc m) (x ∷ xs) = take-drop n m xs
+
 ------------------------------------------------------------------------
 -- drop
 
@@ -912,6 +1076,15 @@ splitAt-defn zero    xs       = refl
 splitAt-defn (suc n) []       = refl
 splitAt-defn (suc n) (x ∷ xs) = cong (Product.map (x ∷_) id) (splitAt-defn n xs)
 
+module _ (f : A → B) where
+
+  splitAt-map : ∀ n → splitAt n ∘ map f ≗
+                      Product.map (map f) (map f) ∘ splitAt n
+  splitAt-map zero    xs       = refl
+  splitAt-map (suc n) []       = refl
+  splitAt-map (suc n) (x ∷ xs) =
+    cong (Product.map₁ (f x ∷_)) (splitAt-map n xs)
+
 ------------------------------------------------------------------------
 -- takeWhile, dropWhile, and span
 
@@ -1233,15 +1406,46 @@ 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
 
+------------------------------------------------------------------------
+-- uncons
 
+module _ (f : A → B) where
+
+  -- 'commute' List.uncons and List.map to obtain a Maybe.map and List.uncons.
+  uncons-map : uncons ∘ map f ≗ Maybe.map (Product.map f (map f)) ∘ uncons
+  uncons-map []       = refl
+  uncons-map (x ∷ xs) = refl
 
 ------------------------------------------------------------------------
 -- 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
+module _ {f : A → B} where
+
+  -- 'commute' List.head and List.map to obtain a Maybe.map and List.head.
+  head-map : head ∘ map f ≗ Maybe.map f ∘ head
+  head-map []      = refl
+  head-map (_ ∷ _) = refl
+
+------------------------------------------------------------------------
+-- last
+
+module _ (f : A → B) where
+
+  -- 'commute' List.last and List.map to obtain a Maybe.map and List.last.
+  last-map : last ∘ map f ≗ Maybe.map f ∘ last
+  last-map []               = refl
+  last-map (x ∷ [])         = refl
+  last-map (x ∷ xs@(_ ∷ _)) = last-map xs
+
+------------------------------------------------------------------------
+-- tail
+
+module _ (f : A → B) where
+
+  -- 'commute' List.tail and List.map to obtain a Maybe.map and List.tail.
+  tail-map : tail ∘ map f ≗ Maybe.map (map f) ∘ tail
+  tail-map []       = refl
+  tail-map (x ∷ xs) = refl