From 76940a93cf9b1c36098f45988ca710a2731e1d53 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Thu, 11 Apr 2024 01:07:25 +0200
Subject: [PATCH 01/14] Add map commutation with other operations

map commutes with most list operations in some way,
and I initially made a section just for these proofs,
but later decided to spread them into each section
for consistency.
---
 CHANGELOG.md                  |  11 ++++
 src/Data/List/Properties.agda | 110 ++++++++++++++++++++++++++++++++--
 2 files changed, 115 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 469c926af8..f6fb564f40 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -281,6 +281,17 @@ 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
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 2d3c9e20e0..2a4b929654 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -145,6 +145,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
+
 ------------------------------------------------------------------------
 -- _++_
 
@@ -317,6 +333,16 @@ module _ {f g : These A B → C} where
   map-alignWith g (x ∷ xs) (y ∷ ys) =
     cong₂ _∷_ refl (map-alignWith g xs ys)
 
+------------------------------------------------------------------------
+-- 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))
+
 ------------------------------------------------------------------------
 -- zipWith
 
@@ -347,7 +373,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 +382,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 +391,16 @@ module _ (f : A → B → C) where
   map-zipWith g (x ∷ xs) (y ∷ ys) =
     cong₂ _∷_ refl (map-zipWith g xs ys)
 
+------------------------------------------------------------------------
+-- 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))
+
 ------------------------------------------------------------------------
 -- unalignWith
 
@@ -440,6 +476,28 @@ module _ (f : A → B × C) where
   zipWith-unzipWith g f∘g≗id (x ∷ xs) =
     cong₂ _∷_ (f∘g≗id x) (zipWith-unzipWith g f∘g≗id xs)
 
+  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)
+
+------------------------------------------------------------------------
+-- 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))
+
 ------------------------------------------------------------------------
 -- foldr
 
@@ -912,6 +970,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 +1300,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
 
 
 

From 00ec37c90abfa339813e8c742cf52e04571240a3 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Mon, 8 Apr 2024 18:49:01 +0200
Subject: [PATCH 02/14] Add congruence to operations that miss it

---
 CHANGELOG.md                  |  4 ++++
 src/Data/List/Properties.agda | 30 ++++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f6fb564f40..04262dffa8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -292,6 +292,10 @@ Additions to existing modules
   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
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 2a4b929654..9092dfcbe7 100644
--- a/src/Data/List/Properties.agda
+++ b/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)
@@ -346,6 +355,14 @@ align-map f g xs ys = trans
 ------------------------------------------------------------------------
 -- zipWith
 
+module _ {f g : A → B → C} where
+
+  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 → A → B) where
 
   zipWith-comm : (∀ x y → f x y ≡ f y x) →
@@ -458,6 +475,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 →
@@ -585,6 +609,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

From bb9a8a2c22266315175b2f61a36013a631e1f7e2 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Tue, 9 Apr 2024 09:20:41 +0200
Subject: [PATCH 03/14] Add flip & comm proofs to align[With] & [un]zip[With]

For the case of zipWith, the existing comm proof
can be provided in terms of cong and flip.

For the case of unzip[With], the comm proof has
little use and the flip proof is better named "swap".
---
 CHANGELOG.md                  |  6 ++++
 src/Data/List/Properties.agda | 64 +++++++++++++++++++++++++++++------
 2 files changed, 60 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 04262dffa8..c25c08ee15 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -296,6 +296,12 @@ Additions to existing modules
   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
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 9092dfcbe7..83367b23b6 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -342,6 +342,21 @@ 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
 
@@ -352,6 +367,13 @@ 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
 
@@ -363,16 +385,6 @@ module _ {f g : A → B → C} where
   zipWith-cong f≗g (a ∷ as)   (b ∷ bs) =
     cong₂ _∷_ (f≗g a b) (zipWith-cong f≗g as bs)
 
-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 []       []       = 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)
-
 module _ (f : A → B → C) where
 
   zipWith-zeroˡ : ∀ xs → zipWith f [] xs ≡ []
@@ -408,6 +420,20 @@ 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
 
@@ -418,6 +444,13 @@ 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
 
@@ -512,6 +545,12 @@ module _ (f : A → B × C) where
   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
 
@@ -522,6 +561,11 @@ 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)
+
 ------------------------------------------------------------------------
 -- foldr
 

From 9318b90d4233fa2c74ac411e40b844b0e531cc17 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Mon, 8 Apr 2024 19:10:59 +0200
Subject: [PATCH 04/14] Remove unbound parameter
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The alignWith section begins with a
module _ {f g : These A B → C} where
but g is only used by the first function.
---
 CHANGELOG.md                  | 3 +++
 src/Data/List/Properties.agda | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c25c08ee15..bc5de662e1 100644
--- a/CHANGELOG.md
+++ b/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
 --------------------------------
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 83367b23b6..291145dc72 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -320,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

From da8ce308d2cbf4fd995de9b0a347c62c2ce344ad Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Tue, 9 Apr 2024 00:13:11 +0200
Subject: [PATCH 05/14] Add properties for take

---
 CHANGELOG.md                  |  2 ++
 src/Data/List/Properties.agda | 15 +++++++++++++++
 2 files changed, 17 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bc5de662e1..f6f829c959 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -305,6 +305,8 @@ Additions to existing modules
   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)
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 291145dc72..7daa1f5be9 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -956,6 +956,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
 

From 6641314f4176ac28d993788d503e6853a56f4305 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Thu, 11 Apr 2024 01:08:32 +0200
Subject: [PATCH 06/14] Proof of zip[With] and unzip[With] being inverses

---
 CHANGELOG.md                  |  3 +++
 src/Data/List/Properties.agda | 21 ++++++++++++++++++---
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f6f829c959..dc00b87ef8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -307,6 +307,9 @@ Additions to existing modules
   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`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 7daa1f5be9..4d3bac1f85 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -531,9 +531,17 @@ 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
@@ -568,6 +576,13 @@ 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
 

From 119c2c3912c4bea9906261f1c0d99fe0868033da Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Thu, 11 Apr 2024 15:51:13 +0200
Subject: [PATCH 07/14] fixup! don't put list parameters in modules

---
 src/Data/List/Properties.agda | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 4d3bac1f85..826a859c5b 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -369,12 +369,11 @@ 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))
+align-flip : ∀ (xs : List A) (ys : List B) →
+             align xs ys ≡ map These.swap (align ys xs)
+align-flip xs ys = trans
+  (alignWith-flip xs ys)
+  (sym (map-alignWith These.swap ys xs))
 
 ------------------------------------------------------------------------
 -- zipWith
@@ -446,12 +445,11 @@ 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))
+zip-flip : ∀ (xs : List A) (ys : List B) →
+           zip xs ys ≡ map Product.swap (zip ys xs)
+zip-flip xs ys = trans
+  (zipWith-flip _,_ xs ys)
+  (sym (map-zipWith _,_ Product.swap ys xs))
 
 ------------------------------------------------------------------------
 -- unalignWith

From 712f48d40355f1da2c38af6bddfb4fe6f727157d Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Thu, 11 Apr 2024 15:52:42 +0200
Subject: [PATCH 08/14] fixup! typo in changelog entry

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dc00b87ef8..3f62084e09 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -308,7 +308,7 @@ Additions to existing modules
   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)
+  unzipWith-zipWith     : f ∘ uncurry′ g ≗ id → length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys)
   unzip-zip             : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
   ```
 

From 6415eff3aa14c87d6674805ab081ea67f4c22e72 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Thu, 11 Apr 2024 20:08:54 +0200
Subject: [PATCH 09/14] fixup! use equational reasoning in place of trans

---
 src/Data/List/Properties.agda | 56 ++++++++++++++++++++---------------
 1 file changed, 32 insertions(+), 24 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 826a859c5b..30dd4a1c1e 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -355,9 +355,10 @@ 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)
+  alignWith-comm f-comm xs ys = begin
+    alignWith f xs ys                ≡⟨ alignWith-flip xs ys ⟩
+    alignWith (f ∘ These.swap) ys xs ≡⟨ alignWith-cong f-comm ys xs ⟩
+    alignWith f ys xs                ∎
 
 ------------------------------------------------------------------------
 -- align
@@ -365,15 +366,17 @@ module _ {f : These A A → B} where
 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))
+align-map f g xs ys = begin
+  align (map f xs) (map g ys)       ≡⟨ alignWith-map f g xs ys ⟩
+  alignWith (These.map f g) xs ys   ≡⟨ sym (map-alignWith (These.map f g) xs ys) ⟩
+  map (These.map f g) (align xs ys) ∎
 
 align-flip : ∀ (xs : List A) (ys : List B) →
              align xs ys ≡ map These.swap (align ys xs)
-align-flip xs ys = trans
-  (alignWith-flip xs ys)
-  (sym (map-alignWith These.swap ys xs))
+align-flip xs ys = begin
+  align xs ys                  ≡⟨ alignWith-flip xs ys ⟩
+  alignWith These.swap ys xs   ≡⟨ sym (map-alignWith These.swap ys xs) ⟩
+  map These.swap (align ys xs) ∎
 
 ------------------------------------------------------------------------
 -- zipWith
@@ -431,9 +434,10 @@ 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)
+  zipWith-comm f-comm xs ys = begin
+    zipWith f xs ys        ≡⟨ zipWith-flip f xs ys ⟩
+    zipWith (flip f) ys xs ≡⟨ zipWith-cong (flip f-comm) ys xs ⟩
+    zipWith f ys xs        ∎
 
 ------------------------------------------------------------------------
 -- zip
@@ -441,15 +445,17 @@ module _ (f : A → A → B) where
 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))
+zip-map f g xs ys = begin
+  zip (map f xs) (map g ys)         ≡⟨ zipWith-map _,_ f g xs ys ⟩
+  zipWith (λ x y → f x , g y) xs ys ≡⟨ sym (map-zipWith _,_ (Product.map f g) xs ys) ⟩
+  map (Product.map f g) (zip xs ys) ∎
 
 zip-flip : ∀ (xs : List A) (ys : List B) →
            zip xs ys ≡ map Product.swap (zip ys xs)
-zip-flip xs ys = trans
-  (zipWith-flip _,_ xs ys)
-  (sym (map-zipWith _,_ Product.swap ys xs))
+zip-flip xs ys = begin
+  zip xs ys                    ≡⟨ zipWith-flip _,_ xs ys ⟩
+  zipWith (flip _,_) ys xs     ≡⟨ sym (map-zipWith _,_ Product.swap ys xs) ⟩
+  map Product.swap (zip ys xs) ∎
 
 ------------------------------------------------------------------------
 -- unalignWith
@@ -565,14 +571,16 @@ module _ (f : A → B × C) where
 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-map f g xs = begin
+  unzip (map (Product.map f g) xs)       ≡⟨ unzipWith-map id (Product.map f g) xs ⟩
+  unzipWith (Product.map f g) xs         ≡⟨ sym (map-unzipWith id f g xs) ⟩
+  Product.map (map f) (map g) (unzip 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)
+unzip-swap xs = begin
+  unzip (map Product.swap xs) ≡⟨ unzipWith-map id Product.swap xs ⟩
+  unzipWith Product.swap xs   ≡⟨ unzipWith-swap id xs ⟩
+  Product.swap (unzip xs)     ∎
 
 zip-unzip : uncurry′ zip ∘ unzip ≗ id {A = List (A × B)}
 zip-unzip = zipWith-unzipWith id _,_ λ _ → refl

From e61bfe202652b3d66877e4923dee27740b1bee54 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Fri, 12 Apr 2024 03:43:32 +0200
Subject: [PATCH 10/14] Add interaction with ++ in two more operations

---
 CHANGELOG.md                  |  2 ++
 src/Data/List/Properties.agda | 14 ++++++++++++++
 2 files changed, 16 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3f62084e09..5737f5d2d4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -310,6 +310,8 @@ Additions to existing modules
   zip-unzip             : uncurry′ zip ∘ unzip ≗ id
   unzipWith-zipWith     : f ∘ uncurry′ g ≗ id → length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys)
   unzip-zip             : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
+  mapMaybe-++           : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
+  unzipWith-++          : unzipWith f (xs ++ ys) ≡ zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 30dd4a1c1e..5afa84bb87 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -154,6 +154,13 @@ module _ (f : A → Maybe B) where
   ... | just y  = s≤s ih
   ... | nothing = m≤n⇒m≤1+n ih
 
+  mapMaybe-++ : ∀ xs ys →
+                mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
+  mapMaybe-++ []       ys = refl
+  mapMaybe-++ (x ∷ xs) ys with ih ← mapMaybe-++ xs ys | f x
+  ... | just y  = cong (y ∷_) ih
+  ... | nothing = ih
+
 module _ (f : B → Maybe C) (g : A → B) where
 
   mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
@@ -565,6 +572,13 @@ module _ (f : A → B × C) where
   unzipWith-swap (x ∷ xs) =
     cong (Product.zip _∷_ _∷_ _) (unzipWith-swap xs)
 
+  unzipWith-++ : ∀ xs ys →
+                 unzipWith f (xs ++ ys) ≡
+                 Product.zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
+  unzipWith-++ []       ys = refl
+  unzipWith-++ (x ∷ xs) ys =
+    cong (Product.zip _∷_ _∷_ (f x)) (unzipWith-++ xs ys)
+
 ------------------------------------------------------------------------
 -- unzip
 

From 25389a7b55906dcb2becb3aaeaa9c11b2038e321 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 21 Apr 2024 12:15:56 +0200
Subject: [PATCH 11/14] =?UTF-8?q?fixup!=20foldl-cong:=20don't=20take=20d?=
 =?UTF-8?q?=20=E2=89=A1=20e?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                  | 2 +-
 src/Data/List/Properties.agda | 9 ++++-----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89de367396..b6554a9c04 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -323,7 +323,7 @@ Additions to existing modules
   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
+  foldl-cong            : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
   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)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index ccb3c19726..7972c3e658 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -696,11 +696,10 @@ 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-cong : ∀ {f g : B → A → B} → (∀ x y → f x y ≡ g x y) →
+             ∀ x → foldl f x ≗ foldl g x
+foldl-cong f≗g x []       = refl
+foldl-cong f≗g x (y ∷ xs) rewrite f≗g x y = foldl-cong f≗g _ xs
 
 foldl-++ : ∀ (f : A → B → A) x ys zs →
            foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs

From bd3e6319266bae5dc4ad1b993cae16c52c85cd07 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 21 Apr 2024 13:35:59 +0200
Subject: [PATCH 12/14] prove properties about catMaybes

now that catMaybes is no longer defined in
terms of mapMaybe, properties about mapMaybe
need to be proven for catMaybe as well
---
 CHANGELOG.md                  |  3 +++
 src/Data/List/Properties.agda | 31 ++++++++++++++++++++++++++-----
 2 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b6554a9c04..57fa2c6bd9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -337,6 +337,9 @@ Additions to existing modules
   unzip-zip             : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
   mapMaybe-++           : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
   unzipWith-++          : unzipWith f (xs ++ ys) ≡ zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
+  catMaybes-concatMap   : catMaybes ≗ concatMap fromMaybe
+  catMaybes-++          : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
+  map-catMaybes         : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 7972c3e658..f1c58c5484 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -119,6 +119,32 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
   let fx≡fy , fxs≡fys = ∷-injective eq in
   cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys)
 
+------------------------------------------------------------------------
+-- catMaybes
+
+catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe
+catMaybes-concatMap []             = refl
+catMaybes-concatMap (just x  ∷ xs) = cong (x ∷_) (catMaybes-concatMap xs)
+catMaybes-concatMap (nothing ∷ xs) = catMaybes-concatMap xs
+
+length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
+length-catMaybes []             = ≤-refl
+length-catMaybes (just x  ∷ xs) = s≤s (length-catMaybes xs)
+length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs)
+
+catMaybes-++ : (xs ys : List (Maybe A)) →
+               catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
+catMaybes-++ []             ys = refl
+catMaybes-++ (just x  ∷ xs) ys = cong (x ∷_) (catMaybes-++ xs ys)
+catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys
+
+module _ (f : A → B) where
+
+  map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
+  map-catMaybes []             = refl
+  map-catMaybes (just x  ∷ xs) = cong (f x ∷_) (map-catMaybes xs)
+  map-catMaybes (nothing ∷ xs) = map-catMaybes xs
+
 ------------------------------------------------------------------------
 -- mapMaybe
 
@@ -131,11 +157,6 @@ module _ {f g : A → Maybe B} where
   ... | just y  = cong (y ∷_) ih
   ... | nothing = ih
 
-length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
-length-catMaybes []        = ≤-refl
-length-catMaybes (just x ∷ xs) = s≤s (length-catMaybes xs)
-length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs)
-
 mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
 mapMaybe-just []       = refl
 mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs)

From 82b7ea42b411225d25e9f8a799b374df1935d1a9 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 21 Apr 2024 14:04:46 +0200
Subject: [PATCH 13/14] move mapMaybe properties down

see next commit (given that mapMaybe-concatMap
now depends on map-concatMap, it has to be
moved down)
---
 src/Data/List/Properties.agda | 118 +++++++++++++++++-----------------
 1 file changed, 59 insertions(+), 59 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f1c58c5484..1659aa35f9 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -145,65 +145,6 @@ module _ (f : A → B) where
   map-catMaybes (just x  ∷ xs) = cong (f x ∷_) (map-catMaybes xs)
   map-catMaybes (nothing ∷ xs) = map-catMaybes xs
 
-------------------------------------------------------------------------
--- 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)
-
-mapMaybe-nothing : (xs : List A) →
-                   mapMaybe {B = B} (λ _ → nothing) xs ≡ []
-mapMaybe-nothing []       = refl
-mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs
-
-module _ (f : A → Maybe B) where
-
-  mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
-  mapMaybe-concatMap []       = refl
-  mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x
-  ... | just y  = cong (y ∷_) ih
-  ... | nothing = ih
-
-  length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
-  length-mapMaybe xs = ≤-begin
-    length (mapMaybe f xs)      ≤⟨ length-catMaybes (map f xs) ⟩
-    length (map f xs)           ≤⟨ ≤-reflexive (length-map f xs) ⟩
-    length xs                   ≤-∎
-    where open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)
-
-  mapMaybe-++ : ∀ xs ys →
-                mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
-  mapMaybe-++ []       ys = refl
-  mapMaybe-++ (x ∷ xs) ys with ih ← mapMaybe-++ xs ys | f x
-  ... | just y  = cong (y ∷_) ih
-  ... | nothing = 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
-
 ------------------------------------------------------------------------
 -- _++_
 
@@ -796,6 +737,65 @@ map-concatMap f g xs = begin
   concatMap (map f ∘′ g) xs
     ∎
 
+------------------------------------------------------------------------
+-- 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)
+
+mapMaybe-nothing : (xs : List A) →
+                   mapMaybe {B = B} (λ _ → nothing) xs ≡ []
+mapMaybe-nothing []       = refl
+mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs
+
+module _ (f : A → Maybe B) where
+
+  mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
+  mapMaybe-concatMap []       = refl
+  mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x
+  ... | just y  = cong (y ∷_) ih
+  ... | nothing = ih
+
+  length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
+  length-mapMaybe xs = ≤-begin
+    length (mapMaybe f xs)      ≤⟨ length-catMaybes (map f xs) ⟩
+    length (map f xs)           ≤⟨ ≤-reflexive (length-map f xs) ⟩
+    length xs                   ≤-∎
+    where open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)
+
+  mapMaybe-++ : ∀ xs ys →
+                mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
+  mapMaybe-++ []       ys = refl
+  mapMaybe-++ (x ∷ xs) ys with ih ← mapMaybe-++ xs ys | f x
+  ... | just y  = cong (y ∷_) ih
+  ... | nothing = 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
+
 ------------------------------------------------------------------------
 -- sum
 

From f7783650ea9aa6468336647d5a7d28c1fb7b2d51 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 21 Apr 2024 14:06:12 +0200
Subject: [PATCH 14/14] simplify mapMaybe proofs

since mapMaybe is now defined in terms
of catMaybes and map, we can derive its
proofs from the proofs of those rather
than using induction directly
---
 src/Data/List/Properties.agda | 35 ++++++++++++++---------------------
 1 file changed, 14 insertions(+), 21 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 1659aa35f9..133cc33ad3 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -743,11 +743,7 @@ map-concatMap f g xs = begin
 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-cong f≗g = cong catMaybes ∘ map-cong f≗g
 
 mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
 mapMaybe-just []       = refl
@@ -761,10 +757,10 @@ mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs
 module _ (f : A → Maybe B) where
 
   mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
-  mapMaybe-concatMap []       = refl
-  mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x
-  ... | just y  = cong (y ∷_) ih
-  ... | nothing = ih
+  mapMaybe-concatMap xs = begin
+    catMaybes (map f xs)            ≡⟨ catMaybes-concatMap (map f xs) ⟩
+    concatMap fromMaybe (map f xs)  ≡⟨ concatMap-map fromMaybe f xs ⟩
+    concatMap (fromMaybe ∘ f) xs    ∎
 
   length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
   length-mapMaybe xs = ≤-begin
@@ -775,26 +771,23 @@ module _ (f : A → Maybe B) where
 
   mapMaybe-++ : ∀ xs ys →
                 mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
-  mapMaybe-++ []       ys = refl
-  mapMaybe-++ (x ∷ xs) ys with ih ← mapMaybe-++ xs ys | f x
-  ... | just y  = cong (y ∷_) ih
-  ... | nothing = ih
+  mapMaybe-++ xs ys = begin
+    catMaybes (map f (xs ++ ys))     ≡⟨ cong catMaybes (map-++ f xs ys) ⟩
+    catMaybes (map f xs ++ map f ys) ≡⟨ catMaybes-++ (map f xs) (map f ys) ⟩
+    mapMaybe f xs ++ mapMaybe f ys   ∎
 
 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
+  mapMaybe-map = cong catMaybes ∘ sym ∘ map-∘
 
 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
+  map-mapMaybe xs = begin
+    map g (catMaybes (map f xs))       ≡⟨ map-catMaybes g (map f xs) ⟩
+    mapMaybe (Maybe.map g) (map f xs)  ≡⟨ mapMaybe-map _ f xs ⟩
+    mapMaybe (Maybe.map g ∘ f) xs      ∎
 
 ------------------------------------------------------------------------
 -- sum