From 0be9346ee95fbf409c701e28daa32d52e0011a37 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 3 Aug 2023 18:01:25 -0400 Subject: [PATCH 1/5] Add `drop-drop` in `Data.List.Properties` Dropping m elements and then n elements is same as dropping n+m elements --- CHANGELOG.md | 14 ++++++++------ src/Data/List/Properties.agda | 9 ++++++++- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3818f1a6f7..907efab0ab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2205,15 +2205,17 @@ Other minor changes drop-map : drop n (map f xs) ≡ map f (drop n xs) head-map : head (map f xs) ≡ Maybe.map f (head xs) - take-suc : (o : Fin (length xs)) → let m = toℕ o in take (suc m) xs ≡ take m xs ∷ʳ lookup xs o - take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o - drop-take-suc : (o : Fin (length xs)) → let m = toℕ o in drop m (take (suc m) xs) ≡ [ lookup xs o ] - drop-take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in drop m (take (suc m) (tabulate f)) ≡ [ f o ] + take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in take (suc m) xs ≡ take m xs ∷ʳ lookup xs i + take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i + drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in drop m (take (suc m) xs) ≡ [ lookup xs i ] + drop-take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ] + + drop-drop : drop n (drop m x) ≡ drop (n + m) x take-all : n ≥ length xs → take n xs ≡ xs - take-[] : ∀ m → take m [] ≡ [] - drop-[] : ∀ m → drop m [] ≡ [] + take-[] : take m [] ≡ [] + drop-[] : drop m [] ≡ [] ``` * Added new patterns and definitions to `Data.Nat.Base`: diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index ca5ffe27f2..48c7956671 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -780,7 +780,7 @@ take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym -- If you take at least as many elements from a list as it has, you get -- the whole list. -take-all :(n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs +take-all : (n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs take-all zero [] _ = refl take-all (suc _) [] _ = refl take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf) @@ -824,6 +824,13 @@ drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i) = drop-take-suc (tabulate f) (cast _ i) +-- Dropping m elements and then n elements is same as dropping n+m elements +drop-drop : (n m : ℕ) → (x : List A) → drop n (drop m x) ≡ drop (n + m) x +drop-drop zero m x = refl +drop-drop (suc n) zero x rewrite +-identityʳ n = refl +drop-drop (suc n) (suc m) [] = refl +drop-drop (suc n) (suc m) (x ∷ xs) rewrite +-suc n m = drop-drop (suc n) m xs + ------------------------------------------------------------------------ -- splitAt From 09fc0365fe0f5fc96ae3e779672b2ea282b9dbb2 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 4 Aug 2023 17:30:00 -0400 Subject: [PATCH 2/5] Simplify the proof Co-authored-by: G. Allais --- CHANGELOG.md | 2 +- src/Data/List/Properties.agda | 9 ++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 907efab0ab..e07fb3d765 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2210,7 +2210,7 @@ Other minor changes drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in drop m (take (suc m) xs) ≡ [ lookup xs i ] drop-take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ] - drop-drop : drop n (drop m x) ≡ drop (n + m) x + drop-drop : drop n (drop m xs) ≡ drop (m + n) xs take-all : n ≥ length xs → take n xs ≡ xs diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 48c7956671..c1a697caa7 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -825,11 +825,10 @@ drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) = drop-take-suc (tabulate f) (cast _ i) -- Dropping m elements and then n elements is same as dropping n+m elements -drop-drop : (n m : ℕ) → (x : List A) → drop n (drop m x) ≡ drop (n + m) x -drop-drop zero m x = refl -drop-drop (suc n) zero x rewrite +-identityʳ n = refl -drop-drop (suc n) (suc m) [] = refl -drop-drop (suc n) (suc m) (x ∷ xs) rewrite +-suc n m = drop-drop (suc n) m xs +drop-drop : (m n : ℕ) → (xs : List A) → drop n (drop m xs) ≡ drop (m + n) xs +drop-drop zero n xs = refl +drop-drop (suc m) n [] = drop-[] n +drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs ------------------------------------------------------------------------ -- splitAt From 13e88ef4e30e9d5e2094b56653ef8b4bcea7c825 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 4 Aug 2023 17:32:57 -0400 Subject: [PATCH 3/5] Fix comment --- src/Data/List/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index c1a697caa7..fc31435e76 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -824,7 +824,7 @@ drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i) = drop-take-suc (tabulate f) (cast _ i) --- Dropping m elements and then n elements is same as dropping n+m elements +-- Dropping m elements and then n elements is same as dropping m+n elements drop-drop : (m n : ℕ) → (xs : List A) → drop n (drop m xs) ≡ drop (m + n) xs drop-drop zero n xs = refl drop-drop (suc m) n [] = drop-[] n From 808a5845ff08fec99e22221c787ba29d808f6374 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 11 Aug 2023 17:05:25 -0400 Subject: [PATCH 4/5] Rename `drop-fusion` and `drop-drop-fusion` to `drop-drop` --- CHANGELOG.md | 6 ++++-- src/Codata/Guarded/Stream/Properties.agda | 12 +++++++++--- src/Codata/Sized/Colist/Properties.agda | 14 ++++++++++---- 3 files changed, 23 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e07fb3d765..6533de7861 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1080,12 +1080,14 @@ Deprecated names ```agda map-identity ↦ map-id map-fusion ↦ map-∘ + drop-fusion ↦ drop-drop ``` * In `Codata.Sized.Colist.Properties`: ```agda - map-identity ↦ map-id - map-map-fusion ↦ map-∘ + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + drop-drop-fusion ↦ drop-drop ``` * In `Codata.Sized.Covec.Properties`: diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index df68a9c4b2..a07a614b59 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -268,9 +268,9 @@ take-zipWith (suc n) f as bs = ------------------------------------------------------------------------ -- Properties of drop -drop-fusion : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as -drop-fusion zero n as = P.refl -drop-fusion (suc m) n as = drop-fusion m n (as .tail) +drop-drop : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as +drop-drop zero n as = P.refl +drop-drop (suc m) n as = drop-drop m n (as .tail) drop-zipWith : ∀ n (f : A → B → C) as bs → drop n (zipWith f as bs) ≡ zipWith f (drop n as) (drop n bs) @@ -331,3 +331,9 @@ map-fusion = map-∘ "Warning: map-fusion was deprecated in v2.0. Please use map-∘ instead." #-} + +drop-fusion = drop-drop +{-# WARNING_ON_USAGE drop-fusion +"Warning: drop-fusion was deprecated in v2.0. +Please use drop-drop instead." +#-} diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index 5b77551b7f..2ec1564627 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -197,11 +197,11 @@ drop-nil : ∀ m → i ⊢ drop {A = A} m [] ≈ [] drop-nil zero = [] drop-nil (suc m) = [] -drop-drop-fusion : ∀ m n (as : Colist A ∞) → +drop-drop : ∀ m n (as : Colist A ∞) → i ⊢ drop n (drop m as) ≈ drop (m ℕ.+ n) as -drop-drop-fusion zero n as = refl -drop-drop-fusion (suc m) n [] = drop-nil n -drop-drop-fusion (suc m) n (a ∷ as) = drop-drop-fusion m n (as .force) +drop-drop zero n as = refl +drop-drop (suc m) n [] = drop-nil n +drop-drop (suc m) n (a ∷ as) = drop-drop m n (as .force) map-drop : ∀ (f : A → B) m as → i ⊢ map f (drop m as) ≈ drop m (map f as) map-drop f zero as = refl @@ -351,3 +351,9 @@ map-map-fusion = map-∘ "Warning: map-map-fusion was deprecated in v2.0. Please use map-∘ instead." #-} + +drop-drop-fusion = drop-drop +{-# WARNING_ON_USAGE drop-drop-fusion +"Warning: drop-drop-fusion was deprecated in v2.0. +Please use drop-drop instead." +#-} From 0d9317ad3bd8f8e6e4e05e461c6d5b52a6c1a868 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Sun, 13 Aug 2023 22:45:07 -0400 Subject: [PATCH 5/5] Update CHANGELOG --- CHANGELOG.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6533de7861..f3f4a7cfc5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2200,24 +2200,24 @@ Other minor changes concatMap-map : concatMap g (map f xs) ≡ concatMap (g ∘′ f) xs map-concatMap : map f ∘′ concatMap g ≗ concatMap (map f ∘′ g) - length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length + length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length take-map : take n (map f xs) ≡ map f (take n xs) drop-map : drop n (map f xs) ≡ map f (drop n xs) head-map : head (map f xs) ≡ Maybe.map f (head xs) - take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in take (suc m) xs ≡ take m xs ∷ʳ lookup xs i - take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i - drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in drop m (take (suc m) xs) ≡ [ lookup xs i ] - drop-take-suc-tabulate : (f : Fin n → A) (i : Fin n) → let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ] - - drop-drop : drop n (drop m xs) ≡ drop (m + n) xs + take-suc : take (suc m) xs ≡ take m xs ∷ʳ lookup xs i + take-suc-tabulate : take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i + drop-take-suc : drop m (take (suc m) xs) ≡ [ lookup xs i ] + drop-take-suc-tabulate : drop m (take (suc m) (tabulate f)) ≡ [ f i ] take-all : n ≥ length xs → take n xs ≡ xs - take-[] : take m [] ≡ [] - drop-[] : drop m [] ≡ [] + take-[] : take m [] ≡ [] + drop-[] : drop m [] ≡ [] + + drop-drop : drop n (drop m xs) ≡ drop (m + n) xs ``` * Added new patterns and definitions to `Data.Nat.Base`: