From d920db76aacb1b840652790ecb7c725d078b7324 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 4 Dec 2021 10:28:12 -0800 Subject: [PATCH 1/7] Add 'truncate' and 'pad' to Data.Vec.Base --- src/Data/Vec/Base.agda | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 9fa2858cad..d777ff64d2 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -8,7 +8,7 @@ module Data.Vec.Base where -open import Data.Bool.Base +open import Data.Bool.Base using (Bool; true; false) open import Data.Nat.Base open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List using (List) @@ -266,6 +266,19 @@ split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs) uncons : ∀ {n} → Vec A (suc n) → A × Vec A n uncons (x ∷ xs) = x , xs +------------------------------------------------------------------------ +-- Operations involving ≤ + +-- Take the first 'm' elements of a vector. +truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m +truncate z≤n _ = [] +truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs) + +-- Pad out a vector with extra elements. +pad : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n +pad z≤n a xs = replicate a +pad (s≤s le) a (x ∷ xs) = x ∷ pad le a xs + ------------------------------------------------------------------------ -- Operations for converting between lists From 072a4fa31173dfa870b788d57b6a4a7c6bf501e2 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 4 Dec 2021 10:52:44 -0800 Subject: [PATCH 2/7] Add properties of 'pad' and 'truncate' --- src/Data/Vec/Properties.agda | 40 ++++++++++++++++++++++++++++++++++-- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index ff27cea065..69dcc5e126 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -14,7 +14,8 @@ open import Data.Empty using (⊥-elim) open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_) open import Data.List.Base as List using (List) open import Data.Nat.Base -open import Data.Nat.Properties using (+-assoc; ≤-step) +open import Data.Nat.Properties + using (+-assoc; ≤-step; ≤-refl; ≤-trans) open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -25,7 +26,7 @@ open import Function.Inverse using (_↔_; inverse) open import Level using (Level) open import Relation.Binary as B hiding (Decidable) open import Relation.Binary.PropositionalEquality as P - using (_≡_; _≢_; refl; _≗_; cong₂) + using (_≡_; _≢_; refl; _≗_; cong; cong₂) open P.≡-Reasoning open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary using (Dec; does; yes; no) @@ -155,6 +156,41 @@ take-drop-id (suc m) (x ∷ xs) = begin x ∷ xs ∎ +-------------------------------------------------------------------------------- +-- truncate + +truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs +truncate-refl [] = refl +truncate-refl (x ∷ xs) = cong (x ∷_) (truncate-refl xs) + +truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) → + truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs) +truncate-trans z≤n le₂ xs = refl +truncate-trans (s≤s le₁) (s≤s le₂) (x ∷ xs) = cong (x ∷_) (truncate-trans le₁ le₂ xs) + +-------------------------------------------------------------------------------- +-- pad + +pad-refl : ∀ {n} → (a : A) → (xs : Vec A n) → pad ≤-refl a xs ≡ xs +pad-refl a [] = refl +pad-refl a (x ∷ xs) = cong (x ∷_) (pad-refl a xs) + +pad-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ pad le a (replicate a) +pad-replicate z≤n a = refl +pad-replicate (s≤s le) a = cong (a ∷_) (pad-replicate le a) + +pad-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → + pad (≤-trans le₁ le₂) a xs ≡ pad le₂ a (pad le₁ a xs) +pad-trans z≤n le₂ a [] = pad-replicate le₂ a +pad-trans (s≤s le₁) (s≤s le₂) a (x ∷ xs) = cong (x ∷_) (pad-trans le₁ le₂ a xs) + +-------------------------------------------------------------------------------- +-- truncate and pad together + +truncate-pad-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (pad le a xs) ≡ xs +truncate-pad-id z≤n a [] = refl +truncate-pad-id (s≤s le) a (x ∷ xs) = cong (x ∷_) (truncate-pad-id le a xs) + ------------------------------------------------------------------------ -- lookup From 384ab7f953969dee315d83e07e615140c83c7cdb Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 4 Dec 2021 10:58:14 -0800 Subject: [PATCH 3/7] update CHANGELOG --- CHANGELOG.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 225b281aa6..fdfb0e9759 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -696,6 +696,8 @@ Other minor changes ```agda diagonal : ∀ {n} → Vec (Vec A n) n → Vec A n DiagonalBind._>>=_ : ∀ {n} → Vec A n → (A → Vec B n) → Vec B n + truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m + pad : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n ``` * Added new instance in `Data.Vec.Categorical`: @@ -708,8 +710,16 @@ Other minor changes map-const : ∀ {n} (xs : Vec A n) (x : B) → map {n = n} (const x) xs ≡ replicate x map-⊛ : ∀ {n} (f : A → B → C) (g : A → B) (xs : Vec A n) → (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs ⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) → (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs) + pad-refl : ∀ {n} → (a : A) → (xs : Vec A n) → pad ≤-refl a xs ≡ xs + pad-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ pad le a (replicate a) + pad-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → + pad (≤-trans le₁ le₂) a xs ≡ pad le₂ a (pad le₁ a xs) transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs []≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y) + + truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs + truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) → + truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs) ``` * Added new proofs in `Function.Construct.Symmetry`: From 65d62ec5840e52e38464b8e071f8a174b9850d12 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 4 Dec 2021 11:21:20 -0800 Subject: [PATCH 4/7] Rename `pad` to `padRight` for consistency with `Data.Vec.Bounded` --- CHANGELOG.md | 9 +++++---- src/Data/Vec/Base.agda | 6 +++--- src/Data/Vec/Properties.agda | 28 ++++++++++++++-------------- 3 files changed, 22 insertions(+), 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fdfb0e9759..350f185c3b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -710,16 +710,17 @@ Other minor changes map-const : ∀ {n} (xs : Vec A n) (x : B) → map {n = n} (const x) xs ≡ replicate x map-⊛ : ∀ {n} (f : A → B → C) (g : A → B) (xs : Vec A n) → (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs ⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) → (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs) - pad-refl : ∀ {n} → (a : A) → (xs : Vec A n) → pad ≤-refl a xs ≡ xs - pad-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ pad le a (replicate a) - pad-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → - pad (≤-trans le₁ le₂) a xs ≡ pad le₂ a (pad le₁ a xs) + padRight-refl : ∀ {n} → (a : A) → (xs : Vec A n) → padRight ≤-refl a xs ≡ xs + padRight-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ padRight le a (replicate a) + padRight-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → + padRight (≤-trans le₁ le₂) a xs ≡ padRight le₂ a (padRight le₁ a xs) transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs []≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y) truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) → truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs) + truncate-padRight-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (padRight le a xs) ≡ xs ``` * Added new proofs in `Function.Construct.Symmetry`: diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index d777ff64d2..e230f6e793 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -275,9 +275,9 @@ truncate z≤n _ = [] truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs) -- Pad out a vector with extra elements. -pad : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n -pad z≤n a xs = replicate a -pad (s≤s le) a (x ∷ xs) = x ∷ pad le a xs +padRight : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n +padRight z≤n a xs = replicate a +padRight (s≤s le) a (x ∷ xs) = x ∷ padRight le a xs ------------------------------------------------------------------------ -- Operations for converting between lists diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 69dcc5e126..7969d54351 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -171,25 +171,25 @@ truncate-trans (s≤s le₁) (s≤s le₂) (x ∷ xs) = cong (x ∷_) (truncate- -------------------------------------------------------------------------------- -- pad -pad-refl : ∀ {n} → (a : A) → (xs : Vec A n) → pad ≤-refl a xs ≡ xs -pad-refl a [] = refl -pad-refl a (x ∷ xs) = cong (x ∷_) (pad-refl a xs) +padRight-refl : ∀ {n} → (a : A) → (xs : Vec A n) → padRight ≤-refl a xs ≡ xs +padRight-refl a [] = refl +padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs) -pad-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ pad le a (replicate a) -pad-replicate z≤n a = refl -pad-replicate (s≤s le) a = cong (a ∷_) (pad-replicate le a) +padRight-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ padRight le a (replicate a) +padRight-replicate z≤n a = refl +padRight-replicate (s≤s le) a = cong (a ∷_) (padRight-replicate le a) -pad-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → - pad (≤-trans le₁ le₂) a xs ≡ pad le₂ a (pad le₁ a xs) -pad-trans z≤n le₂ a [] = pad-replicate le₂ a -pad-trans (s≤s le₁) (s≤s le₂) a (x ∷ xs) = cong (x ∷_) (pad-trans le₁ le₂ a xs) +padRight-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → + padRight (≤-trans le₁ le₂) a xs ≡ padRight le₂ a (padRight le₁ a xs) +padRight-trans z≤n le₂ a [] = padRight-replicate le₂ a +padRight-trans (s≤s le₁) (s≤s le₂) a (x ∷ xs) = cong (x ∷_) (padRight-trans le₁ le₂ a xs) -------------------------------------------------------------------------------- --- truncate and pad together +-- truncate and padRight together -truncate-pad-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (pad le a xs) ≡ xs -truncate-pad-id z≤n a [] = refl -truncate-pad-id (s≤s le) a (x ∷ xs) = cong (x ∷_) (truncate-pad-id le a xs) +truncate-padRight-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (padRight le a xs) ≡ xs +truncate-padRight-id z≤n a [] = refl +truncate-padRight-id (s≤s le) a (x ∷ xs) = cong (x ∷_) (truncate-padRight-id le a xs) ------------------------------------------------------------------------ -- lookup From 33e66bff11b44b679f540608621889019fbfaa36 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 16 Feb 2022 18:16:01 +0000 Subject: [PATCH 5/7] [ cosmetic ] following Matthew's review --- CHANGELOG.md | 36 +++++++++++++++--------------- src/Data/Vec/Properties.agda | 43 ++++++++++++++++++------------------ 2 files changed, 40 insertions(+), 39 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 350f185c3b..c9eab73afd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,7 +31,7 @@ Bug-fixes meta-variable whenever this module was explicitly parameterised. This has been fixed. -* Add module `Algebra.Module` that re-exports the contents of +* Add module `Algebra.Module` that re-exports the contents of `Algebra.Module.(Definitions/Structures/Bundles)` Non-backwards compatible changes @@ -76,7 +76,7 @@ Non-backwards compatible changes ### Refactoring of algebraic lattice hierarchy -* In order to improve modularity and consistency with `Relation.Binary.Lattice`, +* In order to improve modularity and consistency with `Relation.Binary.Lattice`, the structures & bundles for `Semilattice`, `Lattice`, `DistributiveLattice` & `BooleanAlgebra` have been moved out of the `Algebra` modules and into their own hierarchy in `Algebra.Lattice`. @@ -86,7 +86,7 @@ Non-backwards compatible changes `Algebra.Lattice.Properties.Semilattice` or `Algebra.Lattice.Morphism.Lattice`). See the `Deprecated modules` section below for full details. -* Changed definition of `IsDistributiveLattice` and `IsBooleanAlgebra` so that they are +* Changed definition of `IsDistributiveLattice` and `IsBooleanAlgebra` so that they are no longer right-biased which hinders compositionality. More concretely, `IsDistributiveLattice` now has fields: ```agda @@ -269,7 +269,7 @@ Non-backwards compatible changes in order to keep another new definition of `_>>=_`, located in `DiagonalBind` which is also a submodule of `Data.Vec.Base`. -* The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer +* The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` directly to use them. @@ -500,7 +500,7 @@ New modules Function.Properties.Surjection ``` -* In order to improve modularity, the contents of `Relation.Binary.Lattice` has been +* In order to improve modularity, the contents of `Relation.Binary.Lattice` has been split out into the standard: ``` Relation.Binary.Lattice.Definitions @@ -707,20 +707,20 @@ Other minor changes * Added new proofs in `Data.Vec.Properties`: ```agda - map-const : ∀ {n} (xs : Vec A n) (x : B) → map {n = n} (const x) xs ≡ replicate x - map-⊛ : ∀ {n} (f : A → B → C) (g : A → B) (xs : Vec A n) → (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs - ⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) → (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs) - padRight-refl : ∀ {n} → (a : A) → (xs : Vec A n) → padRight ≤-refl a xs ≡ xs - padRight-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ padRight le a (replicate a) - padRight-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → - padRight (≤-trans le₁ le₂) a xs ≡ padRight le₂ a (padRight le₁ a xs) + map-const : map (const x) xs ≡ replicate x + map-⊛ : (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs + ⊛-is->>= : (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs) + + padRight-refl : padRight ≤-refl a xs ≡ xs + padRight-replicate : replicate a ≡ padRight le a (replicate a) + padRight-trans : padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs) + transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs []≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y) - truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs - truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) → - truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs) - truncate-padRight-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (padRight le a xs) ≡ xs + truncate-refl : truncate ≤-refl xs ≡ xs + truncate-trans : truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs) + truncate-padRight : truncate m≤n (padRight m≤n a xs) ≡ xs ``` * Added new proofs in `Function.Construct.Symmetry`: @@ -844,10 +844,10 @@ Other minor changes → dsubst₂ C p q (f x₁ y₁) ≡ f x₂ y₂ ``` -* Added vector associativity proof to +* Added vector associativity proof to `Data/Vec/Relation/Binary/Equality/Setoid.agda`: ``` - ++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) + ++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) → (zs : Vec A k) → (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) ``` diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 7969d54351..1072019573 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -78,8 +78,8 @@ unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x unfold-take n x xs with splitAt n xs unfold-take n x .(xs ++ ys) | xs , ys , refl = refl -take-distr-zipWith : ∀ {m n} → (f : A → B → C) → - (xs : Vec A (m + n)) → (ys : Vec B (m + n)) → +take-distr-zipWith : ∀ {m n} (f : A → B → C) + (xs : Vec A (m + n)) (ys : Vec B (m + n)) → take m (zipWith f xs ys) ≡ zipWith f (take m xs) (take m ys) take-distr-zipWith {m = zero} f xs ys = refl take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin @@ -96,7 +96,7 @@ take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin zipWith f (take (suc m) (x ∷ xs)) (take (suc m) (y ∷ ys)) ∎ -take-distr-map : ∀ {n} → (f : A → B) → (m : ℕ) → (xs : Vec A (m + n)) → +take-distr-map : ∀ {n} (f : A → B) (m : ℕ) (xs : Vec A (m + n)) → take m (map f xs) ≡ map f (take m xs) take-distr-map f zero xs = refl take-distr-map f (suc m) (x ∷ xs) = @@ -115,8 +115,8 @@ unfold-drop : ∀ n {m} x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ d unfold-drop n x xs with splitAt n xs unfold-drop n x .(xs ++ ys) | xs , ys , refl = refl -drop-distr-zipWith : ∀ {m n} → (f : A → B → C) → - (x : Vec A (m + n)) → (y : Vec B (m + n)) → +drop-distr-zipWith : ∀ {m n} (f : A → B → C) + (x : Vec A (m + n)) (y : Vec B (m + n)) → drop m (zipWith f x y) ≡ zipWith f (drop m x) (drop m y) drop-distr-zipWith {m = zero} f xs ys = refl drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin @@ -131,7 +131,7 @@ drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin zipWith f (drop (suc m) (x ∷ xs)) (drop (suc m) (y ∷ ys)) ∎ -drop-distr-map : ∀ {n} → (f : A → B) → (m : ℕ) → (x : Vec A (m + n)) → +drop-distr-map : ∀ {n} (f : A → B) (m : ℕ) (x : Vec A (m + n)) → drop m (map f x) ≡ map f (drop m x) drop-distr-map f zero x = refl drop-distr-map f (suc m) (x ∷ xs) = begin @@ -144,7 +144,7 @@ drop-distr-map f (suc m) (x ∷ xs) = begin ------------------------------------------------------------------------ -- take and drop together -take-drop-id : ∀ {n} → (m : ℕ) → (x : Vec A (m + n)) → take m x ++ drop m x ≡ x +take-drop-id : ∀ {n} (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x take-drop-id zero x = refl take-drop-id (suc m) (x ∷ xs) = begin take (suc m) (x ∷ xs) ++ drop (suc m) (x ∷ xs) @@ -159,37 +159,38 @@ take-drop-id (suc m) (x ∷ xs) = begin -------------------------------------------------------------------------------- -- truncate -truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs +truncate-refl : ∀ {n} (xs : Vec A n) → truncate ≤-refl xs ≡ xs truncate-refl [] = refl truncate-refl (x ∷ xs) = cong (x ∷_) (truncate-refl xs) -truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) → - truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs) -truncate-trans z≤n le₂ xs = refl -truncate-trans (s≤s le₁) (s≤s le₂) (x ∷ xs) = cong (x ∷_) (truncate-trans le₁ le₂ xs) +truncate-trans : ∀ {m n p} (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) → + truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs) +truncate-trans z≤n n≤p xs = refl +truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) -------------------------------------------------------------------------------- -- pad -padRight-refl : ∀ {n} → (a : A) → (xs : Vec A n) → padRight ≤-refl a xs ≡ xs +padRight-refl : ∀ {n} (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs padRight-refl a [] = refl padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs) -padRight-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ padRight le a (replicate a) +padRight-replicate : ∀ {m n} (le : m ≤ n) (a : A) → replicate a ≡ padRight le a (replicate a) padRight-replicate z≤n a = refl padRight-replicate (s≤s le) a = cong (a ∷_) (padRight-replicate le a) -padRight-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) → - padRight (≤-trans le₁ le₂) a xs ≡ padRight le₂ a (padRight le₁ a xs) -padRight-trans z≤n le₂ a [] = padRight-replicate le₂ a -padRight-trans (s≤s le₁) (s≤s le₂) a (x ∷ xs) = cong (x ∷_) (padRight-trans le₁ le₂ a xs) +padRight-trans : ∀ {m n p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) → + padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs) +padRight-trans z≤n n≤p a [] = padRight-replicate n≤p a +padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs) -------------------------------------------------------------------------------- -- truncate and padRight together -truncate-padRight-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (padRight le a xs) ≡ xs -truncate-padRight-id z≤n a [] = refl -truncate-padRight-id (s≤s le) a (x ∷ xs) = cong (x ∷_) (truncate-padRight-id le a xs) +truncate-padRight : ∀ {m n} (m≤n : m ≤ n) (a : A) (xs : Vec A m) → + truncate m≤n (padRight m≤n a xs) ≡ xs +truncate-padRight z≤n a [] = refl +truncate-padRight (s≤s m≤n) a (x ∷ xs) = cong (x ∷_) (truncate-padRight m≤n a xs) ------------------------------------------------------------------------ -- lookup From 43c61b10383d6ec966c4cb2e853d6807bb38756d Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 16 Feb 2022 18:36:08 +0000 Subject: [PATCH 6/7] [ fix ] by default p is a level name --- src/Data/Vec/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 6df8d26716..73386d9a8c 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -160,7 +160,7 @@ truncate-refl : (xs : Vec A n) → truncate ≤-refl xs ≡ xs truncate-refl [] = refl truncate-refl (x ∷ xs) = cong (x ∷_) (truncate-refl xs) -truncate-trans : (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) → +truncate-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) → truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs) truncate-trans z≤n n≤p xs = refl truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) @@ -176,7 +176,7 @@ padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate a ≡ padRight m≤ padRight-replicate z≤n a = refl padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a) -padRight-trans : (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) → +padRight-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) → padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs) padRight-trans z≤n n≤p a [] = padRight-replicate n≤p a padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs) From 0e5e88f85d49c9d9d2e88ee775a5d8175c342e1a Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 16 Feb 2022 19:28:58 +0000 Subject: [PATCH 7/7] [ changelog ] drop duplicated entries --- CHANGELOG.md | 42 ------------------------------------------ 1 file changed, 42 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6928700ae6..915237c028 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1412,48 +1412,6 @@ Other minor changes isFailure : ExitCode → Bool ``` -* Added new functions in `Data.List.Relation.Unary.All`: - ``` - decide : Π[ P ∪ Q ] → Π[ All P ∪ Any Q ] - ``` - -* Added new functions in `Data.List.Fresh.Relation.Unary.All`: - ``` - decide : Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ] - ``` - -* Added new functions in `Data.Vec.Relation.Unary.All`: - ``` - decide : Π[ P ∪ Q ] → Π[ All P ∪ Any Q ] - ``` - -* Added new operations in - `Relation.Binary.PropositionalEquality.Properties`: - ``` - J : {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b) - {y : A} (p : x ≡ y) → B x refl → B y p - dcong : ∀ {A : Set a} {B : A → Set b} (f : (x : A) → B x) {x y} - → (p : x ≡ y) → subst B p (f x) ≡ f y - dcong₂ : ∀ {A : Set a} {B : A → Set b} {C : Set c} - (f : (x : A) → B x → C) {x₁ x₂ y₁ y₂} - → (p : x₁ ≡ x₂) → subst B p y₁ ≡ y₂ - → f x₁ y₁ ≡ f x₂ y₂ - dsubst₂ : ∀ {A : Set a} {B : A → Set b} (C : (x : A) → B x → Set c) - {x₁ x₂ y₁ y₂} (p : x₁ ≡ x₂) → subst B p y₁ ≡ y₂ - → C x₁ y₁ → C x₂ y₂ - ddcong₂ : ∀ {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} - (f : (x : A) (y : B x) → C x y) {x₁ x₂ y₁ y₂} - (p : x₁ ≡ x₂) (q : subst B p y₁ ≡ y₂) - → 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) - ``` - NonZero/Positive/Negative changes ---------------------------------