From c7f1ef39178075271b929d72a51b549eec722afe Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Sun, 14 Nov 2021 14:19:24 +0100 Subject: [PATCH 1/4] associativity for vectors --- src/Data/Vec/Relation/Binary/Equality/Setoid.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda index bb40023d2e..1a3d921d3e 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda @@ -68,6 +68,11 @@ open PW public using (++⁺ ; ++⁻ ; ++ˡ⁻; ++ʳ⁻) ++-identityʳ [] = [] ++-identityʳ (x ∷ xs) = refl ∷ ++-identityʳ xs +++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) + → (zs : Vec A k) → (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) +++-assoc [] ys zs = ≋-refl +++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs + map-++-commute : ∀ {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 From 0c530664386905272dfb434aa1c6ce1f31da8b17 Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Sun, 14 Nov 2021 15:35:49 +0100 Subject: [PATCH 2/4] improving style of associativity for vectors --- src/Data/Vec/Relation/Binary/Equality/Setoid.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda index 1a3d921d3e..50ea8a5b61 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda @@ -68,8 +68,8 @@ open PW public using (++⁺ ; ++⁻ ; ++ˡ⁻; ++ʳ⁻) ++-identityʳ [] = [] ++-identityʳ (x ∷ xs) = refl ∷ ++-identityʳ xs -++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) - → (zs : Vec A k) → (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) +++-assoc : ∀ {n m k} (xs : Vec A n) (ys : Vec A m) (zs : Vec A k) → + (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) ++-assoc [] ys zs = ≋-refl ++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs From bdc233baf13b7a81b96c2d256381083fc8b6b444 Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Sun, 14 Nov 2021 15:41:46 +0100 Subject: [PATCH 3/4] + associativity for vectors in CHANGELOG.md --- CHANGELOG.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b585690f4..4d4c7a30c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -716,6 +716,15 @@ Other minor changes → dsubst₂ C p q (f x₁ y₁) ≡ f x₂ y₂ ``` +* Added vector associativity proof to + `Data/Vec/Relation/Binary/Equality/Setoid.agda`: + ``` + ++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) + → (zs : Vec A k) → (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) + ++-assoc [] ys zs = ≋-refl + ++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs + ``` + NonZero/Positive/Negative changes --------------------------------- From c37059d79de2b68e879e11acd28e683cc19cd1ac Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Sun, 14 Nov 2021 16:56:38 +0100 Subject: [PATCH 4/4] - implementaion for vect. concat. from changelog --- CHANGELOG.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4d4c7a30c8..180efd363f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -721,8 +721,6 @@ Other minor changes ``` ++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) → (zs : Vec A k) → (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) - ++-assoc [] ys zs = ≋-refl - ++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs ``` NonZero/Positive/Negative changes