From 385a651adf7503b015ce61a3545bd7376504a627 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 10:40:42 +0100 Subject: [PATCH 01/24] resolves issue #626; begins addressing issue #509 --- src/Data/List/Properties.agda | 85 +++++++++++++++++++++++++---------- 1 file changed, 61 insertions(+), 24 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 898f29f85f..a61319a0b3 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -9,7 +9,7 @@ {-# OPTIONS --without-K --safe #-} -module Data.List.Properties where +module Data.List.PropertiesNEW where open import Algebra.Bundles open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) @@ -19,6 +19,7 @@ open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁) open import Data.List.Base as List open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_) + renaming (tabulate to All-local) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Base @@ -79,35 +80,41 @@ module _ {x y : A} {xs ys : List A} where ------------------------------------------------------------------------ -- map +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-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' : map id ≗ id {A = List A} +map-id' xs = map-id-local (All-local λ _ → refl) -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-local : ∀ {f g : A → B} {xs} → + All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs +map-cong-local [] = refl +map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs) 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} → - 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' : ∀ {f g : A → B} → f ≗ g → map f ≗ map g +map-cong' f≗g xs = map-cong-local (All-local λ _ → f≗g _) 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 +267,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 +503,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 +525,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 +571,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)) ∎) @@ -1004,6 +1011,36 @@ 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." +#-} + zipWith-identityˡ = zipWith-zeroˡ {-# WARNING_ON_USAGE zipWith-identityˡ "Warning: zipWith-identityˡ was deprecated in v2.0. From 0b28fa15795c10539300bc766ba5c93daa273c69 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 14:31:02 +0100 Subject: [PATCH 02/24] tidied up 'local' properties --- src/Data/List/Properties.agda | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index a61319a0b3..7d50753707 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -9,7 +9,7 @@ {-# OPTIONS --without-K --safe #-} -module Data.List.PropertiesNEW where +module Data.List.Properties where open import Algebra.Bundles open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) @@ -19,7 +19,6 @@ open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁) open import Data.List.Base as List open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_) - renaming (tabulate to All-local) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Base @@ -80,33 +79,27 @@ module _ {x y : A} {xs ys : List A} where ------------------------------------------------------------------------ -- map -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-id : map id ≗ id {A = List A} map-id [] = refl map-id (x ∷ xs) = cong (x ∷_) (map-id xs) -map-id' : map id ≗ id {A = List A} -map-id' xs = map-id-local (All-local λ _ → refl) +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-++ : ∀ (f : A → B) xs ys → map f (xs ++ ys) ≡ map f xs ++ map f ys map-++ f [] ys = refl map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys) -map-cong-local : ∀ {f g : A → B} {xs} → - All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs -map-cong-local [] = refl -map-cong-local (fx≡gx ∷ fxs≡gxs) = cong₂ _∷_ fx≡gx (map-cong-local fxs≡gxs) - 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} → f ≗ g → map f ≗ map g -map-cong' f≗g xs = map-cong-local (All-local λ _ → f≗g _) +map-cong-local : ∀ {f g : A → B} {xs} → + All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs +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 From a05d59df02a64b73e057b6797fb1c9336857f772 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 14:45:33 +0100 Subject: [PATCH 03/24] knock-on changes --- src/Data/Fin/Substitution/List.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Substitution/List.agda b/src/Data/Fin/Substitution/List.agda index 1ce9ee7340..dddce8b278 100644 --- a/src/Data/Fin/Substitution/List.agda +++ b/src/Data/Fin/Substitution/List.agda @@ -39,7 +39,7 @@ appLemmas = record ts ∎ ; /-⊙ = λ {_ _ _ ρ₁ ρ₂} ts → begin ts // ρ₁ ⊙ ρ₂ ≡⟨ map-cong L./-⊙ ts ⟩ - map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-compose ts ⟩ + map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-∘ ts ⟩ ts // ρ₁ // ρ₂ ∎ } From 55e8b643106f06f3a4380d49cd8b983d4aa35360 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 14:50:29 +0100 Subject: [PATCH 04/24] knock-on changes --- src/Data/List/NonEmpty/Properties.agda | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index e961fc402b..f14fe8e533 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -60,7 +60,7 @@ toList->>= : ∀ (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))) ∎ @@ -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,17 @@ 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." +#-} + From eb9e3eef89fe32673566db34221f4d9538b01029 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 15:02:27 +0100 Subject: [PATCH 05/24] knock-on changes --- src/Data/List/Properties.agda | 20 ++++++-- src/Data/List/Zipper/Properties.agda | 71 +++++++++++++++++++++------- 2 files changed, 71 insertions(+), 20 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 7d50753707..17f4159c86 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -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 ʳ++ [] ≡⟨⟩ @@ -1034,6 +1034,18 @@ sum-++-commute = sum-++ 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/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda index 7da32c5b89..549ee034f7 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,59 @@ 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." +#-} + From f35c323633aef9aabc9938fb1c308452bb0776c8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 15:33:14 +0100 Subject: [PATCH 06/24] more knock-on changes --- .../List/Relation/Binary/Suffix/Heterogeneous/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) → From 41ae9f0a66669ba8b2a1199bdcf82ad6978e50e6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 16:32:19 +0100 Subject: [PATCH 07/24] more knock-on changes --- src/Data/Tree/Rose/Properties.agda | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index 51d19732dc..de8add35e4 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,21 @@ 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." +#-} + From 2b8fc52fd6ea9fe8592a9e0478c25ad060ea1c4f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 16:35:08 +0100 Subject: [PATCH 08/24] more knock-on changes --- src/Data/List/NonEmpty/Properties.agda | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index f14fe8e533..5b6c41c50b 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -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 @@ -156,3 +156,9 @@ map-compose = map-∘ Please use map-∘ instead." #-} +map-++⁺-commute = map-++⁺ +{-# WARNING_ON_USAGE map-++⁺-commute +"Warning: map-++⁺-commute was deprecated in v2.0. +Please use map-++⁺ instead." +#-} + From 05fac98d6f003425a519e1cfc976d4e3b9d24c28 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 17:10:05 +0100 Subject: [PATCH 09/24] trailing whitespace --- src/Data/List/NonEmpty/Properties.agda | 1 - src/Data/List/Zipper/Properties.agda | 1 - src/Data/Tree/Rose/Properties.agda | 1 - 3 files changed, 3 deletions(-) diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda index 5b6c41c50b..938e721002 100644 --- a/src/Data/List/NonEmpty/Properties.agda +++ b/src/Data/List/NonEmpty/Properties.agda @@ -161,4 +161,3 @@ map-++⁺-commute = map-++⁺ "Warning: map-++⁺-commute was deprecated in v2.0. Please use map-++⁺ instead." #-} - diff --git a/src/Data/List/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda index 549ee034f7..30ea57a9c2 100644 --- a/src/Data/List/Zipper/Properties.agda +++ b/src/Data/List/Zipper/Properties.agda @@ -170,4 +170,3 @@ toList-foldr-commute = toList-foldr "Warning: toList-foldr-commute was deprecated in v2.0. Please use toList-foldr instead." #-} - diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index de8add35e4..a7ab845999 100644 --- a/src/Data/Tree/Rose/Properties.agda +++ b/src/Data/Tree/Rose/Properties.agda @@ -66,4 +66,3 @@ map-compose = map-∘ "Warning: map-compose was deprecated in v2.0. Please use map-∘ instead." #-} - From 00e17114db1f2102ce29fd67903d5df45c1c7dc5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 15 Sep 2022 17:29:27 +0100 Subject: [PATCH 10/24] yet more... --- src/Data/Maybe/Properties.agda | 56 ++++++++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 12 deletions(-) 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." +#-} From 4f6afcb72ed275767c92da576c09f8275c8b2898 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 16 Sep 2022 12:25:57 +0100 Subject: [PATCH 11/24] updateAt now localised as well --- .../List/Relation/Unary/All/Properties.agda | 74 ++++++++++------ src/Data/Vec/Functional/Properties.agda | 88 +++++++++++++------ src/Data/Vec/Properties.agda | 87 ++++++++++++------ 3 files changed, 167 insertions(+), 82 deletions(-) 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/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index 65875e1ae3..0ba901fec7 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -75,37 +75,37 @@ 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 @@ -263,3 +263,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..35bfab9af6 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -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 @@ -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+ = []≔-++-↑ˡ From cf39a77d38b53ae033367c4e3c4ccc89d8b31236 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 16 Sep 2022 14:45:29 +0100 Subject: [PATCH 12/24] updated CHANGELOG --- CHANGELOG.md | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b647d5114..03f76d5305 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -719,10 +719,53 @@ 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.Nat.Properties`: ``` suc[pred[n]]≡n ↦ suc-pred @@ -758,8 +801,20 @@ Deprecated names negative Date: Fri, 16 Sep 2022 16:47:16 +0100 Subject: [PATCH 13/24] more instances of \-commute --- CHANGELOG.md | 5 +++++ .../Vec/Relation/Binary/Equality/Setoid.agda | 20 ++++++++++++++++--- 2 files changed, 22 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 03f76d5305..b0617f1004 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -837,6 +837,11 @@ Deprecated names updateAt-cong-relative ↦ updateAt-cong-local ``` +* In `Data.Vec.Relation.Binary.Equality.Setoid`: + ```agda + map-++-commute ↦ map-++ + ``` + * In `Function.Construct.Composition`: ``` _∘-⟶_ ↦ _⟶-∘_ 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." +#-} From 30e6ce61a4027a97698a5307c175b702e104d983 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 10:19:50 +0100 Subject: [PATCH 14/24] another bit of #509 (-commute) and #626 (local/global) --- src/Data/Vec/Functional/Properties.agda | 5 +---- src/Data/Vec/Recursive/Properties.agda | 22 ++++++++++++++++++---- 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index 0ba901fec7..fbd865748d 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -109,10 +109,7 @@ 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. 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." +#-} From 027466b512572cc0548c821bf44e7ae0febc7b6b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 10:27:46 +0100 Subject: [PATCH 15/24] another leaf node of #509 (-commute) --- src/Data/Tree/Binary/Zipper/Properties.agda | 68 +++++++++++++++++---- 1 file changed, 56 insertions(+), 12 deletions(-) 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." +#-} From 90d862ee15e8c02fdda8f638e098ca7ac3b38a15 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 10:42:07 +0100 Subject: [PATCH 16/24] =?UTF-8?q?chnaging=20to=20[,]-map=20and=20[,]-?= =?UTF-8?q?=E2=88=98=20and=20their=20knock-ons?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Fin/Properties.agda | 6 +++--- src/Data/Sum/Properties.agda | 37 ++++++++++++++++++++++++++++-------- src/Data/Vec/Properties.agda | 4 ++-- 3 files changed, 34 insertions(+), 13 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 4ecd2bc722..95e65383cb 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -25,7 +25,7 @@ open import Data.Product using (Σ-syntax; ∃; ∃₂; ∄; _×_; _,_; map; pro open import Data.Product.Properties using (,-injective) open import Data.Product.Algebra using (×-cong) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) -open import Data.Sum.Properties using ([,]-map-commute; [,]-∘-distr) +open import Data.Sum.Properties using ([,]-map; [,]-∘) open import Function.Base using (_∘_; id; _$_; flip) open import Function.Bundles using (Injection; _↣_; _⇔_; _↔_; mk⇔; mk↔′) open import Function.Definitions using (Injective) @@ -563,8 +563,8 @@ join-splitAt : ∀ m n i → join m n (splitAt m i) ≡ i join-splitAt zero n i = refl join-splitAt (suc m) n zero = refl join-splitAt (suc m) n (suc i) = begin - [ _↑ˡ n , (suc m) ↑ʳ_ ]′ (splitAt (suc m) (suc i)) ≡⟨ [,]-map-commute (splitAt m i) ⟩ - [ suc ∘ (_↑ˡ n) , suc ∘ (m ↑ʳ_) ]′ (splitAt m i) ≡˘⟨ [,]-∘-distr suc (splitAt m i) ⟩ + [ _↑ˡ n , (suc m) ↑ʳ_ ]′ (splitAt (suc m) (suc i)) ≡⟨ [,]-map (splitAt m i) ⟩ + [ suc ∘ (_↑ˡ n) , suc ∘ (m ↑ʳ_) ]′ (splitAt m i) ≡˘⟨ [,]-∘ suc (splitAt m i) ⟩ suc ([ _↑ˡ n , m ↑ʳ_ ]′ (splitAt m i)) ≡⟨ cong suc (join-splitAt m n i) ⟩ suc i ∎ where open ≡-Reasoning diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda index c881601af9..24331afce1 100644 --- a/src/Data/Sum/Properties.agda +++ b/src/Data/Sum/Properties.agda @@ -53,17 +53,17 @@ 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} {f′ : B → E} {g′ : D → F} → @@ -118,3 +118,24 @@ 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 + +[,]-map-commute = [,]-map +{-# WARNING_ON_USAGE [,]-map-commute +"Warning: [,]-map-commute was deprecated in v2.0. +Please use [,]-map instead." +#-} + +[,]-∘-distr = [,]-∘ +{-# WARNING_ON_USAGE [,]-∘-distr +"Warning: [,]-∘-distr was deprecated in v2.0. +Please use [,]-∘ instead." +#-} + diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 35bfab9af6..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) @@ -482,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 From eda5d3cea66acd634b649570aab72cb11fc817bd Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 10:52:23 +0100 Subject: [PATCH 17/24] CHANGELOG --- CHANGELOG.md | 21 +++++++++++++++++++++ src/Data/Sum/Properties.agda | 11 +++++------ 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b0617f1004..3be0a31fcb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -801,6 +801,22 @@ Deprecated names negative Date: Sat, 17 Sep 2022 11:01:12 +0100 Subject: [PATCH 18/24] cosmetic changes to Data.Sum.Properties in line with #509 --- CHANGELOG.md | 2 ++ src/Data/Sum/Properties.agda | 24 ++++++++++++++++++------ 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3be0a31fcb..1cde04277c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -805,6 +805,8 @@ Deprecated names ```agda [,]-∘-distr ↦ [,]-∘ [,]-map-commute ↦ [,]-map + map-commute ↦ map-map + map₁₂-commute ↦ map₁₂-map₂₁ ``` * In `Data.Tree.Binary.Zipper.Properties`: diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda index 87b6e520bb..7042b8682f 100644 --- a/src/Data/Sum/Properties.agda +++ b/src/Data/Sum/Properties.agda @@ -65,16 +65,16 @@ map-id (inj₂ _) = refl [,]-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) @@ -138,3 +138,15 @@ Please use [,]-∘ instead." "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." +#-} From 7337a1cfa30f5494bbaca383e3d546164e0044eb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 11:34:08 +0100 Subject: [PATCH 19/24] problematic #626 change from 'global' to -local, with new 'global' added --- CHANGELOG.md | 8 ++++++++ src/Data/Vec/Functional/Properties.agda | 18 ++++++++++++------ 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1cde04277c..a6177a141d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -853,7 +853,10 @@ Deprecated names updateAt-compose-relative ↦ updateAt-∘-local updateAt-compose ↦ updateAt-∘ updateAt-cong-relative ↦ updateAt-cong-local + + map-updateAt ↦ map-updateAt-local ``` + NB. This last one is complicated by the *addition* of a 'global' property `map-updateAt` * In `Data.Vec.Recursive.Properties`: ``` @@ -1752,6 +1755,11 @@ Other minor changes transpose-replicate : transpose (replicate xs) ≡ map replicate xs ``` +* Added new proofs in `Data.Vec.Functional.Properties`: + ``` + map-updateAt : f ∘ g ≗ h ∘ f → map f (updateAt i g xs) ≗ updateAt i h (map f xs) + ``` + * Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`: ```agda xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < [] diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index fbd865748d..926627ed17 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -140,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)) ------------------------------------------------------------------------ -- _++_ From 7a47c46db8f88abd664ded79b5d84c8239ff0bd5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 12:43:02 +0100 Subject: [PATCH 20/24] Codata instances of #509 --- CHANGELOG.md | 6 +++++ src/Codata/Guarded/Stream/Properties.agda | 33 ++++++++++++++++++----- 2 files changed, 33 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a6177a141d..4232b9246e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -636,6 +636,12 @@ Deprecated modules Deprecated names ---------------- +* In `Codata.Guarded.Stream.Properties`: + ```agda + map-identity ↦ map-id + 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 diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index 26bff107c5..72082da0ef 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -134,13 +134,13 @@ map-const : (a : A) (bs : Stream B) → map (const a) bs ≈ repeat a map-const a bs .head = P.refl map-const a bs .tail = map-const a (bs .tail) -map-identity : (as : Stream A) → map id as ≈ as -map-identity as .head = P.refl -map-identity as .tail = map-identity (as .tail) +map-id : (as : Stream A) → map id as ≈ as +map-id as .head = P.refl +map-id as .tail = map-id (as .tail) -map-fusion : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as -map-fusion g f as .head = P.refl -map-fusion g f as .tail = map-fusion g f (as .tail) +map-∘ : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as +map-∘ g f as .head = P.refl +map-∘ g f as .tail = map-∘ g f (as .tail) map-unfold : ∀ (g : B → C) (f : A → A × B) a → map g (unfold f a) ≈ unfold (Prod.map₂ g ∘′ f) a @@ -309,3 +309,24 @@ interleave-evens-odds : (as : Stream A) → interleave (evens as) (odds as) ≈ interleave-evens-odds as .head = P.refl interleave-evens-odds as .tail .head = P.refl interleave-evens-odds as .tail .tail = interleave-evens-odds (as .tail .tail) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-identity = map-id +{-# WARNING_ON_USAGE map-identity +"Warning: map-identity was deprecated in v2.0. +Please use map-id instead." +#-} + +map-fusion = map-∘ +{-# WARNING_ON_USAGE map-fusion +"Warning: map-fusion was deprecated in v2.0. +Please use map-∘ instead." +#-} + From e727ddf536751e422d0132584da186623e1b9fdb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 12:46:36 +0100 Subject: [PATCH 21/24] Codata instances of #509 --- CHANGELOG.md | 6 +++++ src/Codata/Guarded/Stream/Properties.agda | 1 - src/Codata/Sized/Stream/Properties.agda | 28 +++++++++++++++++++---- 3 files changed, 30 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4232b9246e..d1a825e514 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -642,6 +642,12 @@ Deprecated names map-fusion ↦ map-∘ ``` +* In `Codata.Sized.Stream.Properties`: + ```agda + map-identity ↦ map-id + map-mapfusion ↦ 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 diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index 72082da0ef..62ae41b014 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -329,4 +329,3 @@ map-fusion = map-∘ "Warning: map-fusion was deprecated in v2.0. Please use map-∘ instead." #-} - diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda index c3773e5f2f..466a4d2db6 100644 --- a/src/Codata/Sized/Stream/Properties.agda +++ b/src/Codata/Sized/Stream/Properties.agda @@ -90,11 +90,11 @@ module _ {a b} {A : Set a} {B : Set b} where ------------------------------------------------------------------------ -- Functor laws -map-identity : ∀ (as : Stream A ∞) → i ⊢ map id as ≈ as -map-identity (a ∷ as) = P.refl ∷ λ where .force → map-identity (as .force) +map-id : ∀ (as : Stream A ∞) → i ⊢ map id as ≈ as +map-id (a ∷ as) = P.refl ∷ λ where .force → map-id (as .force) -map-map-fusion : ∀ (f : A → B) (g : B → C) as → i ⊢ map g (map f as) ≈ map (g ∘′ f) as -map-map-fusion f g (a ∷ as) = P.refl ∷ λ where .force → map-map-fusion f g (as .force) +map-∘ : ∀ (f : A → B) (g : B → C) as → i ⊢ map g (map f as) ≈ map (g ∘′ f) as +map-∘ f g (a ∷ as) = P.refl ∷ λ where .force → map-∘ f g (as .force) ------------------------------------------------------------------------ @@ -117,3 +117,23 @@ lookup-iterate-identity (suc n) f a = begin fold (f a) f n ≡⟨ fold-pull a f (const ∘′ f) (f a) P.refl (λ _ → P.refl) n ⟩ f (fold a f n) ≡⟨⟩ fold a f (suc n) ∎ where open P.≡-Reasoning + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-identity = map-id +{-# WARNING_ON_USAGE map-identity +"Warning: map-identity was deprecated in v2.0. +Please use map-id instead." +#-} + +map-map-fusion = map-∘ +{-# WARNING_ON_USAGE map-map-fusion +"Warning: map-map-fusion was deprecated in v2.0. +Please use map-∘ instead." +#-} From 15f3189cd034ef6fa03e5cbb0a12326d61f6b7e2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 12:53:03 +0100 Subject: [PATCH 22/24] Codata instances of #509 --- CHANGELOG.md | 6 ++++ src/Codata/Sized/Colist/Properties.agda | 38 +++++++++++++++++++------ src/Codata/Sized/Covec/Properties.agda | 32 +++++++++++++++++---- 3 files changed, 61 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d1a825e514..84d13c43d8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -642,6 +642,12 @@ Deprecated names map-fusion ↦ map-∘ ``` +* In `Codata.Sized.Covec.Properties`: + ```agda + map-identity ↦ map-id + map-mapfusion ↦ map-∘ + ``` + * In `Codata.Sized.Stream.Properties`: ```agda map-identity ↦ map-id diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index 76908cad6c..26e7f45f10 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -45,15 +45,15 @@ private ------------------------------------------------------------------------ -- Functor laws -map-identity : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as -map-identity [] = [] -map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force) +map-id : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as +map-id [] = [] +map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force) -map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} → +map-∘ : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as -map-map-fusion f g [] = [] -map-map-fusion f g (a ∷ as) = - Eq.refl ∷ λ where .force → map-map-fusion f g (as .force) +map-∘ f g [] = [] +map-∘ f g (a ∷ as) = + Eq.refl ∷ λ where .force → map-∘ f g (as .force) ------------------------------------------------------------------------ -- Relation to Cowriter @@ -161,8 +161,8 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where map-alignWith : ∀ (f : C → D) (al : These A B → C) as bs → i ⊢ map f (alignWith al as bs) ≈ alignWith (f ∘ al) as bs -map-alignWith f al [] bs = map-map-fusion (al ∘′ that) f bs -map-alignWith f al as@(_ ∷ _) [] = map-map-fusion (al ∘′ this) f as +map-alignWith f al [] bs = map-∘ (al ∘′ that) f bs +map-alignWith f al as@(_ ∷ _) [] = map-∘ (al ∘′ this) f as map-alignWith f al (a ∷ as) (b ∷ bs) = Eq.refl ∷ λ where .force → map-alignWith f al (as .force) (bs .force) @@ -331,3 +331,23 @@ map-fromStream : ∀ (f : A → B) as → i ⊢ map f (fromStream as) ≈ fromStream (Stream.map f as) map-fromStream f (a ∷ as) = Eq.refl ∷ λ where .force → map-fromStream f (as .force) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-identity = map-id +{-# WARNING_ON_USAGE map-identity +"Warning: map-identity was deprecated in v2.0. +Please use map-id instead." +#-} + +map-map-fusion = map-∘ +{-# WARNING_ON_USAGE map-map-fusion +"Warning: map-map-fusion was deprecated in v2.0. +Please use map-∘ instead." +#-} diff --git a/src/Codata/Sized/Covec/Properties.agda b/src/Codata/Sized/Covec/Properties.agda index eb09c06429..468e379c47 100644 --- a/src/Codata/Sized/Covec/Properties.agda +++ b/src/Codata/Sized/Covec/Properties.agda @@ -20,12 +20,32 @@ open import Relation.Binary.PropositionalEquality as Eq module _ {a} {A : Set a} where - map-identity : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as - map-identity [] = [] - map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force) + map-id : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as + map-id [] = [] + map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force) module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where - map-map-fusion : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as - map-map-fusion f g [] = [] - map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force) + map-∘ : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as + map-∘ f g [] = [] + map-∘ f g (a ∷ as) = Eq.refl ∷ λ where .force → map-∘ f g (as .force) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-identity = map-id +{-# WARNING_ON_USAGE map-identity +"Warning: map-identity was deprecated in v2.0. +Please use map-id instead." +#-} + +map-map-fusion = map-∘ +{-# WARNING_ON_USAGE map-map-fusion +"Warning: map-map-fusion was deprecated in v2.0. +Please use map-∘ instead." +#-} From 60b564b99a1e5f0ca993fd6de44597314a8799d9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 13:05:43 +0100 Subject: [PATCH 23/24] Codata instances of #509: Sized/Delay --- CHANGELOG.md | 22 +++++++++++-- src/Codata/Sized/Delay/Properties.agda | 44 ++++++++++++++++++++++---- 2 files changed, 57 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 84d13c43d8..d37d455c89 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -642,16 +642,29 @@ Deprecated names 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-mapfusion ↦ map-∘ + 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.Stream.Properties`: ```agda map-identity ↦ map-id - map-mapfusion ↦ map-∘ + map-map-fusion ↦ map-∘ ``` * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ` @@ -1343,6 +1356,11 @@ Other minor changes execState : State s a → s → s ``` +* Added new proofs in `Codata.Sized.Delay.Properties`: + ```agda + map-id : i ⊢ map id da ≈ da + ``` + * Added new proofs in `Data.Bool.Properties`: ```agda <-wellFounded : WellFounded _<_ diff --git a/src/Codata/Sized/Delay/Properties.agda b/src/Codata/Sized/Delay/Properties.agda index e57551e892..5fa3b7c629 100644 --- a/src/Codata/Sized/Delay/Properties.agda +++ b/src/Codata/Sized/Delay/Properties.agda @@ -39,16 +39,20 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where length-zipWith f (later da) (later db) = suc λ where .force → length-zipWith f (da .force) (db .force) - map-map-fusion : ∀ (f : A → B) (g : B → C) da {i} → + map-id : ∀ da {i} → i ⊢ map (id {A = A}) da ≈ da + map-id (now a) = now Eq.refl + map-id (later da) = later λ where .force → map-id (da .force) + + map-∘ : ∀ (f : A → B) (g : B → C) da {i} → i ⊢ map g (map f da) ≈ map (g ∘′ f) da - map-map-fusion f g (now a) = now Eq.refl - map-map-fusion f g (later da) = later λ where .force → map-map-fusion f g (da .force) + map-∘ f g (now a) = now Eq.refl + map-∘ f g (later da) = later λ where .force → map-∘ f g (da .force) - map-unfold-fusion : ∀ (f : B → C) n (s : A) {i} → + map-unfold : ∀ (f : B → C) n (s : A) {i} → i ⊢ map f (unfold n s) ≈ unfold (Sum.map id f ∘′ n) s - map-unfold-fusion f n s with n s - ... | Sum.inj₁ s′ = later λ where .force → map-unfold-fusion f n s′ - ... | Sum.inj₂ b = now Eq.refl + map-unfold f n s with n s + ... | Sum.inj₁ s′ = later λ where .force → map-unfold f n s′ + ... | Sum.inj₂ b = now Eq.refl ------------------------------------------------------------------------ @@ -105,3 +109,29 @@ module _ {a} {A B : Set a} where Eq.cong (toℕ ∘′ length-⇓) (⇓-unique bind⇓ f⇓) bind⇓-length {d = d@(later dt)} {f = f} bind⇓@(later bind'⇓) d⇓@(later r) f⇓ = Eq.cong ℕ.suc (bind⇓-length bind'⇓ r f⇓) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +map-identity = map-id +{-# WARNING_ON_USAGE map-identity +"Warning: map-identity was deprecated in v2.0. +Please use map-id instead." +#-} + +map-map-fusion = map-∘ +{-# WARNING_ON_USAGE map-map-fusion +"Warning: map-map-fusion was deprecated in v2.0. +Please use map-∘ instead." +#-} + +map-unfold-fusion = map-unfold +{-# WARNING_ON_USAGE map-unfold-fusion +"Warning: map-unfold-fusion was deprecated in v2.0. +Please use map-unfold instead." +#-} From 11ff5afae62f1c6cc762681f5749abda51c019ea Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 17 Sep 2022 13:08:44 +0100 Subject: [PATCH 24/24] Codata instances of #509: Sized/M --- CHANGELOG.md | 5 +++++ src/Codata/Sized/M/Properties.agda | 18 ++++++++++++++++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d37d455c89..1b24879e14 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -661,6 +661,11 @@ Deprecated names map-unfold-fusion ↦ map-unfold ``` +* In `Codata.Sized.M.Properties`: + ```agda + map-compose ↦ map-∘ + ``` + * In `Codata.Sized.Stream.Properties`: ```agda map-identity ↦ map-id diff --git a/src/Codata/Sized/M/Properties.agda b/src/Codata/Sized/M/Properties.agda index 30b0c8d131..60e69618f5 100644 --- a/src/Codata/Sized/M/Properties.agda +++ b/src/Codata/Sized/M/Properties.agda @@ -46,9 +46,9 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s module _ {s₁ s₂ s₃ p₁ p₂ p₃} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃} where - map-compose : ∀ {i} {g : C₂ ⇒ C₃} {f : C₁ ⇒ C₂} c₁ → + map-∘ : ∀ {i} {g : C₂ ⇒ C₃} {f : C₁ ⇒ C₂} c₁ → Bisim C₃ i (map (g Mp.∘ f) c₁) (map g $′ map f c₁) - map-compose (inf (s , f)) = inf (P.refl , λ where p .force → map-compose (f _ .force)) + map-∘ (inf (s , f)) = inf (P.refl , λ where p .force → map-∘ (f _ .force)) module _ {s₁ s₂ p₁ p₂ s} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} @@ -57,3 +57,17 @@ module _ {s₁ s₂ p₁ p₂ s} {C₁ : Container s₁ p₁} {C₂ : Container map-unfold : ∀ {i} s → Bisim C₂ i (map f (unfold alg s)) (unfold (⟪ f ⟫ ∘′ alg) s) map-unfold s = inf (P.refl , λ where p .force → map-unfold _) + +------------------------------------------------------------------------ +-- 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." +#-}