Skip to content

Commit 8d831bf

Browse files
omelkonianomelkonian
committed
More list properties about catMaybes/mapMaybe
- Follow-up to PR #2361 - Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256)
1 parent c5255d0 commit 8d831bf

File tree

5 files changed

+226
-78
lines changed

5 files changed

+226
-78
lines changed

‎CHANGELOG.md‎

Lines changed: 57 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -343,47 +343,54 @@ Additions to existing modules
343343

344344
* In `Data.List.Properties`:
345345
```agda
346-
length-catMaybes : length (catMaybes xs) ≤ length xs
347-
applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
348-
applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
349-
upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n)
350-
downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
351-
reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse
352-
reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n
353-
reverse-upTo : reverse (upTo n) ≡ downFrom n
354-
reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
355-
reverse-downFrom : reverse (downFrom n) ≡ upTo n
356-
mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
357-
map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
358-
align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys)
359-
zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys)
360-
unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
361-
map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f)
362-
unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip
363-
splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n
364-
uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons
365-
last-map : last ∘ map f ≗ map f ∘ last
366-
tail-map : tail ∘ map f ≗ map (map f) ∘ tail
367-
mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
368-
zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
369-
unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g
370-
foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
371-
alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
372-
alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
373-
align-flip : align xs ys ≡ map swap (align ys xs)
374-
zip-flip : zip xs ys ≡ map swap (zip ys xs)
375-
unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f
376-
unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip
377-
take-take : take n (take m xs) ≡ take (n ⊓ m) xs
378-
take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs)
379-
zip-unzip : uncurry′ zip ∘ unzip ≗ id
380-
unzipWith-zipWith : f ∘ uncurry′ g ≗ id → length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys)
381-
unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
382-
mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
383-
unzipWith-++ : unzipWith f (xs ++ ys) ≡ zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
384-
catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe
385-
catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
386-
map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
346+
length-catMaybes : length (catMaybes xs) ≤ length xs
347+
applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
348+
applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
349+
upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n)
350+
downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
351+
reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse
352+
reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n
353+
reverse-upTo : reverse (upTo n) ≡ downFrom n
354+
reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
355+
reverse-downFrom : reverse (downFrom n) ≡ upTo n
356+
mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
357+
map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
358+
align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys)
359+
zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys)
360+
unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
361+
map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f)
362+
unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip
363+
splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n
364+
uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons
365+
last-map : last ∘ map f ≗ map f ∘ last
366+
tail-map : tail ∘ map f ≗ map (map f) ∘ tail
367+
mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
368+
zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
369+
unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g
370+
foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
371+
alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
372+
alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
373+
align-flip : align xs ys ≡ map swap (align ys xs)
374+
zip-flip : zip xs ys ≡ map swap (zip ys xs)
375+
unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f
376+
unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip
377+
take-take : take n (take m xs) ≡ take (n ⊓ m) xs
378+
take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs)
379+
zip-unzip : uncurry′ zip ∘ unzip ≗ id
380+
unzipWith-zipWith : f ∘ uncurry′ g ≗ id → length xs ≡
381+
length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys)
382+
unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
383+
mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
384+
unzipWith-++ : unzipWith f (xs ++ ys) ≡
385+
zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
386+
catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe
387+
catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
388+
map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
389+
Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs)
390+
mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs
391+
mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ []
392+
mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs
393+
mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ []
387394
```
388395

389396
* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
@@ -496,7 +503,15 @@ Additions to existing modules
496503

497504
* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
498505
```agda
499-
product-↭ : product Preserves _↭_ ⟶ _≡_
506+
product-↭ : product Preserves _↭_ ⟶ _≡_
507+
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
508+
mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
509+
```
510+
511+
* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`:
512+
```agda
513+
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
514+
mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
500515
```
501516

502517
* Added new functions in `Data.String.Base`:

‎src/Data/List/Properties.agda‎

Lines changed: 64 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,15 @@ open import Data.List.Base as List
2323
open import Data.List.Membership.Propositional using (_∈_)
2424
open import Data.List.Relation.Unary.All using (All; []; _∷_)
2525
open import Data.List.Relation.Unary.Any using (Any; here; there)
26-
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe)
26+
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
27+
open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
2728
open import Data.Nat.Base
2829
open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
2930
open import Data.Nat.Properties
3031
open import Data.Product.Base as Product
3132
using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
3233
import Data.Product.Relation.Unary.All as Product using (All)
33-
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
34+
open import Data.Sum using (_⊎_; inj₁; inj₂; isInj₁; isInj₂)
3435
open import Data.These.Base as These using (These; this; that; these)
3536
open import Data.Fin.Properties using (toℕ-cast)
3637
open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
@@ -48,12 +49,11 @@ open import Relation.Unary using (Pred; Decidable; ∁)
4849
open import Relation.Unary.Properties using (∁?)
4950
import Data.Nat.GeneralisedArithmetic as ℕ
5051

51-
5252
open ≡-Reasoning
5353

5454
private
5555
variable
56-
a b c d e p : Level
56+
a b c d e p ℓ : Level
5757
A : Set a
5858
B : Set b
5959
C : Set c
@@ -122,32 +122,6 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
122122
let fx≡fy , fxs≡fys = ∷-injective eq in
123123
cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys)
124124

125-
------------------------------------------------------------------------
126-
-- catMaybes
127-
128-
catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe
129-
catMaybes-concatMap [] = refl
130-
catMaybes-concatMap (just x ∷ xs) = cong (x ∷_) (catMaybes-concatMap xs)
131-
catMaybes-concatMap (nothing ∷ xs) = catMaybes-concatMap xs
132-
133-
length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
134-
length-catMaybes [] = ≤-refl
135-
length-catMaybes (just x ∷ xs) = s≤s (length-catMaybes xs)
136-
length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs)
137-
138-
catMaybes-++ : (xs ys : List (Maybe A)) →
139-
catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
140-
catMaybes-++ [] ys = refl
141-
catMaybes-++ (just x ∷ xs) ys = cong (x ∷_) (catMaybes-++ xs ys)
142-
catMaybes-++ (nothing ∷ xs) ys = catMaybes-++ xs ys
143-
144-
module _ (f : A → B) where
145-
146-
map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
147-
map-catMaybes [] = refl
148-
map-catMaybes (just x ∷ xs) = cong (f x ∷_) (map-catMaybes xs)
149-
map-catMaybes (nothing ∷ xs) = map-catMaybes xs
150-
151125
------------------------------------------------------------------------
152126
-- _++_
153127

@@ -741,12 +715,52 @@ map-concatMap f g xs = begin
741715
∎
742716

743717
------------------------------------------------------------------------
744-
-- mapMaybe
718+
-- catMaybes
719+
720+
catMaybes-concatMap : catMaybes {A = A} ≗ concatMap fromMaybe
721+
catMaybes-concatMap [] = refl
722+
catMaybes-concatMap (mx ∷ xs)
723+
with IH ← catMaybes-concatMap xs
724+
with mx
725+
... | just x = cong (x ∷_) IH
726+
... | nothing = IH
727+
728+
length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
729+
length-catMaybes [] = ≤-refl
730+
length-catMaybes (mx ∷ xs)
731+
with IH ← length-catMaybes xs
732+
with mx
733+
... | just _ = s≤s IH
734+
... | nothing = m≤n⇒m≤1+n IH
735+
736+
catMaybes-++ : (xs ys : List (Maybe A)) →
737+
catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
738+
catMaybes-++ [] _ = refl
739+
catMaybes-++ (mx ∷ xs) ys
740+
with IH ← catMaybes-++ xs ys
741+
with mx
742+
... | just x = cong (x ∷_) IH
743+
... | nothing = IH
744+
745+
map-catMaybes : (f : A → B) → map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
746+
map-catMaybes _ [] = refl
747+
map-catMaybes f (mx ∷ xs)
748+
with IH ← map-catMaybes f xs
749+
with mx
750+
... | just x = cong (f x ∷_) IH
751+
... | nothing = IH
752+
753+
Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} →
754+
Any (MAny P) xs → Any P (catMaybes xs)
755+
Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈) = Any-catMaybes⁺ x∈
756+
Any-catMaybes⁺ {xs = just x ∷ xs} (here (just px)) = here px
757+
Any-catMaybes⁺ {xs = just x ∷ xs} (there x∈) = there $ Any-catMaybes⁺ x∈
745758

746-
module _ {f g : A → Maybe B} where
759+
------------------------------------------------------------------------
760+
-- mapMaybe
747761

748-
mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
749-
mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g
762+
mapMaybe-cong : {f g : A → Maybe B} → f ≗ g → mapMaybe f ≗ mapMaybe g
763+
mapMaybe-cong f≗g = cong catMaybes ∘ map-cong f≗g
750764

751765
mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
752766
mapMaybe-just [] = refl
@@ -792,6 +806,22 @@ module _ (g : B → C) (f : A → Maybe B) where
792806
mapMaybe (Maybe.map g) (map f xs) ≡⟨ mapMaybe-map _ f xs ⟩
793807
mapMaybe (Maybe.map g ∘ f) xs ∎
794808

809+
mapMaybeIsInj₁∘mapInj₁ : (xs : List A) → mapMaybe (isInj₁ {B = B}) (map inj₁ xs) ≡ xs
810+
mapMaybeIsInj₁∘mapInj₁ [] = refl
811+
mapMaybeIsInj₁∘mapInj₁ (x ∷ xs) = cong (x ∷_) (mapMaybeIsInj₁∘mapInj₁ xs)
812+
813+
mapMaybeIsInj₁∘mapInj₂ : (xs : List B) → mapMaybe (isInj₁ {A = A}) (map inj₂ xs) ≡ []
814+
mapMaybeIsInj₁∘mapInj₂ [] = refl
815+
mapMaybeIsInj₁∘mapInj₂ (x ∷ xs) = mapMaybeIsInj₁∘mapInj₂ xs
816+
817+
mapMaybeIsInj₂∘mapInj₂ : (xs : List B) → mapMaybe (isInj₂ {A = A}) (map inj₂ xs) ≡ xs
818+
mapMaybeIsInj₂∘mapInj₂ [] = refl
819+
mapMaybeIsInj₂∘mapInj₂ (x ∷ xs) = cong (x ∷_) (mapMaybeIsInj₂∘mapInj₂ xs)
820+
821+
mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
822+
mapMaybeIsInj₂∘mapInj₁ [] = refl
823+
mapMaybeIsInj₂∘mapInj₁ (x ∷ xs) = mapMaybeIsInj₂∘mapInj₁ xs
824+
795825
------------------------------------------------------------------------
796826
-- sum
797827

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

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,8 @@ open import Data.List.Membership.Propositional
2323
open import Data.List.Membership.Propositional.Properties
2424
import Data.List.Properties as Lₚ
2525
open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
26-
open import Function.Base using (_∘_; _⟨_⟩_)
26+
open import Data.Maybe.Base using (Maybe; just; nothing)
27+
open import Function.Base using (_∘_; _⟨_⟩_; _$_)
2728
open import Level using (Level)
2829
open import Relation.Unary using (Pred)
2930
open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
@@ -38,6 +39,7 @@ private
3839
a b p : Level
3940
A : Set a
4041
B : Set b
42+
xs ys : List A
4143

4244
------------------------------------------------------------------------
4345
-- Permutations of empty and singleton lists
@@ -373,3 +375,28 @@ product-↭ (swap {xs} {ys} x y r) = begin
373375
(y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
374376
y * (x * product ys) ∎
375377
where open ≡-Reasoning
378+
379+
------------------------------------------------------------------------
380+
-- catMaybes
381+
382+
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
383+
catMaybes-↭ refl = refl
384+
catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
385+
catMaybes-↭ {xs = .mx ∷ xs} {.mx ∷ ys} (prep mx xs↭)
386+
with IH ← catMaybes-↭ xs↭
387+
with mx
388+
... | nothing = IH
389+
... | just x = prep x IH
390+
catMaybes-↭ {xs = .mx ∷ .my ∷ xs} {.my ∷ .mx ∷ ys} (swap mx my xs↭)
391+
with IH ← catMaybes-↭ xs↭
392+
with mx | my
393+
... | nothing | nothing = IH
394+
... | nothing | just y = prep y IH
395+
... | just x | nothing = prep x IH
396+
... | just x | just y = swap x y IH
397+
398+
------------------------------------------------------------------------
399+
-- mapMaybe
400+
401+
mapMaybe-↭ : (f : A → Maybe B) → xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
402+
mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f

‎src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ steps-respʳ ys≋xs (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_)
144144
------------------------------------------------------------------------
145145
-- map
146146

147-
module _ (T : Setoid b ℓ) where
147+
module _ {ℓ} (T : Setoid b ℓ) where
148148

149149
open Setoid T using () renaming (_≈_ to _≈′_)
150150
open Permutation T using () renaming (_↭_ to _↭′_)

‎src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of permutations using setoid equality (on Maybe elements)
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
module Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe where
10+
11+
open import Relation.Binary.Core using (_Preserves_⟶_)
12+
open import Relation.Binary.Bundles using (Setoid)
13+
14+
open import Level using (Level)
15+
open import Function.Base using (_∘_)
16+
17+
open import Data.List.Base using (catMaybes; mapMaybe)
18+
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
19+
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
20+
open import Data.List.Relation.Binary.Permutation.Setoid.Properties
21+
22+
open import Data.Maybe using (Maybe; nothing; just)
23+
open import Data.Maybe.Relation.Binary.Pointwise using (nothing; just)
24+
renaming (setoid to setoidᴹ)
25+
26+
private
27+
variable
28+
a b ℓ ℓ′ : Level
29+
30+
------------------------------------------------------------------------
31+
-- catMaybes
32+
33+
module _ (sᴬ : Setoid a ℓ) where
34+
open Setoid sᴬ using () renaming (_≈_ to _≈_)
35+
open Permutation sᴬ
36+
37+
private sᴹ = setoidᴹ sᴬ
38+
open Setoid sᴹ using () renaming (_≈_ to _≈ᴹ_)
39+
open Permutation sᴹ using () renaming (_↭_ to _↭ᴹ_)
40+
41+
catMaybes-↭ : ∀ {xs ys} → xs ↭ᴹ ys → catMaybes xs ↭ catMaybes ys
42+
catMaybes-↭ (refl p) = refl (pointwise p)
43+
where
44+
pointwise : ∀ {xs ys} → Pointwise _≈ᴹ_ xs ys →
45+
Pointwise _≈_ (catMaybes xs) (catMaybes ys)
46+
pointwise [] = []
47+
pointwise (just p ∷ ps) = p ∷ pointwise ps
48+
pointwise (nothing ∷ ps) = pointwise ps
49+
catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
50+
catMaybes-↭ (prep p xs↭) with IH ← catMaybes-↭ xs↭
51+
with p
52+
... | nothing = IH
53+
... | just x~y = prep x~y IH
54+
catMaybes-↭ (swap p q xs↭) with IH ← catMaybes-↭ xs↭
55+
with p | q
56+
... | nothing | nothing = IH
57+
... | nothing | just y = prep y IH
58+
... | just x | nothing = prep x IH
59+
... | just x | just y = swap x y IH
60+
61+
62+
module _ (sᴬ : Setoid a ℓ) (sᴮ : Setoid b ℓ′) where
63+
open Setoid sᴬ using () renaming (_≈_ to _≈ᴬ_)
64+
open Permutation sᴬ using () renaming (_↭_ to _↭ᴬ_)
65+
66+
open Setoid sᴮ using () renaming (_≈_ to _≈ᴮ_)
67+
open Permutation sᴮ using () renaming (_↭_ to _↭ᴮ_)
68+
69+
private sᴹᴮ = setoidᴹ sᴮ
70+
open Setoid sᴹᴮ using () renaming (_≈_ to _≈ᴹᴮ_)
71+
open Permutation sᴹᴮ using () renaming (_↭_ to _↭ᴹᴮ_)
72+
73+
mapMaybe-↭ :
74+
∀ {f} → f Preserves _≈ᴬ_ ⟶ _≈ᴹᴮ_ →
75+
∀ {xs ys} → xs ↭ᴬ ys → mapMaybe f xs ↭ᴮ mapMaybe f ys
76+
mapMaybe-↭ pres = catMaybes-↭ sᴮ ∘ map⁺ sᴬ sᴹᴮ pres

0 commit comments

Comments
 (0)