diff --git a/CHANGELOG.md b/CHANGELOG.md index e443a391b4..9de211b5d5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -685,6 +685,42 @@ Deprecated modules Deprecated names ---------------- +* In `Codata.Guarded.Stream.Properties`: + ```agda + map-identity ↦ map-id + map-fusion ↦ map-∘ + ``` + +* In `Codata.Sized.Colist.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + ``` + +* In `Codata.Sized.Covec.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + ``` + +* In `Codata.Sized.Delay.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + map-unfold-fusion ↦ map-unfold + ``` + +* In `Codata.Sized.M.Properties`: + ```agda + map-compose ↦ map-∘ + ``` + +* In `Codata.Sized.Stream.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + ``` + * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the @@ -768,10 +804,52 @@ Deprecated names * In `Data.List.Properties`: ```agda + map-id₂ ↦ map-id-local + map-cong₂ ↦ map-cong-local + map-compose ↦ map-∘ + + map-++-commute ↦ map-++ + sum-++-commute ↦ sum-++ + reverse-map-commute ↦ reverse-map + reverse-++-commute ↦ reverse-++ + zipWith-identityˡ ↦ zipWith-zeroˡ zipWith-identityʳ ↦ zipWith-zeroʳ ``` +* In `Data.List.NonEmpty.Properties`: + ```agda + map-compose ↦ map-∘ + + map-++⁺-commute ↦ map-++⁺ + ``` + +* In `Data.List.Relation.Unary.All.Properties`: + ```agda + updateAt-id-relative ↦ updateAt-id-local + updateAt-compose-relative ↦ updateAt-∘-local + updateAt-compose ↦ updateAt-∘ + updateAt-cong-relative ↦ updateAt-cong-local + ``` + +* In `Data.List.Zipper.Properties`: + ```agda + toList-reverse-commute ↦ toList-reverse + toList-ˡ++-commute ↦ toList-ˡ++ + toList-++ʳ-commute ↦ toList-++ʳ + toList-map-commute ↦ toList-map + toList-foldr-commute ↦ toList-foldr + ``` + +* In `Data.Maybe.Properties`: + ```agda + map-id₂ ↦ map-id-local + map-cong₂ ↦ map-cong-local + + map-compose ↦ map-∘ + + map-<∣>-commute ↦ map-<∣> + * In `Data.List.Relation.Binary.Subset.Propositional.Properties`: ``` map-with-∈⁺ ↦ mapWith∈⁺ @@ -819,8 +897,38 @@ Deprecated names negative>= : ∀ (f : A → List⁺ B) (xs : List⁺ A) → (toList xs ⋆>>= toList ∘ f) ≡ toList (xs >>= f) toList->>= f (x ∷ xs) = begin List.concat (List.map (toList ∘ f) (x ∷ xs)) - ≡⟨ cong List.concat $ List.map-compose {g = toList} (x ∷ xs) ⟩ + ≡⟨ cong List.concat $ List.map-∘ {g = toList} (x ∷ xs) ⟩ List.concat (List.map toList (List.map f (x ∷ xs))) ∎ @@ -96,10 +96,10 @@ drop-+-++⁺ : ∀ (xs : List A) ys → drop+ (List.length xs) (xs ++⁺ ys) ≡ drop-+-++⁺ [] ys = refl drop-+-++⁺ (x ∷ xs) ys = drop-+-++⁺ xs ys -map-++⁺-commute : ∀ (f : A → B) xs ys → +map-++⁺ : ∀ (f : A → B) xs ys → map f (xs ++⁺ ys) ≡ List.map f xs ++⁺ map f ys -map-++⁺-commute f [] ys = refl -map-++⁺-commute f (x ∷ xs) ys = cong (λ zs → f x ∷ toList zs) (map-++⁺-commute f xs ys) +map-++⁺ f [] ys = refl +map-++⁺ f (x ∷ xs) ys = cong (λ zs → f x ∷ toList zs) (map-++⁺ f xs ys) ------------------------------------------------------------------------ -- map @@ -110,8 +110,8 @@ length-map f (_ ∷ xs) = cong suc (List.length-map f xs) map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs) -map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose (x ∷ xs) = cong (_ ∷_) (List.map-compose xs) +map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f +map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs) ------------------------------------------------------------------------ -- groupSeqs @@ -142,3 +142,22 @@ module _ {P : Pred A p} (P? : Decidable P) where ... | false | inj₁ _ ∷ _ | hyp = cong (x ∷_) hyp ... | false | inj₂ _ ∷ _ | hyp = cong (x ∷_) hyp +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + +map-++⁺-commute = map-++⁺ +{-# WARNING_ON_USAGE map-++⁺-commute +"Warning: map-++⁺-commute was deprecated in v2.0. +Please use map-++⁺ instead." +#-} diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 898f29f85f..17f4159c86 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -83,31 +83,31 @@ map-id : map id ≗ id {A = List A} map-id [] = refl map-id (x ∷ xs) = cong (x ∷_) (map-id xs) -map-id₂ : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs -map-id₂ [] = refl -map-id₂ (fx≡x ∷ pxs) = cong₂ _∷_ fx≡x (map-id₂ pxs) +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-++-commute : ∀ (f : A → B) xs ys → +map-++ : ∀ (f : A → B) xs ys → map f (xs ++ ys) ≡ map f xs ++ map f ys -map-++-commute f [] ys = refl -map-++-commute f (x ∷ xs) ys = cong (f x ∷_) (map-++-commute f xs 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₂ : ∀ {f g : A → B} {xs} → +map-cong-local : ∀ {f g : A → B} {xs} → All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs -map-cong₂ [] = refl -map-cong₂ (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong₂ fxs≡gxs) +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-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose [] = refl -map-compose (x ∷ xs) = cong (_ ∷_) (map-compose 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 @@ -260,16 +260,16 @@ module _ {f g : These A B → C} where alignWith-map : (g : D → A) (h : E → B) → ∀ xs ys → alignWith f (map g xs) (map h ys) ≡ alignWith (f ∘′ These.map g h) xs ys - alignWith-map g h [] ys = sym (map-compose ys) - alignWith-map g h xs@(_ ∷ _) [] = sym (map-compose xs) + alignWith-map g h [] ys = sym (map-∘ ys) + alignWith-map g h xs@(_ ∷ _) [] = sym (map-∘ xs) alignWith-map g h (x ∷ xs) (y ∷ ys) = cong₂ _∷_ refl (alignWith-map g h xs ys) map-alignWith : ∀ (g : C → D) → ∀ xs ys → map g (alignWith f xs ys) ≡ alignWith (g ∘′ f) xs ys - map-alignWith g [] ys = sym (map-compose ys) - map-alignWith g xs@(_ ∷ _) [] = sym (map-compose xs) + map-alignWith g [] ys = sym (map-∘ ys) + map-alignWith g xs@(_ ∷ _) [] = sym (map-∘ xs) map-alignWith g (x ∷ xs) (y ∷ ys) = cong₂ _∷_ refl (map-alignWith g xs ys) @@ -496,7 +496,7 @@ concat-map : ∀ {f : A → B} → concat ∘ map (map f) ≗ map f ∘ concat concat-map {f = f} xss = begin concat (map (map f) xss) ≡⟨ cong concat (map-is-foldr xss) ⟩ concat (foldr (λ xs → map f xs ∷_) [] xss) ≡⟨ foldr-fusion concat [] (λ _ _ → refl) xss ⟩ - foldr (λ ys → map f ys ++_) [] xss ≡⟨ sym (foldr-fusion (map f) [] (map-++-commute f) xss) ⟩ + foldr (λ ys → map f ys ++_) [] xss ≡⟨ sym (foldr-fusion (map f) [] (map-++ f) xss) ⟩ map f (concat xss) ∎ concat-++ : (xss yss : List (List A)) → concat xss ++ concat yss ≡ concat (xss ++ yss) @@ -518,10 +518,10 @@ concat-[-] (x ∷ xs) = cong (x ∷_) (concat-[-] xs) ------------------------------------------------------------------------ -- sum -sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys -sum-++-commute [] ys = refl -sum-++-commute (x ∷ xs) ys = begin - x + sum (xs ++ ys) ≡⟨ cong (x +_) (sum-++-commute xs ys) ⟩ +sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys +sum-++ [] ys = refl +sum-++ (x ∷ xs) ys = begin + x + sum (xs ++ ys) ≡⟨ cong (x +_) (sum-++ xs ys) ⟩ x + (sum xs + sum ys) ≡⟨ sym (+-assoc x _ _) ⟩ (x + sum xs) + sum ys ∎ @@ -564,7 +564,7 @@ scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin map (foldl f (f e x)) (inits xs) ≡⟨ refl ⟩ map (foldl f e ∘ (x ∷_)) (inits xs) - ≡⟨ map-compose (inits xs) ⟩ + ≡⟨ map-∘ (inits xs) ⟩ map (foldl f e) (map (x ∷_) (inits xs)) ∎) @@ -927,9 +927,9 @@ unfold-reverse x xs = ʳ++-defn xs -- reverse is an involution with respect to append. -reverse-++-commute : (xs ys : List A) → +reverse-++ : (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs -reverse-++-commute xs ys = begin +reverse-++ xs ys = begin reverse (xs ++ ys) ≡⟨⟩ (xs ++ ys) ʳ++ [] ≡⟨ ʳ++-++ xs ⟩ ys ʳ++ xs ʳ++ [] ≡⟨⟩ @@ -960,8 +960,8 @@ length-reverse xs = begin length xs + 0 ≡⟨ +-identityʳ _ ⟩ length xs ∎ -reverse-map-commute : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f -reverse-map-commute f xs = begin +reverse-map : (f : A → B) → map f ∘ reverse ≗ reverse ∘ map f +reverse-map f xs = begin map f (reverse xs) ≡⟨⟩ map f (xs ʳ++ []) ≡⟨ map-ʳ++ f xs ⟩ map f xs ʳ++ [] ≡⟨⟩ @@ -1004,6 +1004,48 @@ module _ {x y : A} where -- Version 2.0 +map-id₂ = map-id-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-id₂ was deprecated in v2.0. +Please use map-id-local instead." +#-} + +map-cong₂ = map-cong-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-cong₂ was deprecated in v2.0. +Please use map-cong-local instead." +#-} + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + +map-++-commute = map-++ +{-# WARNING_ON_USAGE map-++-commute +"Warning: map-++-commute was deprecated in v2.0. +Please use map-++ instead." +#-} + +sum-++-commute = sum-++ +{-# WARNING_ON_USAGE sum-++-commute +"Warning: map-++-commute was deprecated in v2.0. +Please use map-++ instead." +#-} + +reverse-map-commute = reverse-map +{-# WARNING_ON_USAGE reverse-map-commute +"Warning: reverse-map-commute was deprecated in v2.0. +Please use reverse-map instead." +#-} + +reverse-++-commute = reverse-++ +{-# WARNING_ON_USAGE reverse-++-commute +"Warning: reverse-++-commute was deprecated in v2.0. +Please use reverse-++ instead." +#-} + zipWith-identityˡ = zipWith-zeroˡ {-# WARNING_ON_USAGE zipWith-identityˡ "Warning: zipWith-identityˡ was deprecated in v2.0. diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index 8438609c61..36aa5259f6 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -42,7 +42,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where fromPrefix {as} {bs} p with Prefix.toView p ... | Prefix._++_ {cs} rs ds = subst (Suffix R (reverse as)) - (sym (Listₚ.reverse-++-commute cs ds)) + (sym (Listₚ.reverse-++ cs ds)) (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs)) fromPrefix-rev : ∀ {as bs} → Prefix R (reverse as) (reverse bs) → @@ -58,7 +58,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toPrefix-rev {as} {bs} s with Suffix.toView s ... | Suffix._++_ cs {ds} rs = subst (Prefix R (reverse as)) - (sym (Listₚ.reverse-++-commute cs ds)) + (sym (Listₚ.reverse-++ cs ds)) (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs)) toPrefix : ∀ {as bs} → Suffix R (reverse as) (reverse bs) → diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 9a94e100f3..5b9cdb8871 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -247,59 +247,57 @@ lookup∘updateAt′ i j pxs i≢j = -- the defining properties. -- In the explanations, we make use of shorthand f = g ↾ x --- meaning that f and g agree at point x, i.e. f x ≡ g x. +-- meaning that f and g agree locally at point x, i.e. f x ≡ g x. -- updateAt (i : x ∈ xs) is a morphism -- from the monoid of endofunctions P x → P x -- to the monoid of endofunctions All P xs → All P xs. --- 1a. relative identity: f = id ↾ (lookup pxs i) --- implies updateAt i f = id ↾ pxs +-- 1a. local identity: f = id ↾ (lookup pxs i) +-- implies updateAt i f = id ↾ pxs -updateAt-id-relative : ∀ (i : x ∈ xs) {f : P x → P x} (pxs : All P xs) → - f (lookup pxs i) ≡ lookup pxs i → - updateAt i f pxs ≡ pxs -updateAt-id-relative (here refl)(px ∷ pxs) eq = cong (_∷ pxs) eq -updateAt-id-relative (there i) (px ∷ pxs) eq = cong (px ∷_) (updateAt-id-relative i pxs eq) +updateAt-id-local : ∀ (i : x ∈ xs) {f : P x → P x} (pxs : All P xs) → + f (lookup pxs i) ≡ lookup pxs i → + updateAt i f pxs ≡ pxs +updateAt-id-local (here refl)(px ∷ pxs) eq = cong (_∷ pxs) eq +updateAt-id-local (there i) (px ∷ pxs) eq = cong (px ∷_) (updateAt-id-local i pxs eq) -- 1b. identity: updateAt i id ≗ id updateAt-id : ∀ (i : x ∈ xs) (pxs : All P xs) → updateAt i id pxs ≡ pxs -updateAt-id i pxs = updateAt-id-relative i pxs refl +updateAt-id i pxs = updateAt-id-local i pxs refl -- 2a. relative composition: f ∘ g = h ↾ (lookup i pxs) -- implies updateAt i f ∘ updateAt i g = updateAt i h ↾ pxs -updateAt-compose-relative : ∀ (i : x ∈ xs) {f g h : P x → P x} (pxs : All P xs) → - f (g (lookup pxs i)) ≡ h (lookup pxs i) → - updateAt i f (updateAt i g pxs) ≡ updateAt i h pxs -updateAt-compose-relative (here refl) (px ∷ pxs) fg=h = cong (_∷ pxs) fg=h -updateAt-compose-relative (there i) (px ∷ pxs) fg=h = - cong (px ∷_) (updateAt-compose-relative i pxs fg=h) +updateAt-∘-local : ∀ (i : x ∈ xs) {f g h : P x → P x} (pxs : All P xs) → + f (g (lookup pxs i)) ≡ h (lookup pxs i) → + updateAt i f (updateAt i g pxs) ≡ updateAt i h pxs +updateAt-∘-local (here refl) (px ∷ pxs) fg=h = cong (_∷ pxs) fg=h +updateAt-∘-local (there i) (px ∷ pxs) fg=h = cong (px ∷_) (updateAt-∘-local i pxs fg=h) -- 2b. composition: updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) -updateAt-compose : ∀ (i : x ∈ xs) {f g : P x → P x} → - updateAt {P = P} i f ∘ updateAt i g ≗ updateAt i (f ∘ g) -updateAt-compose (here refl) (px ∷ pxs) = refl -updateAt-compose (there i) (px ∷ pxs) = cong (px ∷_) (updateAt-compose i pxs) +updateAt-∘ : ∀ (i : x ∈ xs) {f g : P x → P x} → + updateAt {P = P} i f ∘ updateAt i g ≗ updateAt i (f ∘ g) +updateAt-∘ i pxs = updateAt-∘-local i pxs refl -- 3. congruence: updateAt i is a congruence wrt. extensional equality. -- 3a. If f = g ↾ (lookup pxs i) -- then updateAt i f = updateAt i g ↾ pxs -updateAt-cong-relative : ∀ (i : x ∈ xs) {f g : P x → P x} (pxs : All P xs) → - f (lookup pxs i) ≡ g (lookup pxs i) → - updateAt i f pxs ≡ updateAt i g pxs -updateAt-cong-relative (here refl) (px ∷ pxs) f=g = cong (_∷ pxs) f=g -updateAt-cong-relative (there i) (px ∷ pxs) f=g = cong (px ∷_) (updateAt-cong-relative i pxs f=g) +updateAt-cong-local : ∀ (i : x ∈ xs) {f g : P x → P x} (pxs : All P xs) → + f (lookup pxs i) ≡ g (lookup pxs i) → + updateAt i f pxs ≡ updateAt i g pxs +updateAt-cong-local (here refl) (px ∷ pxs) f=g = cong (_∷ pxs) f=g +updateAt-cong-local (there i) (px ∷ pxs) f=g = cong (px ∷_) (updateAt-cong-local i pxs f=g) -- 3b. congruence: f ≗ g → updateAt i f ≗ updateAt i g updateAt-cong : ∀ (i : x ∈ xs) {f g : P x → P x} → f ≗ g → updateAt {P = P} i f ≗ updateAt i g -updateAt-cong i f≗g pxs = updateAt-cong-relative i pxs (f≗g (lookup pxs i)) +updateAt-cong i f≗g pxs = updateAt-cong-local i pxs (f≗g (lookup pxs i)) -- The order of updates at different indices i ≢ j does not matter. @@ -749,3 +747,29 @@ Any¬→¬All = Any¬⇒¬All "Warning: Any¬→¬All was deprecated in v1.3. Please use Any¬⇒¬All instead." #-} + +-- Version 2.0 + +updateAt-id-relative = updateAt-id-local +{-# WARNING_ON_USAGE updateAt-id-relative +"Warning: updateAt-id-relative was deprecated in v2.0. +Please use updateAt-id-local instead." +#-} + +updateAt-compose-relative = updateAt-∘-local +{-# WARNING_ON_USAGE updateAt-compose-relative +"Warning: updateAt-compose-relative was deprecated in v2.0. +Please use updateAt-∘-local instead." +#-} + +updateAt-compose = updateAt-∘ +{-# WARNING_ON_USAGE updateAt-compose +"Warning: updateAt-compose was deprecated in v2.0. +Please use updateAt-∘ instead." +#-} + +updateAt-cong-relative = updateAt-cong-local +{-# WARNING_ON_USAGE updateAt-cong-relative +"Warning: updateAt-cong-relative was deprecated in v2.0. +Please use updateAt-cong-local instead." +#-} diff --git a/src/Data/List/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda index 7da32c5b89..30ea57a9c2 100644 --- a/src/Data/List/Zipper/Properties.agda +++ b/src/Data/List/Zipper/Properties.agda @@ -46,12 +46,12 @@ module _ {a} {A : Set a} where -- Applying reverse does correspond to reversing the represented list - toList-reverse-commute : (zp : Zipper A) → toList (reverse zp) ≡ List.reverse (toList zp) - toList-reverse-commute (mkZipper ctx val) = begin + toList-reverse : (zp : Zipper A) → toList (reverse zp) ≡ List.reverse (toList zp) + toList-reverse (mkZipper ctx val) = begin List.reverse val List.++ ctx ≡⟨ cong (List.reverse val List.++_) (sym (reverse-involutive ctx)) ⟩ List.reverse val List.++ List.reverse (List.reverse ctx) - ≡⟨ sym (reverse-++-commute (List.reverse ctx) val) ⟩ + ≡⟨ sym (reverse-++ (List.reverse ctx) val) ⟩ List.reverse (List.reverse ctx List.++ val) ∎ @@ -61,10 +61,10 @@ module _ {a} {A : Set a} where -- _ˡ++_ properties - toList-ˡ++-commute : ∀ xs (zp : Zipper A) → toList (xs ˡ++ zp) ≡ xs List.++ toList zp - toList-ˡ++-commute xs (mkZipper ctx val) = begin + toList-ˡ++ : ∀ xs (zp : Zipper A) → toList (xs ˡ++ zp) ≡ xs List.++ toList zp + toList-ˡ++ xs (mkZipper ctx val) = begin List.reverse (ctx List.++ List.reverse xs) List.++ val - ≡⟨ cong (List._++ _) (reverse-++-commute ctx (List.reverse xs)) ⟩ + ≡⟨ cong (List._++ _) (reverse-++ ctx (List.reverse xs)) ⟩ (List.reverse (List.reverse xs) List.++ List.reverse ctx) List.++ val ≡⟨ ++-assoc (List.reverse (List.reverse xs)) (List.reverse ctx) val ⟩ List.reverse (List.reverse xs) List.++ List.reverse ctx List.++ val @@ -77,7 +77,7 @@ module _ {a} {A : Set a} where (ctx List.++ List.reverse ys) List.++ List.reverse xs ≡⟨ ++-assoc ctx _ _ ⟩ ctx List.++ List.reverse ys List.++ List.reverse xs - ≡⟨ cong (ctx List.++_) (sym (reverse-++-commute xs ys)) ⟩ + ≡⟨ cong (ctx List.++_) (sym (reverse-++ xs ys)) ⟩ ctx List.++ List.reverse (xs List.++ ys) ∎ @@ -88,7 +88,7 @@ module _ {a} {A : Set a} where List.reverse xs List.++ List.reverse ys List.++ ctx ≡⟨ sym (++-assoc (List.reverse xs) (List.reverse ys) ctx) ⟩ (List.reverse xs List.++ List.reverse ys) List.++ ctx - ≡⟨ cong (List._++ ctx) (sym (reverse-++-commute ys xs)) ⟩ + ≡⟨ cong (List._++ ctx) (sym (reverse-++ ys xs)) ⟩ List.reverse (ys List.++ xs) List.++ ctx ∎ @@ -99,8 +99,8 @@ module _ {a} {A : Set a} where -- _++ʳ_ properties - toList-++ʳ-commute : ∀ (zp : Zipper A) xs → toList (zp ++ʳ xs) ≡ toList zp List.++ xs - toList-++ʳ-commute (mkZipper ctx val) xs = begin + toList-++ʳ : ∀ (zp : Zipper A) xs → toList (zp ++ʳ xs) ≡ toList zp List.++ xs + toList-++ʳ (mkZipper ctx val) xs = begin List.reverse ctx List.++ val List.++ xs ≡⟨ sym (++-assoc (List.reverse ctx) val xs) ⟩ (List.reverse ctx List.++ val) List.++ xs @@ -115,20 +115,58 @@ module _ {a} {A : Set a} where module _ {a b} {A : Set a} {B : Set b} where - toList-map-commute : ∀ (f : A → B) zp → toList (map f zp) ≡ List.map f (toList zp) - toList-map-commute f zp@(mkZipper ctx val) = begin + toList-map : ∀ (f : A → B) zp → toList (map f zp) ≡ List.map f (toList zp) + toList-map f zp@(mkZipper ctx val) = begin List.reverse (List.map f ctx) List.++ List.map f val - ≡⟨ cong (List._++ _) (sym (reverse-map-commute f ctx)) ⟩ + ≡⟨ cong (List._++ _) (sym (reverse-map f ctx)) ⟩ List.map f (List.reverse ctx) List.++ List.map f val - ≡⟨ sym (map-++-commute f (List.reverse ctx) val) ⟩ + ≡⟨ sym (map-++ f (List.reverse ctx) val) ⟩ List.map f (List.reverse ctx List.++ val) ∎ - toList-foldr-commute : ∀ (c : A → B → B) n zp → foldr c n zp ≡ List.foldr c n (toList zp) - toList-foldr-commute c n (mkZipper ctx val) = begin + toList-foldr : ∀ (c : A → B → B) n zp → foldr c n zp ≡ List.foldr c n (toList zp) + toList-foldr c n (mkZipper ctx val) = begin List.foldl (flip c) (List.foldr c n val) ctx ≡⟨ sym (reverse-foldr c (List.foldr c n val) ctx) ⟩ List.foldr c (List.foldr c n val) (List.reverse ctx) ≡⟨ sym (foldr-++ c n (List.reverse ctx) val) ⟩ List.foldr c n (List.reverse ctx List.++ val) ∎ + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +toList-reverse-commute = toList-reverse +{-# WARNING_ON_USAGE toList-reverse-commute +"Warning: toList-reverse-commute was deprecated in v2.0. +Please use toList-reverse instead." +#-} + +toList-ˡ++-commute = toList-ˡ++ +{-# WARNING_ON_USAGE toList-ˡ++-commute +"Warning: toList-ˡ++-commute was deprecated in v2.0. +Please use toList-ˡ++ instead." +#-} + +toList-++ʳ-commute = toList-++ʳ +{-# WARNING_ON_USAGE toList-++ʳ-commute +"Warning: toList-++ʳ-commute was deprecated in v2.0. +Please use toList-++ʳ instead." +#-} + +toList-map-commute = toList-map +{-# WARNING_ON_USAGE toList-map-commute +"Warning: toList-map-commute was deprecated in v2.0. +Please use toList-map instead." +#-} + +toList-foldr-commute = toList-foldr +{-# WARNING_ON_USAGE toList-foldr-commute +"Warning: toList-foldr-commute was deprecated in v2.0. +Please use toList-foldr instead." +#-} diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda index 018e364899..2ade049d6e 100644 --- a/src/Data/Maybe/Properties.agda +++ b/src/Data/Maybe/Properties.agda @@ -47,31 +47,31 @@ map-id : map id ≗ id {A = Maybe A} map-id (just x) = refl map-id nothing = refl -map-id₂ : ∀ {f : A → A} {mx} → All (λ x → f x ≡ x) mx → map f mx ≡ mx -map-id₂ (just eq) = cong just eq -map-id₂ nothing = refl +map-id-local : ∀ {f : A → A} {mx} → All (λ x → f x ≡ x) mx → map f mx ≡ mx +map-id-local (just eq) = cong just eq +map-id-local nothing = refl -map-<∣>-commute : ∀ (f : A → B) mx my → +map-<∣> : ∀ (f : A → B) mx my → map f (mx <∣> my) ≡ map f mx <∣> map f my -map-<∣>-commute f (just x) my = refl -map-<∣>-commute f nothing my = refl +map-<∣> f (just x) my = refl +map-<∣> f nothing my = refl map-cong : {f g : A → B} → f ≗ g → map f ≗ map g map-cong f≗g (just x) = cong just (f≗g x) map-cong f≗g nothing = refl -map-cong₂ : ∀ {f g : A → B} {mx} → +map-cong-local : ∀ {f g : A → B} {mx} → All (λ x → f x ≡ g x) mx → map f mx ≡ map g mx -map-cong₂ (just eq) = cong just eq -map-cong₂ nothing = refl +map-cong-local (just eq) = cong just eq +map-cong-local nothing = refl map-injective : ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f) map-injective f-inj {nothing} {nothing} p = refl map-injective f-inj {just x} {just y} p = cong just (f-inj (just-injective p)) -map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f -map-compose (just x) = refl -map-compose nothing = refl +map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f +map-∘ (just x) = refl +map-∘ nothing = refl map-nothing : ∀ {f : A → B} {ma} → ma ≡ nothing → map f ma ≡ nothing map-nothing refl = refl @@ -149,3 +149,35 @@ module _ (A : Set a) where <∣>-monoid = record { isMonoid = <∣>-isMonoid } + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-id₂ = map-id-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-id₂ was deprecated in v2.0. +Please use map-id-local instead." +#-} + +map-cong₂ = map-cong-local +{-# WARNING_ON_USAGE map-id₂ +"Warning: map-cong₂ was deprecated in v2.0. +Please use map-cong-local instead." +#-} + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} + +map-<∣>-commute = map-<∣> +{-# WARNING_ON_USAGE map-<∣>-commute +"Warning: map-<∣>-commute was deprecated in v2.0. +Please use map-<∣> instead." +#-} diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda index c881601af9..7042b8682f 100644 --- a/src/Data/Sum/Properties.agda +++ b/src/Data/Sum/Properties.agda @@ -53,28 +53,28 @@ map-id : map {A = A} {B = B} id id ≗ id map-id (inj₁ _) = refl map-id (inj₂ _) = refl -[,]-∘-distr : (f : A → B) +[,]-∘ : (f : A → B) {g : C → A} {h : D → A} → f ∘ [ g , h ] ≗ [ f ∘ g , f ∘ h ] -[,]-∘-distr _ (inj₁ _) = refl -[,]-∘-distr _ (inj₂ _) = refl +[,]-∘ _ (inj₁ _) = refl +[,]-∘ _ (inj₂ _) = refl -[,]-map-commute : {f : A → B} {g : C → D} - {f′ : B → E} {g′ : D → E} → - [ f′ , g′ ] ∘ map f g ≗ [ f′ ∘ f , g′ ∘ g ] -[,]-map-commute (inj₁ _) = refl -[,]-map-commute (inj₂ _) = refl +[,]-map : {f : A → B} {g : C → D} + {f′ : B → E} {g′ : D → E} → + [ f′ , g′ ] ∘ map f g ≗ [ f′ ∘ f , g′ ∘ g ] +[,]-map (inj₁ _) = refl +[,]-map (inj₂ _) = refl -map-commute : {f : A → B} {g : C → D} +map-map : {f : A → B} {g : C → D} {f′ : B → E} {g′ : D → F} → map f′ g′ ∘ map f g ≗ map (f′ ∘ f) (g′ ∘ g) -map-commute (inj₁ _) = refl -map-commute (inj₂ _) = refl +map-map (inj₁ _) = refl +map-map (inj₂ _) = refl -map₁₂-commute : {f : A → B} {g : C → D} → +map₁₂-map₂₁ : {f : A → B} {g : C → D} → map₁ f ∘ map₂ g ≗ map₂ g ∘ map₁ f -map₁₂-commute (inj₁ _) = refl -map₁₂-commute (inj₂ _) = refl +map₁₂-map₂₁ (inj₁ _) = refl +map₁₂-map₂₁ (inj₂ _) = refl map-assocˡ : (f : A → C) (g : B → D) (h : C → F) → map (map f g) h ∘ assocˡ ≗ assocˡ ∘ map f (map g h) @@ -118,3 +118,35 @@ map₂-cong : {g g′ : C → D} → g ≗ g′ → map₂ {A = A} g ≗ map₂ g′ map₂-cong g≗g′ = [,-]-cong ((cong inj₂) ∘ g≗g′) + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +[,]-∘-distr = [,]-∘ +{-# WARNING_ON_USAGE [,]-∘-distr +"Warning: [,]-∘-distr was deprecated in v2.0. +Please use [,]-∘ instead." +#-} + +[,]-map-commute = [,]-map +{-# WARNING_ON_USAGE [,]-map-commute +"Warning: [,]-map-commute was deprecated in v2.0. +Please use [,]-map instead." +#-} + +map-commute = map-map +{-# WARNING_ON_USAGE map-commute +"Warning: map-commute was deprecated in v2.0. +Please use map-map instead." +#-} + +map₁₂-commute = map₁₂-map₂₁ +{-# WARNING_ON_USAGE map₁₂-commute +"Warning: map₁₂-commute was deprecated in v2.0. +Please use map₁₂-map₂₁ instead." +#-} diff --git a/src/Data/Tree/Binary/Zipper/Properties.agda b/src/Data/Tree/Binary/Zipper/Properties.agda index 0b2e1ef01f..7a5707b2e8 100644 --- a/src/Data/Tree/Binary/Zipper/Properties.agda +++ b/src/Data/Tree/Binary/Zipper/Properties.agda @@ -49,8 +49,8 @@ toTree-right-identity (mkZipper ctx (node l m r)) = just refl ------------------------------------------------------------------------ -- Tree-like operations indeed correspond to their counterparts -toTree-#nodes-commute : ∀ (zp : Zipper N L) → #nodes zp ≡ BT.#nodes (toTree zp) -toTree-#nodes-commute (mkZipper c v) = helper c v +toTree-#nodes : ∀ (zp : Zipper N L) → #nodes zp ≡ BT.#nodes (toTree zp) +toTree-#nodes (mkZipper c v) = helper c v where helper : (cs : List (Crumb N L)) → (t : Tree N L) → @@ -75,8 +75,8 @@ toTree-#nodes-commute (mkZipper c v) = helper c v #nodes (mkZipper ctx (node foc m r)) ≡⟨ helper ctx (node foc m r) ⟩ BT.#nodes (toTree (mkZipper cs foc)) ∎ -toTree-#leaves-commute : ∀ (zp : Zipper N L) → #leaves zp ≡ BT.#leaves (toTree zp) -toTree-#leaves-commute (mkZipper c v) = helper c v +toTree-#leaves : ∀ (zp : Zipper N L) → #leaves zp ≡ BT.#leaves (toTree zp) +toTree-#leaves (mkZipper c v) = helper c v where helper : (cs : List (Crumb N L)) → (t : Tree N L) → @@ -98,8 +98,8 @@ toTree-#leaves-commute (mkZipper c v) = helper c v #leaves (mkZipper ctx (node foc m r)) ≡⟨ helper ctx (node foc m r) ⟩ BT.#leaves (toTree (mkZipper cs foc)) ∎ -toTree-map-commute : ∀ (f : N → N₁) (g : L → L₁) zp → toTree (map f g zp) ≡ BT.map f g (toTree zp) -toTree-map-commute {N = N} {L = L} f g (mkZipper c v) = helper c v +toTree-map : ∀ (f : N → N₁) (g : L → L₁) zp → toTree (map f g zp) ≡ BT.map f g (toTree zp) +toTree-map {N = N} {L = L} f g (mkZipper c v) = helper c v where helper : (cs : List (Crumb N L)) → (t : Tree N L) → @@ -108,8 +108,8 @@ toTree-map-commute {N = N} {L = L} f g (mkZipper c v) = helper c v helper (leftBranch m l ∷ ctx) foc = helper ctx (node l m foc) helper (rightBranch m r ∷ ctx) foc = helper ctx (node foc m r) -toTree-foldr-commute : ∀ (f : A → N → A → A) (g : L → A) zp → foldr f g zp ≡ BT.foldr f g (toTree zp) -toTree-foldr-commute {N = N} {L = L} f g (mkZipper c v) = helper c v +toTree-foldr : ∀ (f : A → N → A → A) (g : L → A) zp → foldr f g zp ≡ BT.foldr f g (toTree zp) +toTree-foldr {N = N} {L = L} f g (mkZipper c v) = helper c v where helper : (cs : List (Crumb N L)) → (t : Tree N L) → @@ -123,8 +123,8 @@ toTree-foldr-commute {N = N} {L = L} f g (mkZipper c v) = helper c v -- _⟪_⟫ˡ_ properties -toTree-⟪⟫ˡ-commute : ∀ l m (zp : Zipper N L) → toTree (l ⟪ m ⟫ˡ zp) ≡ node l m (toTree zp) -toTree-⟪⟫ˡ-commute {N = N} {L = L} l m (mkZipper c v) = helper c v +toTree-⟪⟫ˡ : ∀ l m (zp : Zipper N L) → toTree (l ⟪ m ⟫ˡ zp) ≡ node l m (toTree zp) +toTree-⟪⟫ˡ {N = N} {L = L} l m (mkZipper c v) = helper c v where helper : (cs : List (Crumb N L)) → (t : Tree N L) → @@ -135,8 +135,8 @@ toTree-⟪⟫ˡ-commute {N = N} {L = L} l m (mkZipper c v) = helper c v -- _⟪_⟫ʳ_ properties -toTree-⟪⟫ʳ-commute : ∀ (zp : Zipper N L) m r → toTree (zp ⟪ m ⟫ʳ r) ≡ node (toTree zp) m r -toTree-⟪⟫ʳ-commute {N = N} {L = L} (mkZipper c v) m r = helper c v +toTree-⟪⟫ʳ : ∀ (zp : Zipper N L) m r → toTree (zp ⟪ m ⟫ʳ r) ≡ node (toTree zp) m r +toTree-⟪⟫ʳ {N = N} {L = L} (mkZipper c v) m r = helper c v where helper : (cs : List (Crumb N L)) → (t : Tree N L) → @@ -144,3 +144,47 @@ toTree-⟪⟫ʳ-commute {N = N} {L = L} (mkZipper c v) m r = helper c v helper [] foc = refl helper (leftBranch m l ∷ ctx) foc = helper ctx (node l m foc) helper (rightBranch m r ∷ ctx) foc = helper ctx (node foc m r) + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +toTree-#nodes-commute = toTree-#nodes +{-# WARNING_ON_USAGE toTree-#nodes-commute +"Warning: toTree-#nodes-commute was deprecated in v2.0. +Please use toTree-#nodes instead." +#-} + +toTree-#leaves-commute = toTree-#leaves +{-# WARNING_ON_USAGE toTree-#leaves-commute +"Warning: toTree-#leaves-commute was deprecated in v2.0. +Please use toTree-#leaves instead." +#-} + +toTree-map-commute = toTree-map +{-# WARNING_ON_USAGE toTree-map-commute +"Warning: toTree-map-commute was deprecated in v2.0. +Please use toTree-map instead." +#-} + +toTree-foldr-commute = toTree-foldr +{-# WARNING_ON_USAGE toTree-foldr-commute +"Warning: toTree-foldr-commute was deprecated in v2.0. +Please use toTree-foldr instead." +#-} + +toTree-⟪⟫ˡ-commute = toTree-⟪⟫ˡ +{-# WARNING_ON_USAGE toTree-⟪⟫ˡ-commute +"Warning: toTree-⟪⟫ˡ-commute was deprecated in v2.0. +Please use toTree-⟪⟫ˡ instead." +#-} + +toTree-⟪⟫ʳ-commute = toTree-⟪⟫ʳ +{-# WARNING_ON_USAGE toTree-⟪⟫ʳ-commute +"Warning: toTree-⟪⟫ʳ-commute was deprecated in v2.0. +Please use toTree-⟪⟫ʳ instead." +#-} diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index 51d19732dc..a7ab845999 100644 --- a/src/Data/Tree/Rose/Properties.agda +++ b/src/Data/Tree/Rose/Properties.agda @@ -30,16 +30,16 @@ private ------------------------------------------------------------------------ -- map properties -map-compose : (f : A → B) (g : B → C) → +map-∘ : (f : A → B) (g : B → C) → map {i = i} (g ∘′ f) ≗ map {i = i} g ∘′ map {i = i} f -map-compose f g (node a ts) = cong (node (g (f a))) $ begin - List.map (map (g ∘′ f)) ts ≡⟨ Listₚ.map-cong (map-compose f g) ts ⟩ - List.map (map g ∘ map f) ts ≡⟨ Listₚ.map-compose ts ⟩ +map-∘ f g (node a ts) = cong (node (g (f a))) $ begin + List.map (map (g ∘′ f)) ts ≡⟨ Listₚ.map-cong (map-∘ f g) ts ⟩ + List.map (map g ∘ map f) ts ≡⟨ Listₚ.map-∘ ts ⟩ List.map (map g) (List.map (map f) ts) ∎ depth-map : (f : A → B) (t : Rose A i) → depth {i = i} (map {i = i} f t) ≡ depth {i = i} t depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin - List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩ + List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩ List.map (depth ∘′ map f) ts ≡⟨ Listₚ.map-cong (depth-map f) ts ⟩ List.map depth ts ∎ @@ -49,6 +49,20 @@ depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin foldr-map : (f : A → B) (n : B → List C → C) (ts : Rose A i) → foldr {i = i} n (map {i = i} f ts) ≡ foldr {i = i} (n ∘′ f) ts foldr-map f n (node a ts) = cong (n (f a)) $ begin - List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-compose ts ⟩ + List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩ List.map (foldr n ∘′ map f) ts ≡⟨ Listₚ.map-cong (foldr-map f n) ts ⟩ List.map (foldr (n ∘′ f)) ts ∎ + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-compose = map-∘ +{-# WARNING_ON_USAGE map-compose +"Warning: map-compose was deprecated in v2.0. +Please use map-∘ instead." +#-} diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index 65875e1ae3..926627ed17 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -75,44 +75,41 @@ updateAt-minimal (suc i) (suc j) xs i≢j = updateAt-minimal i j (tail xs) (i≢ -- updateAt i is a monoid morphism from A → A to Vector A n → Vector A n. -updateAt-id-relative : ∀ {n} (i : Fin n) {f : A → A} (xs : Vector A n) → - f (xs i) ≡ xs i → - updateAt i f xs ≗ xs -updateAt-id-relative zero xs eq zero = eq -updateAt-id-relative zero xs eq (suc j) = refl -updateAt-id-relative (suc i) xs eq zero = refl -updateAt-id-relative (suc i) xs eq (suc j) = updateAt-id-relative i (tail xs) eq j +updateAt-id-local : ∀ {n} (i : Fin n) {f : A → A} (xs : Vector A n) → + f (xs i) ≡ xs i → + updateAt i f xs ≗ xs +updateAt-id-local zero xs eq zero = eq +updateAt-id-local zero xs eq (suc j) = refl +updateAt-id-local (suc i) xs eq zero = refl +updateAt-id-local (suc i) xs eq (suc j) = updateAt-id-local i (tail xs) eq j updateAt-id : ∀ {n} (i : Fin n) (xs : Vector A n) → updateAt i id xs ≗ xs -updateAt-id i xs = updateAt-id-relative i xs refl - -updateAt-compose-relative : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vector A n) → - f (g (xs i)) ≡ h (xs i) → - updateAt i f (updateAt i g xs) ≗ updateAt i h xs -updateAt-compose-relative zero xs eq zero = eq -updateAt-compose-relative zero xs eq (suc j) = refl -updateAt-compose-relative (suc i) xs eq zero = refl -updateAt-compose-relative (suc i) xs eq (suc j) = updateAt-compose-relative i (tail xs) eq j - -updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) → - updateAt i f (updateAt i g xs) ≗ updateAt i (f ∘ g) xs -updateAt-compose i xs = updateAt-compose-relative i xs refl - -updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) → - f (xs i) ≡ g (xs i) → - updateAt i f xs ≗ updateAt i g xs -updateAt-cong-relative zero xs eq zero = eq -updateAt-cong-relative zero xs eq (suc j) = refl -updateAt-cong-relative (suc i) xs eq zero = refl -updateAt-cong-relative (suc i) xs eq (suc j) = updateAt-cong-relative i (tail xs) eq j +updateAt-id i xs = updateAt-id-local i xs refl + +updateAt-∘-local : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vector A n) → + f (g (xs i)) ≡ h (xs i) → + updateAt i f (updateAt i g xs) ≗ updateAt i h xs +updateAt-∘-local zero xs eq zero = eq +updateAt-∘-local zero xs eq (suc j) = refl +updateAt-∘-local (suc i) xs eq zero = refl +updateAt-∘-local (suc i) xs eq (suc j) = updateAt-∘-local i (tail xs) eq j + +updateAt-∘ : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) → + updateAt i f (updateAt i g xs) ≗ updateAt i (f ∘ g) xs +updateAt-∘ i xs = updateAt-∘-local i xs refl + +updateAt-cong-local : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) → + f (xs i) ≡ g (xs i) → + updateAt i f xs ≗ updateAt i g xs +updateAt-cong-local zero xs eq zero = eq +updateAt-cong-local zero xs eq (suc j) = refl +updateAt-cong-local (suc i) xs eq zero = refl +updateAt-cong-local (suc i) xs eq (suc j) = updateAt-cong-local i (tail xs) eq j updateAt-cong : ∀ {n} (i : Fin n) {f g : A → A} → f ≗ g → (xs : Vector A n) → updateAt i f xs ≗ updateAt i g xs -updateAt-cong zero eq xs zero = eq (xs zero) -updateAt-cong zero eq xs (suc j) = refl -updateAt-cong (suc i) eq xs zero = refl -updateAt-cong (suc i) eq xs (suc j) = updateAt-cong i eq (tail xs) j +updateAt-cong i eq xs = updateAt-cong-local i xs (eq (xs i)) -- The order of updates at different indices i ≢ j does not matter. @@ -143,14 +140,20 @@ lookup-map : ∀ {n} (i : Fin n) (f : A → B) (xs : Vector A n) → map f xs i ≡ f (xs i) lookup-map i f xs = refl -map-updateAt : ∀ {n} {f : A → B} {g : A → A} {h : B → B} +map-updateAt-local : ∀ {n} {f : A → B} {g : A → A} {h : B → B} + (xs : Vector A n) (i : Fin n) → + f (g (xs i)) ≡ h (f (xs i)) → + map f (updateAt i g xs) ≗ updateAt i h (map f xs) +map-updateAt-local {n = suc n} {f = f} xs zero eq zero = eq +map-updateAt-local {n = suc n} {f = f} xs zero eq (suc j) = refl +map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq zero = refl +map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq (suc j) = map-updateAt-local {f = f} (tail xs) i eq j + +map-updateAt : ∀ {n} {f : A → B} {g : A → A} {h : B → B} → + f ∘ g ≗ h ∘ f → (xs : Vector A n) (i : Fin n) → - f (g (xs i)) ≡ h (f (xs i)) → map f (updateAt i g xs) ≗ updateAt i h (map f xs) -map-updateAt {n = suc n} {f = f} xs zero eq zero = eq -map-updateAt {n = suc n} {f = f} xs zero eq (suc j) = refl -map-updateAt {n = suc (suc n)} {f = f} xs (suc i) eq zero = refl -map-updateAt {n = suc (suc n)} {f = f} xs (suc i) eq (suc j) = map-updateAt {f = f} (tail xs) i eq j +map-updateAt {f = f} {g = g} f∘g≗h∘f xs i = map-updateAt-local {f = f} {g = g} xs i (f∘g≗h∘f (xs i)) ------------------------------------------------------------------------ -- _++_ @@ -263,3 +266,35 @@ fromVec∘toVec = Vₚ.lookup∘tabulate toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs toList∘fromList = Lₚ.tabulate-lookup + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +updateAt-id-relative = updateAt-id-local +{-# WARNING_ON_USAGE updateAt-id-relative +"Warning: updateAt-id-relative was deprecated in v2.0. +Please use updateAt-id-local instead." +#-} + +updateAt-compose-relative = updateAt-∘-local +{-# WARNING_ON_USAGE updateAt-compose-relative +"Warning: updateAt-compose-relative was deprecated in v2.0. +Please use updateAt-∘-local instead." +#-} + +updateAt-compose = updateAt-∘ +{-# WARNING_ON_USAGE updateAt-compose +"Warning: updateAt-compose was deprecated in v2.0. +Please use updateAt-∘ instead." +#-} + +updateAt-cong-relative = updateAt-cong-local +{-# WARNING_ON_USAGE updateAt-cong-relative +"Warning: updateAt-cong-relative was deprecated in v2.0. +Please use updateAt-cong-local instead." +#-} diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 3303dd4d79..459880d8cf 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -18,7 +18,7 @@ open import Data.Nat.Properties open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry) open import Data.Sum.Base using ([_,_]′) -open import Data.Sum.Properties using ([,]-map-commute) +open import Data.Sum.Properties using ([,]-map) open import Data.Vec.Base open import Function.Base open import Function.Inverse using (_↔_; inverse) @@ -250,57 +250,56 @@ updateAt-minimal (suc i) (suc j) (x ∷ xs) i≢j (there loc) = -- the defining properties. -- In the explanations, we make use of shorthand f = g ↾ x --- meaning that f and g agree at point x, i.e. f x ≡ g x. +-- meaning that f and g agree locally at point x, i.e. f x ≡ g x. -- updateAt i is a morphism from the monoid of endofunctions A → A -- to the monoid of endofunctions Vec A n → Vec A n --- 1a. relative identity: f = id ↾ (lookup xs i) --- implies updateAt i f = id ↾ xs +-- 1a. local identity: f = id ↾ (lookup xs i) +-- implies updateAt i f = id ↾ xs -updateAt-id-relative : ∀ (i : Fin n) {f : A → A} (xs : Vec A n) → - f (lookup xs i) ≡ lookup xs i → - updateAt i f xs ≡ xs -updateAt-id-relative zero (x ∷ xs) eq = cong (_∷ xs) eq -updateAt-id-relative (suc i) (x ∷ xs) eq = cong (x ∷_) (updateAt-id-relative i xs eq) +updateAt-id-local : ∀ (i : Fin n) {f : A → A} (xs : Vec A n) → + f (lookup xs i) ≡ lookup xs i → + updateAt i f xs ≡ xs +updateAt-id-local zero (x ∷ xs) eq = cong (_∷ xs) eq +updateAt-id-local (suc i) (x ∷ xs) eq = cong (x ∷_) (updateAt-id-local i xs eq) -- 1b. identity: updateAt i id ≗ id updateAt-id : ∀ (i : Fin n) (xs : Vec A n) → updateAt i id xs ≡ xs -updateAt-id i xs = updateAt-id-relative i xs refl +updateAt-id i xs = updateAt-id-local i xs refl --- 2a. relative composition: f ∘ g = h ↾ (lookup xs i) --- implies updateAt i f ∘ updateAt i g = updateAt i h ↾ xs +-- 2a. local composition: f ∘ g = h ↾ (lookup xs i) +-- implies updateAt i f ∘ updateAt i g = updateAt i h ↾ xs -updateAt-compose-relative : ∀ (i : Fin n) {f g h : A → A} (xs : Vec A n) → - f (g (lookup xs i)) ≡ h (lookup xs i) → - updateAt i f (updateAt i g xs) ≡ updateAt i h xs -updateAt-compose-relative zero (x ∷ xs) fg=h = cong (_∷ xs) fg=h -updateAt-compose-relative (suc i) (x ∷ xs) fg=h = - cong (x ∷_) (updateAt-compose-relative i xs fg=h) +updateAt-∘-local : ∀ (i : Fin n) {f g h : A → A} (xs : Vec A n) → + f (g (lookup xs i)) ≡ h (lookup xs i) → + updateAt i f (updateAt i g xs) ≡ updateAt i h xs +updateAt-∘-local zero (x ∷ xs) fg=h = cong (_∷ xs) fg=h +updateAt-∘-local (suc i) (x ∷ xs) fg=h = cong (x ∷_) (updateAt-∘-local i xs fg=h) -- 2b. composition: updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) -updateAt-compose : ∀ (i : Fin n) {f g : A → A} → +updateAt-∘ : ∀ (i : Fin n) {f g : A → A} → updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) -updateAt-compose i xs = updateAt-compose-relative i xs refl +updateAt-∘ i xs = updateAt-∘-local i xs refl -- 3. congruence: updateAt i is a congruence wrt. extensional equality. -- 3a. If f = g ↾ (lookup xs i) -- then updateAt i f = updateAt i g ↾ xs -updateAt-cong-relative : ∀ (i : Fin n) {f g : A → A} (xs : Vec A n) → - f (lookup xs i) ≡ g (lookup xs i) → - updateAt i f xs ≡ updateAt i g xs -updateAt-cong-relative zero (x ∷ xs) f=g = cong (_∷ xs) f=g -updateAt-cong-relative (suc i) (x ∷ xs) f=g = cong (x ∷_) (updateAt-cong-relative i xs f=g) +updateAt-cong-local : ∀ (i : Fin n) {f g : A → A} (xs : Vec A n) → + f (lookup xs i) ≡ g (lookup xs i) → + updateAt i f xs ≡ updateAt i g xs +updateAt-cong-local zero (x ∷ xs) f=g = cong (_∷ xs) f=g +updateAt-cong-local (suc i) (x ∷ xs) f=g = cong (x ∷_) (updateAt-cong-local i xs f=g) -- 3b. congruence: f ≗ g → updateAt i f ≗ updateAt i g updateAt-cong : ∀ (i : Fin n) {f g : A → A} → f ≗ g → updateAt i f ≗ updateAt i g -updateAt-cong i f≗g xs = updateAt-cong-relative i xs (f≗g (lookup xs i)) +updateAt-cong i f≗g xs = updateAt-cong-local i xs (f≗g (lookup xs i)) -- The order of updates at different indices i ≢ j does not matter. @@ -337,11 +336,11 @@ lookup∘updateAt′ i j xs i≢j = []%=-id : ∀ (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs []%=-id xs i = updateAt-id i xs -[]%=-compose : ∀ (xs : Vec A n) (i : Fin n) {f g : A → A} → +[]%=-∘ : ∀ (xs : Vec A n) (i : Fin n) {f g : A → A} → xs [ i ]%= f [ i ]%= g ≡ xs [ i ]%= g ∘ f -[]%=-compose xs i = updateAt-compose i xs +[]%=-∘ xs i = updateAt-∘ i xs ------------------------------------------------------------------------ @@ -352,7 +351,7 @@ lookup∘updateAt′ i j xs i≢j = []≔-idempotent : ∀ (xs : Vec A n) (i : Fin n) → (xs [ i ]≔ x) [ i ]≔ y ≡ xs [ i ]≔ y -[]≔-idempotent xs i = updateAt-compose i xs +[]≔-idempotent xs i = updateAt-∘ i xs []≔-commutes : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j → (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x @@ -366,7 +365,7 @@ lookup∘updateAt′ i j xs i≢j = []≔-minimal xs i j i≢j loc = updateAt-minimal i j xs i≢j loc []≔-lookup : ∀ (xs : Vec A n) (i : Fin n) → xs [ i ]≔ lookup xs i ≡ xs -[]≔-lookup xs i = updateAt-id-relative i xs refl +[]≔-lookup xs i = updateAt-id-local i xs refl []≔-++-↑ˡ : ∀ (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ i ↑ˡ n ]≔ x ≡ (xs [ i ]≔ x) ++ ys @@ -483,7 +482,7 @@ lookup-splitAt zero [] ys i = refl lookup-splitAt (suc m) (x ∷ xs) ys zero = refl lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = trans (lookup-splitAt m xs ys i) - (sym ([,]-map-commute (Fin.splitAt m i))) + (sym ([,]-map (Fin.splitAt m i))) ------------------------------------------------------------------------ -- concat @@ -1060,6 +1059,36 @@ toList∘fromList (x List.∷ xs) = cong (x List.∷_) (toList∘fromList xs) -- Version 2.0 +updateAt-id-relative = updateAt-id-local +{-# WARNING_ON_USAGE updateAt-id-relative +"Warning: updateAt-id-relative was deprecated in v2.0. +Please use updateAt-id-local instead." +#-} + +updateAt-compose-relative = updateAt-∘-local +{-# WARNING_ON_USAGE updateAt-compose-relative +"Warning: updateAt-compose-relative was deprecated in v2.0. +Please use updateAt-∘-local instead." +#-} + +updateAt-compose = updateAt-∘ +{-# WARNING_ON_USAGE updateAt-compose +"Warning: updateAt-compose was deprecated in v2.0. +Please use updateAt-∘ instead." +#-} + +updateAt-cong-relative = updateAt-cong-local +{-# WARNING_ON_USAGE updateAt-cong-relative +"Warning: updateAt-cong-relative was deprecated in v2.0. +Please use updateAt-cong-local instead." +#-} + +[]%=-compose = []%=-∘ +{-# WARNING_ON_USAGE []%=-compose +"Warning: []%=-compose was deprecated in v2.0. +Please use []%=-∘ instead." +#-} + []≔-++-inject+ : ∀ {m n x} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ i ↑ˡ n ]≔ x ≡ (xs [ i ]≔ x) ++ ys []≔-++-inject+ = []≔-++-↑ˡ diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda index f97c91ef43..5ae48cb0d3 100644 --- a/src/Data/Vec/Recursive/Properties.agda +++ b/src/Data/Vec/Recursive/Properties.agda @@ -37,10 +37,10 @@ tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as tail-cons-identity 0 a as = P.refl tail-cons-identity (suc n) a as = P.refl -append-cons-commute : ∀ m n a (xs : A ^ m) ys → +append-cons : ∀ m n a (xs : A ^ m) ys → append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys) -append-cons-commute 0 n a xs ys = P.refl -append-cons-commute (suc m) n a xs ys = P.refl +append-cons 0 n a xs ys = P.refl +append-cons (suc m) n a xs ys = P.refl append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as append-splitAt-identity 0 n as = P.refl @@ -48,7 +48,7 @@ append-splitAt-identity (suc m) n as = begin let x = head (m + n) as in let (xs , ys) = splitAt m n (tail (m + n) as) in append (suc m) n (cons m (head (m + n) as) xs) ys - ≡⟨ append-cons-commute m n x xs ys ⟩ + ≡⟨ append-cons m n x xs ys ⟩ cons (m + n) x (append m n xs ys) ≡⟨ P.cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩ cons (m + n) x (tail (m + n) as) @@ -83,3 +83,17 @@ toVec∘fromVec {n = suc n} (x Vec.∷ xs) = begin ↔Vec : ∀ n → A ^ n ↔ Vec A n ↔Vec n = inverse (toVec n) fromVec (fromVec∘toVec n) toVec∘fromVec + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +append-cons-commute = append-cons +{-# WARNING_ON_USAGE append-cons-commute +"Warning: append-cons-commute was deprecated in v2.0. +Please use append-cons instead." +#-} diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda index 779feb6515..991efdba33 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda @@ -73,11 +73,11 @@ open PW public using (++⁺ ; ++⁻ ; ++ˡ⁻; ++ʳ⁻) ++-assoc [] ys zs = ≋-refl ++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs -map-++-commute : ∀ {b m n} {B : Set b} +map-++ : ∀ {b m n} {B : Set b} (f : B → A) (xs : Vec B m) {ys : Vec B n} → map f (xs ++ ys) ≋ map f xs ++ map f ys -map-++-commute f [] = ≋-refl -map-++-commute f (x ∷ xs) = refl ∷ map-++-commute f xs +map-++ f [] = ≋-refl +map-++ f (x ∷ xs) = refl ∷ map-++ f xs ------------------------------------------------------------------------ -- concat @@ -92,3 +92,17 @@ replicate-shiftʳ : ∀ {m} n x (xs : Vec A m) → replicate {n = 1 + n} x ++ xs replicate-shiftʳ zero x xs = ≋-refl replicate-shiftʳ (suc n) x xs = refl ∷ (replicate-shiftʳ n x xs) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-++-commute = map-++ +{-# WARNING_ON_USAGE map-++-commute +"Warning: map-++-commute was deprecated in v2.0. +Please use map-++ instead." +#-}