More list properties about catMaybes/mapMaybe

- Follow-up to PR #2361
- Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256)

Author: omelkonian

CHANGELOG.md

@@ -343,47 +343,54 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
-  length-catMaybes      : length (catMaybes xs) ≤ length xs
-  applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
-  applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
-  upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
-  downFrom-∷ʳ           : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
-  reverse-selfInverse   : SelfInverse {A = List A} _≡_ reverse
-  reverse-applyUpTo     : reverse (applyUpTo f n) ≡ applyDownFrom f n
-  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) → ∀ 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)
-  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     : 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)
-  catMaybes-concatMap   : catMaybes ≗ concatMap fromMaybe
-  catMaybes-++          : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
-  map-catMaybes         : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
+  length-catMaybes       : length (catMaybes xs) ≤ length xs
+  applyUpTo-∷ʳ           : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
+  applyDownFrom-∷ʳ       : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
+  upTo-∷ʳ                : upTo n ∷ʳ n ≡ upTo (suc n)
+  downFrom-∷ʳ            : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
+  reverse-selfInverse    : SelfInverse {A = List A} _≡_ reverse
+  reverse-applyUpTo      : reverse (applyUpTo f n) ≡ applyDownFrom f n
+  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) → ∀ 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)
+  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      : 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)
+  catMaybes-concatMap    : catMaybes ≗ concatMap fromMaybe
+  catMaybes-++           : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
+  map-catMaybes          : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
+  Any-catMaybes⁺         : Any (M.Any P) xs → Any P (catMaybes xs)
+  mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs
+  mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ []
+  mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs
+  mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ []
   ```
 
 * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
@@ -496,7 +503,9 @@ Additions to existing modules
 
 * Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
-  product-↭ : product Preserves _↭_ ⟶ _≡_
+  product-↭   : product Preserves _↭_ ⟶ _≡_
+  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
   ```
 
 * Added new functions in `Data.String.Base`:

src/Data/List/Properties.agda

@@ -24,13 +24,14 @@ 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 as Maybe using (Maybe; just; nothing; maybe)
+open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
   using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
 import Data.Product.Relation.Unary.All as Product using (All)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂; isInj₁; isInj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Fin.Properties using (toℕ-cast)
 open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
@@ -48,6 +49,7 @@ open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
+private variable ℓ : Level
 
 open ≡-Reasoning
 
@@ -83,71 +85,6 @@ private
 ≡-dec _≟_ []       (y ∷ ys) = no λ()
 ≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys)
 
-------------------------------------------------------------------------
--- map
-
-map-id : map id ≗ id {A = List A}
-map-id []       = refl
-map-id (x ∷ xs) = cong (x ∷_) (map-id xs)
-
-map-id-local : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
-map-id-local []           = refl
-map-id-local (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id-local pxs)
-
-map-++ : ∀ (f : A → B) xs ys →
-                 map f (xs ++ ys) ≡ map f xs ++ map f ys
-map-++ f []       ys = refl
-map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)
-
-map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
-map-cong f≗g []       = refl
-map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
-
-map-cong-local : ∀ {f g : A → B} {xs} →
-            All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
-map-cong-local []                = refl
-map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs)
-
-length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs
-length-map f []       = refl
-length-map f (x ∷ xs) = cong suc (length-map f xs)
-
-map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
-map-∘ []       = refl
-map-∘ (x ∷ xs) = cong (_ ∷_) (map-∘ xs)
-
-map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
-map-injective finj {[]} {[]} eq = refl
-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
-
 ------------------------------------------------------------------------
 -- _++_
 
@@ -263,6 +200,46 @@ module _ (A : Set a) where
     ; ε-homo = refl
     }
 
+
+------------------------------------------------------------------------
+-- map
+
+map-id : map id ≗ id {A = List A}
+map-id []       = refl
+map-id (x ∷ xs) = cong (x ∷_) (map-id xs)
+
+map-id-local : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
+map-id-local []           = refl
+map-id-local (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id-local pxs)
+
+map-++ : ∀ (f : A → B) xs ys →
+                 map f (xs ++ ys) ≡ map f xs ++ map f ys
+map-++ f []       ys = refl
+map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)
+
+map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
+map-cong f≗g []       = refl
+map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
+
+map-cong-local : ∀ {f g : A → B} {xs} →
+            All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
+map-cong-local []                = refl
+map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs)
+
+length-map : ∀ (f : A → B) xs → length (map f xs) ≡ length xs
+length-map f []       = refl
+length-map f (x ∷ xs) = cong suc (length-map f xs)
+
+map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
+map-∘ []       = refl
+map-∘ (x ∷ xs) = cong (_ ∷_) (map-∘ xs)
+
+map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f)
+map-injective finj {[]} {[]} eq = refl
+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)
+
 ------------------------------------------------------------------------
 -- cartesianProductWith
 
@@ -740,6 +717,39 @@ map-concatMap f g xs = begin
   concatMap (map f ∘′ g) xs
     ∎
 
+------------------------------------------------------------------------
+-- 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
+
+Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)}
+  → Any (MAny P) xs → Any P (catMaybes xs)
+Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈) = Any-catMaybes⁺ x∈
+Any-catMaybes⁺ {xs = just x ∷ xs} = λ where
+  (here (just px)) → here px
+  (there x∈)       → there $ Any-catMaybes⁺ x∈
+
 ------------------------------------------------------------------------
 -- mapMaybe
 
@@ -792,6 +802,26 @@ module _ (g : B → C) (f : A → Maybe B) where
     mapMaybe (Maybe.map g) (map f xs)  ≡⟨ mapMaybe-map _ f xs ⟩
     mapMaybe (Maybe.map g ∘ f) xs      ∎
 
+mapMaybeIsInj₁∘mapInj₁ : (xs : List A) → mapMaybe (isInj₁ {B = B}) (map inj₁ xs) ≡ xs
+mapMaybeIsInj₁∘mapInj₁ = λ where
+  [] → refl
+  (x ∷ xs) → cong (x ∷_) (mapMaybeIsInj₁∘mapInj₁ xs)
+
+mapMaybeIsInj₁∘mapInj₂ : (xs : List B) → mapMaybe (isInj₁ {A = A}) (map inj₂ xs) ≡ []
+mapMaybeIsInj₁∘mapInj₂ = λ where
+  [] → refl
+  (x ∷ xs) → mapMaybeIsInj₁∘mapInj₂ xs
+
+mapMaybeIsInj₂∘mapInj₂ : (xs : List B) → mapMaybe (isInj₂ {A = A}) (map inj₂ xs) ≡ xs
+mapMaybeIsInj₂∘mapInj₂ = λ where
+  [] → refl
+  (x ∷ xs) → cong (x ∷_) (mapMaybeIsInj₂∘mapInj₂ xs)
+
+mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
+mapMaybeIsInj₂∘mapInj₁ = λ where
+  [] → refl
+  (x ∷ xs) → mapMaybeIsInj₂∘mapInj₁ xs
+
 ------------------------------------------------------------------------
 -- sum
 

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -23,7 +23,8 @@ open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
 import Data.List.Properties as Lₚ
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
-open import Function.Base using (_∘_; _⟨_⟩_)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Function.Base using (_∘_; _⟨_⟩_; _$_)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
@@ -33,11 +34,11 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Relation.Nullary
 
-private
-  variable
-    a b p : Level
-    A : Set a
-    B : Set b
+private variable
+  a b p : Level
+  A : Set a
+  B : Set b
+  xs ys : List A
 
 ------------------------------------------------------------------------
 -- Permutations of empty and singleton lists
@@ -373,3 +374,28 @@ product-↭ (swap {xs} {ys} x y r) = begin
   (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
   y * (x * product ys) ∎
   where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- catMaybes
+
+catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+catMaybes-↭ refl = refl
+catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
+catMaybes-↭ {xs = .(mx ∷ _)} {.(mx ∷ _)} (prep mx xs↭)
+  with mx
+... | nothing = catMaybes-↭ xs↭
+... | just x  = prep x $ catMaybes-↭ xs↭
+catMaybes-↭ {xs = .(mx ∷ my ∷ _)} {.(my ∷ mx ∷ _)} (swap mx my xs↭)
+  with mx | my
+... | nothing | nothing = catMaybes-↭ xs↭
+... | nothing | just y  = prep y $ catMaybes-↭ xs↭
+... | just x  | nothing = prep x $ catMaybes-↭ xs↭
+... | just x  | just y  = swap x y $ catMaybes-↭ xs↭
+
+------------------------------------------------------------------------
+-- mapMaybe
+
+module _ (f : A → Maybe B) where
+
+  mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
+  mapMaybe-↭ = catMaybes-↭ ∘ map⁺ f