From 842a6596da9d7649701e7c806321428cdd546d12 Mon Sep 17 00:00:00 2001 From: shuhung Date: Tue, 12 Sep 2023 02:04:19 -0500 Subject: [PATCH] =?UTF-8?q?Add=20some=20`=5F=E2=88=B7=CA=B3=5F`=20properti?= =?UTF-8?q?es=20to=20`Data.Vec.Properties`=20(#2041)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 11 +++++++++++ src/Data/List/Properties.agda | 16 +++++++++++----- src/Data/Vec/Base.agda | 8 ++++---- src/Data/Vec/Properties.agda | 33 ++++++++++++++++++++++++++++++++- 4 files changed, 58 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5121e27af9..599b64fcef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -864,6 +864,9 @@ Non-backwards compatible changes * In `Data.Sum.Base` the definitions `fromDec` and `toDec` have been moved to `Data.Sum`. +* In `Data.Vec.Base`: the definitions `init` and `last` have been changed from the `initLast` + view-derived implementation to direct recursive definitions. + * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions: * `cycle` * `interleave⁺` @@ -1253,6 +1256,8 @@ Deprecated names zipWith-identityˡ ↦ zipWith-zeroˡ zipWith-identityʳ ↦ zipWith-zeroʳ + ʳ++-++ ↦ ++-ʳ++ + take++drop ↦ take++drop≡id ``` @@ -2658,6 +2663,12 @@ Other minor changes ∷ʳ-injectiveˡ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys ∷ʳ-injectiveʳ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y + unfold-∷ʳ : cast eq (xs ∷ʳ x) ≡ xs ++ [ x ] + init-∷ʳ : init (xs ∷ʳ x) ≡ xs + last-∷ʳ : last (xs ∷ʳ x) ≡ x + cast-∷ʳ : cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x + ++-∷ʳ : cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z) + reverse-∷ : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x reverse-involutive : Involutive _≡_ reverse reverse-reverse : reverse xs ≡ ys → reverse ys ≡ xs diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 9e86d12436..eb403f8b91 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -993,11 +993,11 @@ module _ {P : Pred A p} (P? : Decidable P) where -- Reverse-append of append is reverse-append after reverse-append. -ʳ++-++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs -ʳ++-++ [] = refl -ʳ++-++ (x ∷ xs) {ys} {zs} = begin +++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs +++-ʳ++ [] = refl +++-ʳ++ (x ∷ xs) {ys} {zs} = begin (x ∷ xs ++ ys) ʳ++ zs ≡⟨⟩ - (xs ++ ys) ʳ++ x ∷ zs ≡⟨ ʳ++-++ xs ⟩ + (xs ++ ys) ʳ++ x ∷ zs ≡⟨ ++-ʳ++ xs ⟩ ys ʳ++ xs ʳ++ x ∷ zs ≡⟨⟩ ys ʳ++ (x ∷ xs) ʳ++ zs ∎ @@ -1073,7 +1073,7 @@ reverse-++ : (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs reverse-++ xs ys = begin reverse (xs ++ ys) ≡⟨⟩ - (xs ++ ys) ʳ++ [] ≡⟨ ʳ++-++ xs ⟩ + (xs ++ ys) ʳ++ [] ≡⟨ ++-ʳ++ xs ⟩ ys ʳ++ xs ʳ++ [] ≡⟨⟩ ys ʳ++ reverse xs ≡⟨ ʳ++-defn ys ⟩ reverse ys ++ reverse xs ∎ @@ -1213,6 +1213,12 @@ zipWith-identityʳ = zipWith-zeroʳ Please use zipWith-zeroʳ instead." #-} +ʳ++-++ = ++-ʳ++ +{-# WARNING_ON_USAGE ʳ++-++ +"Warning: ʳ++-++ was deprecated in v2.0. +Please use ++-ʳ++ instead." +#-} + take++drop = take++drop≡id {-# WARNING_ON_USAGE take++drop "Warning: take++drop was deprecated in v2.0. diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 9f6d86b792..0bf095eaa1 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -345,12 +345,12 @@ initLast {n = suc n} (x ∷ xs) with initLast xs ... | (ys , y , refl) = (x ∷ ys , y , refl) init : Vec A (1 + n) → Vec A n -init xs with initLast xs -... | (ys , y , refl) = ys +init {n = zero} (x ∷ _) = [] +init {n = suc n} (x ∷ xs) = x ∷ init xs last : Vec A (1 + n) → A -last xs with initLast xs -... | (ys , y , refl) = y +last {n = zero} (x ∷ _) = x +last {n = suc n} (_ ∷ xs) = last xs ------------------------------------------------------------------------ -- Other operations diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 56a2001f1e..b6c1f165be 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -399,7 +399,7 @@ cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs) subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs subst-is-cast refl xs = sym (cast-is-id refl xs) -cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) → +cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) → cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs cast-trans {m = zero} {n = zero} {o = zero} eq₁ eq₂ [] = refl cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) = @@ -864,6 +864,12 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl ( ------------------------------------------------------------------------ -- _∷ʳ_ +-- snoc is snoc + +unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ] +unfold-∷ʳ eq x [] = refl +unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs) + ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y ∷ʳ-injective [] [] refl = (refl , refl) ∷ʳ-injective (x ∷ xs) (y ∷ ys) eq with ∷-injective eq @@ -885,12 +891,37 @@ foldr-∷ʳ : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e} y (ys : Vec A n) → foldr-∷ʳ B f y [] = refl foldr-∷ʳ B f y (x ∷ xs) = cong (f x) (foldr-∷ʳ B f y xs) +-- init, last and _∷ʳ_ + +init-∷ʳ : ∀ x (xs : Vec A n) → init (xs ∷ʳ x) ≡ xs +init-∷ʳ x [] = refl +init-∷ʳ x (y ∷ xs) = cong (y ∷_) (init-∷ʳ x xs) + +last-∷ʳ : ∀ x (xs : Vec A n) → last (xs ∷ʳ x) ≡ x +last-∷ʳ x [] = refl +last-∷ʳ x (y ∷ xs) = last-∷ʳ x xs + -- map and _∷ʳ_ map-∷ʳ : ∀ (f : A → B) x (xs : Vec A n) → map f (xs ∷ʳ x) ≡ map f xs ∷ʳ f x map-∷ʳ f x [] = refl map-∷ʳ f x (y ∷ xs) = cong (f y ∷_) (map-∷ʳ f x xs) +-- cast and _∷ʳ_ + +cast-∷ʳ : ∀ .(eq : suc n ≡ suc m) x (xs : Vec A n) → + cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x +cast-∷ʳ {m = zero} eq x [] = refl +cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq) x xs) + +-- _++_ and _∷ʳ_ + +++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) → + cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z) +++-∷ʳ {m = zero} eq z [] [] = refl +++-∷ʳ {m = zero} eq z [] (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys) +++-∷ʳ {m = suc m} eq z (x ∷ xs) ys = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys) + ------------------------------------------------------------------------ -- reverse