Skip to content

Commit 622c19b

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 622c19b

File tree

3 files changed

+151
-78
lines changed

3 files changed

+151
-78
lines changed

‎CHANGELOG.md

+51-42
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,9 @@ 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
500509
```
501510

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

‎src/Data/List/Properties.agda

+64-30
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

@@ -740,6 +714,50 @@ map-concatMap f g xs = begin
740714
concatMap (map f ∘′ g) xs
741715
∎
742716

717+
------------------------------------------------------------------------
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+
module _ (f : A → B) where
746+
747+
map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
748+
map-catMaybes [] = refl
749+
map-catMaybes (mx ∷ xs)
750+
with IH ← map-catMaybes xs
751+
with mx
752+
... | just x = cong (f x ∷_) IH
753+
... | nothing = IH
754+
755+
Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)}
756+
→ Any (MAny P) xs → Any P (catMaybes xs)
757+
Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈) = Any-catMaybes⁺ x∈
758+
Any-catMaybes⁺ {xs = just x ∷ xs} (here (just px)) = here px
759+
Any-catMaybes⁺ {xs = just x ∷ xs} (there x∈) = there $ Any-catMaybes⁺ x∈
760+
743761
------------------------------------------------------------------------
744762
-- mapMaybe
745763

@@ -792,6 +810,22 @@ module _ (g : B → C) (f : A → Maybe B) where
792810
mapMaybe (Maybe.map g) (map f xs) ≡⟨ mapMaybe-map _ f xs ⟩
793811
mapMaybe (Maybe.map g ∘ f) xs ∎
794812

813+
mapMaybeIsInj₁∘mapInj₁ : (xs : List A) → mapMaybe (isInj₁ {B = B}) (map inj₁ xs) ≡ xs
814+
mapMaybeIsInj₁∘mapInj₁ [] = refl
815+
mapMaybeIsInj₁∘mapInj₁ (x ∷ xs) = cong (x ∷_) (mapMaybeIsInj₁∘mapInj₁ xs)
816+
817+
mapMaybeIsInj₁∘mapInj₂ : (xs : List B) → mapMaybe (isInj₁ {A = A}) (map inj₂ xs) ≡ []
818+
mapMaybeIsInj₁∘mapInj₂ [] = refl
819+
mapMaybeIsInj₁∘mapInj₂ (x ∷ xs) = mapMaybeIsInj₁∘mapInj₂ xs
820+
821+
mapMaybeIsInj₂∘mapInj₂ : (xs : List B) → mapMaybe (isInj₂ {A = A}) (map inj₂ xs) ≡ xs
822+
mapMaybeIsInj₂∘mapInj₂ [] = refl
823+
mapMaybeIsInj₂∘mapInj₂ (x ∷ xs) = cong (x ∷_) (mapMaybeIsInj₂∘mapInj₂ xs)
824+
825+
mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
826+
mapMaybeIsInj₂∘mapInj₁ [] = refl
827+
mapMaybeIsInj₂∘mapInj₁ (x ∷ xs) = mapMaybeIsInj₂∘mapInj₁ xs
828+
795829
------------------------------------------------------------------------
796830
-- sum
797831

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

+36-6
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₂_⟶_⟶_)
@@ -33,11 +34,11 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
3334
open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
3435
open import Relation.Nullary
3536

36-
private
37-
variable
38-
a b p : Level
39-
A : Set a
40-
B : Set b
37+
private variable
38+
a b p : Level
39+
A : Set a
40+
B : Set b
41+
xs ys : List A
4142

4243
------------------------------------------------------------------------
4344
-- Permutations of empty and singleton lists
@@ -373,3 +374,32 @@ product-↭ (swap {xs} {ys} x y r) = begin
373374
(y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
374375
y * (x * product ys) ∎
375376
where open ≡-Reasoning
377+
378+
------------------------------------------------------------------------
379+
-- catMaybes
380+
381+
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
382+
catMaybes-↭ refl = refl
383+
catMaybes-↭ (trans xs↭ ↭ys) = trans (catMaybes-↭ xs↭) (catMaybes-↭ ↭ys)
384+
catMaybes-↭ {xs = .mx ∷ xs} {.mx ∷ ys} (prep mx xs↭)
385+
with IH ← catMaybes-↭ xs↭
386+
with mx
387+
... | nothing = IH
388+
... | just x = prep x IH
389+
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+
------------------------------------------------------------------------
400+
-- mapMaybe
401+
402+
module _ (f : A → Maybe B) where
403+
404+
mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
405+
mapMaybe-↭ = catMaybes-↭ ∘ map⁺ f

0 commit comments

Comments
 (0)