Skip to content

Commit 3590a48

Browse files
jamesmckinnajamesmckinna
authored
Make names of container lemmas relating map and other functions more consistent (#1822)
1 parent 81a924e commit 3590a48

File tree

22 files changed

+828
-233
lines changed

22 files changed

+828
-233
lines changed

‎CHANGELOG.md

+134
Original file line numberDiff line numberDiff line change
@@ -685,6 +685,42 @@ Deprecated modules
685685
Deprecated names
686686
----------------
687687

688+
* In `Codata.Guarded.Stream.Properties`:
689+
```agda
690+
map-identity ↦ map-id
691+
map-fusion ↦ map-∘
692+
```
693+
694+
* In `Codata.Sized.Colist.Properties`:
695+
```agda
696+
map-identity ↦ map-id
697+
map-map-fusion ↦ map-∘
698+
```
699+
700+
* In `Codata.Sized.Covec.Properties`:
701+
```agda
702+
map-identity ↦ map-id
703+
map-map-fusion ↦ map-∘
704+
```
705+
706+
* In `Codata.Sized.Delay.Properties`:
707+
```agda
708+
map-identity ↦ map-id
709+
map-map-fusion ↦ map-∘
710+
map-unfold-fusion ↦ map-unfold
711+
```
712+
713+
* In `Codata.Sized.M.Properties`:
714+
```agda
715+
map-compose ↦ map-∘
716+
```
717+
718+
* In `Codata.Sized.Stream.Properties`:
719+
```agda
720+
map-identity ↦ map-id
721+
map-map-fusion ↦ map-∘
722+
```
723+
688724
* In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ`
689725
for the 'left', resp. 'right' injection of a Fin m into a 'larger' type,
690726
`Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the
@@ -768,10 +804,52 @@ Deprecated names
768804

769805
* In `Data.List.Properties`:
770806
```agda
807+
map-id₂ ↦ map-id-local
808+
map-cong₂ ↦ map-cong-local
809+
map-compose ↦ map-∘
810+
811+
map-++-commute ↦ map-++
812+
sum-++-commute ↦ sum-++
813+
reverse-map-commute ↦ reverse-map
814+
reverse-++-commute ↦ reverse-++
815+
771816
zipWith-identityˡ ↦ zipWith-zeroˡ
772817
zipWith-identityʳ ↦ zipWith-zeroʳ
773818
```
774819

820+
* In `Data.List.NonEmpty.Properties`:
821+
```agda
822+
map-compose ↦ map-∘
823+
824+
map-++⁺-commute ↦ map-++⁺
825+
```
826+
827+
* In `Data.List.Relation.Unary.All.Properties`:
828+
```agda
829+
updateAt-id-relative ↦ updateAt-id-local
830+
updateAt-compose-relative ↦ updateAt-∘-local
831+
updateAt-compose ↦ updateAt-∘
832+
updateAt-cong-relative ↦ updateAt-cong-local
833+
```
834+
835+
* In `Data.List.Zipper.Properties`:
836+
```agda
837+
toList-reverse-commute ↦ toList-reverse
838+
toList-ˡ++-commute ↦ toList-ˡ++
839+
toList-++ʳ-commute ↦ toList-++ʳ
840+
toList-map-commute ↦ toList-map
841+
toList-foldr-commute ↦ toList-foldr
842+
```
843+
844+
* In `Data.Maybe.Properties`:
845+
```agda
846+
map-id₂ ↦ map-id-local
847+
map-cong₂ ↦ map-cong-local
848+
849+
map-compose ↦ map-∘
850+
851+
map-<∣>-commute ↦ map-<∣>
852+
775853
* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
776854
```
777855
map-with-∈⁺ ↦ mapWith∈⁺
@@ -819,8 +897,38 @@ Deprecated names
819897
negative<positive ↦ neg<pos
820898
```
821899
900+
* In `Data.Sum.Properties`:
901+
```agda
902+
[,]-∘-distr ↦ [,]-∘
903+
[,]-map-commute ↦ [,]-map
904+
map-commute ↦ map-map
905+
map₁₂-commute ↦ map₁₂-map₂₁
906+
```
907+
908+
* In `Data.Tree.Binary.Zipper.Properties`:
909+
```
910+
toTree-#nodes-commute ↦ toTree-#nodes
911+
toTree-#leaves-commute ↦ toTree-#leaves
912+
toTree-map-commute ↦ toTree-map
913+
toTree-foldr-commute ↦ toTree-foldr
914+
toTree-⟪⟫ˡ-commute ↦ toTree--⟪⟫ˡ
915+
toTree-⟪⟫ʳ-commute ↦ toTree-⟪⟫ʳ
916+
```
917+
918+
* In `Data.Tree.Rose.Properties`:
919+
```agda
920+
map-compose ↦ map-∘
921+
```
922+
822923
* In `Data.Vec.Properties`:
823924
```
925+
updateAt-id-relative ↦ updateAt-id-local
926+
updateAt-compose-relative ↦ updateAt-∘-local
927+
updateAt-compose ↦ updateAt-∘
928+
updateAt-cong-relative ↦ updateAt-cong-local
929+
930+
[]%=-compose ↦ []%=-∘
931+
824932
[]≔-++-inject+ ↦ []≔-++-↑ˡ
825933
[]≔-++-raise ↦ []≔-++-↑ʳ
826934
idIsFold ↦ id-is-foldr
@@ -835,6 +943,27 @@ Deprecated names
835943
zipWith-comm : ∀ {f : A → B → C} {g : B → A → C} (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs
836944
```
837945

946+
* In `Data.Vec.Functional.Properties`:
947+
```
948+
updateAt-id-relative ↦ updateAt-id-local
949+
updateAt-compose-relative ↦ updateAt-∘-local
950+
updateAt-compose ↦ updateAt-∘
951+
updateAt-cong-relative ↦ updateAt-cong-local
952+
953+
map-updateAt ↦ map-updateAt-local
954+
```
955+
NB. This last one is complicated by the *addition* of a 'global' property `map-updateAt`
956+
957+
* In `Data.Vec.Recursive.Properties`:
958+
```
959+
append-cons-commute ↦ append-cons
960+
```
961+
962+
* In `Data.Vec.Relation.Binary.Equality.Setoid`:
963+
```agda
964+
map-++-commute ↦ map-++
965+
```
966+
838967
* In `Function.Construct.Composition`:
839968
```
840969
_∘-⟶_ ↦ _⟶-∘_
@@ -1725,6 +1854,11 @@ Other minor changes
17251854
transpose-replicate : transpose (replicate xs) ≡ map replicate xs
17261855
```
17271856

1857+
* Added new proofs in `Data.Vec.Functional.Properties`:
1858+
```
1859+
map-updateAt : f ∘ g ≗ h ∘ f → map f (updateAt i g xs) ≗ updateAt i h (map f xs)
1860+
```
1861+
17281862
* Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`:
17291863
```agda
17301864
xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []

‎src/Codata/Guarded/Stream/Properties.agda

+26-6
Original file line numberDiff line numberDiff line change
@@ -134,13 +134,13 @@ map-const : (a : A) (bs : Stream B) → map (const a) bs ≈ repeat a
134134
map-const a bs .head = P.refl
135135
map-const a bs .tail = map-const a (bs .tail)
136136

137-
map-identity : (as : Stream A) → map id as ≈ as
138-
map-identity as .head = P.refl
139-
map-identity as .tail = map-identity (as .tail)
137+
map-id : (as : Stream A) → map id as ≈ as
138+
map-id as .head = P.refl
139+
map-id as .tail = map-id (as .tail)
140140

141-
map-fusion : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as
142-
map-fusion g f as .head = P.refl
143-
map-fusion g f as .tail = map-fusion g f (as .tail)
141+
map-∘ : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as
142+
map-∘ g f as .head = P.refl
143+
map-∘ g f as .tail = map-∘ g f (as .tail)
144144

145145
map-unfold : ∀ (g : B → C) (f : A → A × B) a →
146146
map g (unfold f a) ≈ unfold (Prod.map₂ g ∘′ f) a
@@ -311,3 +311,23 @@ interleave-evens-odds : (as : Stream A) → interleave (evens as) (odds as) ≈
311311
interleave-evens-odds as .head = P.refl
312312
interleave-evens-odds as .tail .head = P.refl
313313
interleave-evens-odds as .tail .tail = interleave-evens-odds (as .tail .tail)
314+
315+
------------------------------------------------------------------------
316+
-- DEPRECATED
317+
------------------------------------------------------------------------
318+
-- Please use the new names as continuing support for the old names is
319+
-- not guaranteed.
320+
321+
-- Version 2.0
322+
323+
map-identity = map-id
324+
{-# WARNING_ON_USAGE map-identity
325+
"Warning: map-identity was deprecated in v2.0.
326+
Please use map-id instead."
327+
#-}
328+
329+
map-fusion = map-∘
330+
{-# WARNING_ON_USAGE map-fusion
331+
"Warning: map-fusion was deprecated in v2.0.
332+
Please use map-∘ instead."
333+
#-}

‎src/Codata/Sized/Colist/Properties.agda

+29-9
Original file line numberDiff line numberDiff line change
@@ -45,15 +45,15 @@ private
4545
------------------------------------------------------------------------
4646
-- Functor laws
4747

48-
map-identity : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as
49-
map-identity [] = []
50-
map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)
48+
map-id : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as
49+
map-id [] = []
50+
map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force)
5151

52-
map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} →
52+
map-∘ : ∀ (f : A → B) (g : B → C) as {i} →
5353
i ⊢ map g (map f as) ≈ map (g ∘ f) as
54-
map-map-fusion f g [] = []
55-
map-map-fusion f g (a ∷ as) =
56-
Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)
54+
map-∘ f g [] = []
55+
map-∘ f g (a ∷ as) =
56+
Eq.refl ∷ λ where .force → map-∘ f g (as .force)
5757

5858
------------------------------------------------------------------------
5959
-- Relation to Cowriter
@@ -161,8 +161,8 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where
161161

162162
map-alignWith : ∀ (f : C → D) (al : These A B → C) as bs →
163163
i ⊢ map f (alignWith al as bs) ≈ alignWith (f ∘ al) as bs
164-
map-alignWith f al [] bs = map-map-fusion (al ∘′ that) f bs
165-
map-alignWith f al as@(_ ∷ _) [] = map-map-fusion (al ∘′ this) f as
164+
map-alignWith f al [] bs = map-∘ (al ∘′ that) f bs
165+
map-alignWith f al as@(_ ∷ _) [] = map-∘ (al ∘′ this) f as
166166
map-alignWith f al (a ∷ as) (b ∷ bs) =
167167
Eq.refl ∷ λ where .force → map-alignWith f al (as .force) (bs .force)
168168

@@ -331,3 +331,23 @@ map-fromStream : ∀ (f : A → B) as →
331331
i ⊢ map f (fromStream as) ≈ fromStream (Stream.map f as)
332332
map-fromStream f (a ∷ as) =
333333
Eq.refl ∷ λ where .force → map-fromStream f (as .force)
334+
335+
------------------------------------------------------------------------
336+
-- DEPRECATED
337+
------------------------------------------------------------------------
338+
-- Please use the new names as continuing support for the old names is
339+
-- not guaranteed.
340+
341+
-- Version 2.0
342+
343+
map-identity = map-id
344+
{-# WARNING_ON_USAGE map-identity
345+
"Warning: map-identity was deprecated in v2.0.
346+
Please use map-id instead."
347+
#-}
348+
349+
map-map-fusion = map-∘
350+
{-# WARNING_ON_USAGE map-map-fusion
351+
"Warning: map-map-fusion was deprecated in v2.0.
352+
Please use map-∘ instead."
353+
#-}

‎src/Codata/Sized/Covec/Properties.agda

+26-6
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,32 @@ open import Relation.Binary.PropositionalEquality as Eq
2020

2121
module _ {a} {A : Set a} where
2222

23-
map-identity : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as
24-
map-identity [] = []
25-
map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)
23+
map-id : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as
24+
map-id [] = []
25+
map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force)
2626

2727
module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
2828

29-
map-map-fusion : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as
30-
map-map-fusion f g [] = []
31-
map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)
29+
map-∘ : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as
30+
map-∘ f g [] = []
31+
map-∘ f g (a ∷ as) = Eq.refl ∷ λ where .force → map-∘ f g (as .force)
32+
33+
------------------------------------------------------------------------
34+
-- DEPRECATED
35+
------------------------------------------------------------------------
36+
-- Please use the new names as continuing support for the old names is
37+
-- not guaranteed.
38+
39+
-- Version 2.0
40+
41+
map-identity = map-id
42+
{-# WARNING_ON_USAGE map-identity
43+
"Warning: map-identity was deprecated in v2.0.
44+
Please use map-id instead."
45+
#-}
46+
47+
map-map-fusion = map-∘
48+
{-# WARNING_ON_USAGE map-map-fusion
49+
"Warning: map-map-fusion was deprecated in v2.0.
50+
Please use map-∘ instead."
51+
#-}

‎src/Codata/Sized/Delay/Properties.agda

+37-7
Original file line numberDiff line numberDiff line change
@@ -39,16 +39,20 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
3939
length-zipWith f (later da) (later db) =
4040
suc λ where .force → length-zipWith f (da .force) (db .force)
4141

42-
map-map-fusion : ∀ (f : A → B) (g : B → C) da {i} →
42+
map-id : ∀ da {i} → i ⊢ map (id {A = A}) da ≈ da
43+
map-id (now a) = now Eq.refl
44+
map-id (later da) = later λ where .force → map-id (da .force)
45+
46+
map-∘ : ∀ (f : A → B) (g : B → C) da {i} →
4347
i ⊢ map g (map f da) ≈ map (g ∘′ f) da
44-
map-map-fusion f g (now a) = now Eq.refl
45-
map-map-fusion f g (later da) = later λ where .force → map-map-fusion f g (da .force)
48+
map-∘ f g (now a) = now Eq.refl
49+
map-∘ f g (later da) = later λ where .force → map-∘ f g (da .force)
4650

47-
map-unfold-fusion : ∀ (f : B → C) n (s : A) {i} →
51+
map-unfold : ∀ (f : B → C) n (s : A) {i} →
4852
i ⊢ map f (unfold n s) ≈ unfold (Sum.map id f ∘′ n) s
49-
map-unfold-fusion f n s with n s
50-
... | Sum.inj₁ s′ = later λ where .force → map-unfold-fusion f n s′
51-
... | Sum.inj₂ b = now Eq.refl
53+
map-unfold f n s with n s
54+
... | Sum.inj₁ s′ = later λ where .force → map-unfold f n s′
55+
... | Sum.inj₂ b = now Eq.refl
5256

5357

5458
------------------------------------------------------------------------
@@ -105,3 +109,29 @@ module _ {a} {A B : Set a} where
105109
Eq.cong (toℕ ∘′ length-⇓) (⇓-unique bind⇓ f⇓)
106110
bind⇓-length {d = d@(later dt)} {f = f} bind⇓@(later bind'⇓) d⇓@(later r) f⇓ =
107111
Eq.cong ℕ.suc (bind⇓-length bind'⇓ r f⇓)
112+
113+
------------------------------------------------------------------------
114+
-- DEPRECATED
115+
------------------------------------------------------------------------
116+
-- Please use the new names as continuing support for the old names is
117+
-- not guaranteed.
118+
119+
-- Version 2.0
120+
121+
map-identity = map-id
122+
{-# WARNING_ON_USAGE map-identity
123+
"Warning: map-identity was deprecated in v2.0.
124+
Please use map-id instead."
125+
#-}
126+
127+
map-map-fusion = map-∘
128+
{-# WARNING_ON_USAGE map-map-fusion
129+
"Warning: map-map-fusion was deprecated in v2.0.
130+
Please use map-∘ instead."
131+
#-}
132+
133+
map-unfold-fusion = map-unfold
134+
{-# WARNING_ON_USAGE map-unfold-fusion
135+
"Warning: map-unfold-fusion was deprecated in v2.0.
136+
Please use map-unfold instead."
137+
#-}

0 commit comments

Comments
 (0)