From 2f4008023de53992c5b4a098160a5421a557fff7 Mon Sep 17 00:00:00 2001 From: Sofia-Insa Date: Wed, 14 Jun 2023 13:13:04 -0400 Subject: [PATCH 1/7] Added new function to --- src/Data/List/Properties.agda | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 312ef2e7a8..f45564d6ab 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -758,6 +758,13 @@ length-take zero xs = refl length-take (suc n) [] = refl length-take (suc n) (x ∷ xs) = cong suc (length-take n xs) +-- If you take at least as many elements from a list as it has, you get the whole list. +take-all : {a : Level} {A : Set a} (k : ℕ) (l : List A) → (k ≥ length l) → take k l ≡ l +take-all ℕ.zero [] _ = refl +take-all (suc _) [] _ = refl +take-all (suc k) (x ∷ l) (s≤s pf) = cong (x ∷_) (take-all k l pf) + + ------------------------------------------------------------------------ -- drop From 577c161957fd6e17bb57e12b3df1913db3415038 Mon Sep 17 00:00:00 2001 From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com> Date: Wed, 14 Jun 2023 13:21:00 -0400 Subject: [PATCH 2/7] Update CHANGELOG.md add take-all to stdl Data.List.Propreties --- CHANGELOG.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d5ba31beaf..bbec36e1f3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2784,7 +2784,11 @@ Other minor changes foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs ``` - + +* Added new function to `Data.List.Properties` + ```agda + take-all : {a : Level} {A : Set a} (k : ℕ) (l : List A) → (k ≥ length l) → take k l ≡ l + ``` NonZero/Positive/Negative changes --------------------------------- From 33ffbc728ab05d3c33e563e4661e35327a9cb390 Mon Sep 17 00:00:00 2001 From: Sofia-Insa Date: Thu, 15 Jun 2023 10:57:59 -0400 Subject: [PATCH 3/7] rewrrite syntaxe of of Data.List.Prperties --- src/Data/List/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index f45564d6ab..14bfaba204 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -759,10 +759,10 @@ length-take (suc n) [] = refl length-take (suc n) (x ∷ xs) = cong suc (length-take n xs) -- If you take at least as many elements from a list as it has, you get the whole list. -take-all : {a : Level} {A : Set a} (k : ℕ) (l : List A) → (k ≥ length l) → take k l ≡ l -take-all ℕ.zero [] _ = refl +take-all :(n : ℕ) (l : List A) → (n ≥ length l) → take n l ≡ l +take-all zero [] _ = refl take-all (suc _) [] _ = refl -take-all (suc k) (x ∷ l) (s≤s pf) = cong (x ∷_) (take-all k l pf) +take-all (suc n) (x ∷ l) (s≤s pf) = cong (x ∷_) (take-all n l pf) ------------------------------------------------------------------------ From 7e0be3850a22fa65a84fc13cc406f300021cc0cc Mon Sep 17 00:00:00 2001 From: Sofia-Insa Date: Thu, 15 Jun 2023 11:07:29 -0400 Subject: [PATCH 4/7] rewritte syntaxe of take-all from Data.List.Properties --- src/Data/List/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 14bfaba204..8f2f4d340d 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -759,10 +759,10 @@ length-take (suc n) [] = refl length-take (suc n) (x ∷ xs) = cong suc (length-take n xs) -- If you take at least as many elements from a list as it has, you get the whole list. -take-all :(n : ℕ) (l : List A) → (n ≥ length l) → take n l ≡ l +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 ∷ l) (s≤s pf) = cong (x ∷_) (take-all n l pf) +take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf) ------------------------------------------------------------------------ From 04bb2ba53a9fbce8c2f277a3d3fc7aae40340870 Mon Sep 17 00:00:00 2001 From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com> Date: Thu, 15 Jun 2023 11:16:01 -0400 Subject: [PATCH 5/7] Update Properties.agda Syntaxe of `take-all` adjusted --- 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 8f2f4d340d..39597bf87a 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -759,7 +759,7 @@ length-take (suc n) [] = refl length-take (suc n) (x ∷ xs) = cong suc (length-take n xs) -- 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) From f4b369254c344bbc1e8ee4f2efe49a75582bff25 Mon Sep 17 00:00:00 2001 From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com> Date: Thu, 15 Jun 2023 11:56:28 -0400 Subject: [PATCH 6/7] Update CHANGELOG.md declaration of `take-al` to the section **Other minor changes** / Add new proofs in `Data.List.Properties` --- CHANGELOG.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bbec36e1f3..422cc07412 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2053,6 +2053,8 @@ Other minor changes length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length + + take-all : n ≥ length l → take n xs ≡ xs ``` * Added new patterns and definitions to `Data.Nat.Base`: @@ -2784,11 +2786,7 @@ Other minor changes foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs ``` - -* Added new function to `Data.List.Properties` - ```agda - take-all : {a : Level} {A : Set a} (k : ℕ) (l : List A) → (k ≥ length l) → take k l ≡ l - ``` + NonZero/Positive/Negative changes --------------------------------- From 25b26da04dacf19bf633ef32607b9b8143ac4c80 Mon Sep 17 00:00:00 2001 From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com> Date: Mon, 19 Jun 2023 17:36:39 -0400 Subject: [PATCH 7/7] Update CHANGELOG.md error l instead of l fixed --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a826da3376..28aa64402f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2083,7 +2083,7 @@ Other minor changes length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length - take-all : n ≥ length l → take n xs ≡ xs + take-all : n ≥ length xs → take n xs ≡ xs take-[] : ∀ m → take m [] ≡ [] drop-[] : ∀ m → drop m [] ≡ [] ```