Skip to content

More list properties about catMaybes/mapMaybe #2389

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 5, 2024
Merged

More list properties about catMaybes/mapMaybe #2389

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e5fdf1c
More list properties about `catMaybes/mapMaybe`
omelkonian May 23, 2024
6cf7716
Revert irrefutable `with`s for inductive hypotheses.
omelkonian Jun 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 58 additions & 42 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -343,47 +343,55 @@ 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`:
Expand Down Expand Up @@ -496,7 +504,15 @@ 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 proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`:
```agda
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
```

* Added new functions in `Data.String.Base`:
Expand Down
100 changes: 66 additions & 34 deletions src/Data/List/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,15 @@ 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 as Maybe using (Maybe; just; nothing; maybe)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
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)
Expand All @@ -48,12 +49,11 @@ open import Relation.Unary using (Pred; Decidable; ∁)
open import Relation.Unary.Properties using (∁?)
import Data.Nat.GeneralisedArithmetic as ℕ


open ≡-Reasoning

private
variable
a b c d e p : Level
a b c d e p ℓ : Level
A : Set a
B : Set b
C : Set c
Expand Down Expand Up @@ -122,32 +122,6 @@ 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

------------------------------------------------------------------------
-- _++_

Expand Down Expand Up @@ -741,12 +715,40 @@ map-concatMap f g xs = begin
∎

------------------------------------------------------------------------
-- mapMaybe
-- 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 _ ∷ xs) = s≤s $ length-catMaybes xs
length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n $ length-catMaybes xs

module _ {f g : A → Maybe B} where
catMaybes-++ : (xs ys : List (Maybe A)) →
catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
catMaybes-++ [] _ = refl
catMaybes-++ (just x ∷ xs) ys = cong (x ∷_) $ catMaybes-++ xs ys
catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys

mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g
map-catMaybes : (f : A → B) → map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
map-catMaybes _ [] = refl
map-catMaybes f (just x ∷ xs) = cong (f x ∷_) $ map-catMaybes f xs
map-catMaybes f (nothing ∷ xs) = map-catMaybes f 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} (here (just px)) = here px
Any-catMaybes⁺ {xs = just x ∷ xs} (there x∈) = there $ Any-catMaybes⁺ x∈

------------------------------------------------------------------------
-- mapMaybe

mapMaybe-cong : {f g : A → Maybe B} → f ≗ g → mapMaybe f ≗ mapMaybe g
mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g

mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
mapMaybe-just [] = refl
Expand Down Expand Up @@ -792,6 +794,36 @@ 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 ∎

-- embedding-projection pairs
module _ {proj : B → Maybe A} {emb : A → B} where
mapMaybe-map-retract : proj ∘ emb ≗ just → mapMaybe proj ∘ map emb ≗ id
mapMaybe-map-retract retract xs = begin
mapMaybe proj (map emb xs) ≡⟨ mapMaybe-map _ _ xs ⟩
mapMaybe (proj ∘ emb) xs ≡⟨ mapMaybe-cong retract xs ⟩
mapMaybe just xs ≡⟨ mapMaybe-just _ ⟩
xs ∎

module _ {proj : C → Maybe B} {emb : A → C} where
mapMaybe-map-none : proj ∘ emb ≗ const nothing → mapMaybe proj ∘ map emb ≗ const []
mapMaybe-map-none retract xs = begin
mapMaybe proj (map emb xs) ≡⟨ mapMaybe-map _ _ xs ⟩
mapMaybe (proj ∘ emb) xs ≡⟨ mapMaybe-cong retract xs ⟩
mapMaybe (const nothing) xs ≡⟨ mapMaybe-nothing xs ⟩
[] ∎

-- embedding-projection pairs on sums
mapMaybeIsInj₁∘mapInj₁ : (xs : List A) → mapMaybe (isInj₁ {B = B}) (map inj₁ xs) ≡ xs
mapMaybeIsInj₁∘mapInj₁ = mapMaybe-map-retract λ _ → refl

mapMaybeIsInj₁∘mapInj₂ : (xs : List B) → mapMaybe (isInj₁ {A = A}) (map inj₂ xs) ≡ []
mapMaybeIsInj₁∘mapInj₂ = mapMaybe-map-none λ _ → refl

mapMaybeIsInj₂∘mapInj₂ : (xs : List B) → mapMaybe (isInj₂ {A = A}) (map inj₂ xs) ≡ xs
mapMaybeIsInj₂∘mapInj₂ = mapMaybe-map-retract λ _ → refl

mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
mapMaybeIsInj₂∘mapInj₁ = mapMaybe-map-none λ _ → refl

------------------------------------------------------------------------
-- sum

Expand Down
23 changes: 22 additions & 1 deletion src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₂_⟶_⟶_)
Expand All @@ -38,6 +39,7 @@ private
a b p : Level
A : Set a
B : Set b
xs ys : List A

------------------------------------------------------------------------
-- Permutations of empty and singleton lists
Expand Down Expand Up @@ -373,3 +375,22 @@ 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-↭ (prep nothing xs↭) = catMaybes-↭ xs↭
catMaybes-↭ (prep (just x) xs↭) = prep x $ catMaybes-↭ xs↭
catMaybes-↭ (swap nothing nothing xs↭) = catMaybes-↭ xs↭
catMaybes-↭ (swap nothing (just y) xs↭) = prep y $ catMaybes-↭ xs↭
catMaybes-↭ (swap (just x) nothing xs↭) = prep x $ catMaybes-↭ xs↭
catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭

------------------------------------------------------------------------
-- mapMaybe

mapMaybe-↭ : (f : A → Maybe B) → xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ steps-respʳ ys≋xs (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_)
------------------------------------------------------------------------
-- map

module _ (T : Setoid b ℓ) where
module _ {ℓ} (T : Setoid b ℓ) where

open Setoid T using () renaming (_≈_ to _≈′_)
open Permutation T using () renaming (_↭_ to _↭′_)
Expand Down
70 changes: 70 additions & 0 deletions src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of permutations using setoid equality (on Maybe elements)
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe where

open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.Bundles using (Setoid)

open import Level using (Level)
open import Function.Base using (_∘_; _$_)

open import Data.List.Base using (catMaybes; mapMaybe)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
open import Data.List.Relation.Binary.Permutation.Setoid.Properties

open import Data.Maybe using (Maybe; nothing; just)
open import Data.Maybe.Relation.Binary.Pointwise using (nothing; just)
renaming (setoid to setoidᴹ)

private
variable
a b ℓ ℓ′ : Level

------------------------------------------------------------------------
-- catMaybes

module _ (sᴬ : Setoid a ℓ) where
open Setoid sᴬ using (_≈_)
open Permutation sᴬ

private sᴹ = setoidᴹ sᴬ
open Setoid sᴹ using () renaming (_≈_ to _≈ᴹ_)
open Permutation sᴹ using () renaming (_↭_ to _↭ᴹ_)

catMaybes-↭ : ∀ {xs ys} → xs ↭ᴹ ys → catMaybes xs ↭ catMaybes ys
catMaybes-↭ (refl p) = refl (pointwise p)
where
pointwise : ∀ {xs ys} → Pointwise _≈ᴹ_ xs ys →
Pointwise _≈_ (catMaybes xs) (catMaybes ys)
pointwise [] = []
pointwise (just p ∷ ps) = p ∷ pointwise ps
pointwise (nothing ∷ ps) = pointwise ps
catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
catMaybes-↭ (prep nothing xs↭) = catMaybes-↭ xs↭
catMaybes-↭ (prep (just x~y) xs↭) = prep x~y $ catMaybes-↭ xs↭
catMaybes-↭ (swap nothing nothing xs↭) = catMaybes-↭ xs↭
catMaybes-↭ (swap nothing (just y) xs↭) = prep y $ catMaybes-↭ xs↭
catMaybes-↭ (swap (just x) nothing xs↭) = prep x $ catMaybes-↭ xs↭
catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭

------------------------------------------------------------------------
-- mapMaybe

module _ (sᴬ : Setoid a ℓ) (sᴮ : Setoid b ℓ′) where
open Setoid sᴬ using () renaming (_≈_ to _≈ᴬ_)
open Permutation sᴬ using () renaming (_↭_ to _↭ᴬ_)
open Permutation sᴮ using () renaming (_↭_ to _↭ᴮ_)

private sᴹᴮ = setoidᴹ sᴮ
open Setoid sᴹᴮ using () renaming (_≈_ to _≈ᴹᴮ_)

mapMaybe-↭ : ∀ {f} → f Preserves _≈ᴬ_ ⟶ _≈ᴹᴮ_ →
∀ {xs ys} → xs ↭ᴬ ys → mapMaybe f xs ↭ᴮ mapMaybe f ys
mapMaybe-↭ pres = catMaybes-↭ sᴮ ∘ map⁺ sᴬ sᴹᴮ pres