Modernise Data.Vec(.Properties) (#1673)

Author: MatthewDaggitt

CHANGELOG.md

@@ -552,6 +552,14 @@ Deprecated names
   idIsFold        ↦ id-is-foldr
   sum-++-commute  ↦ sum-++
   ```
+  and the type of the proof `zipWith-comm` has been generalised from:
+  ```
+  zipWith-comm : ∀ {f : A → A → B} (comm : ∀ x y → f x y ≡ f y x) (xs ys : Vec A n) → zipWith f xs ys ≡ zipWith f ys xs
+  ```
+  to
+  ```
+  zipWith-comm : ∀ {f : A → B → C} {g : B → A → C}  (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs
+  ```
 
 * In `Function.Construct.Composition`:
   ```

src/Data/Vec/Base.agda

@@ -26,6 +26,7 @@ private
     A : Set a
     B : Set b
     C : Set c
+    m n : ℕ
 
 ------------------------------------------------------------------------
 -- Types
@@ -34,121 +35,121 @@ infixr 5 _∷_
 
 data Vec (A : Set a) : ℕ → Set a where
   []  : Vec A zero
-  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
+  _∷_ : ∀ (x : A) (xs : Vec A n) → Vec A (suc n)
 
 infix 4 _[_]=_
 
-data _[_]=_ {A : Set a} : ∀ {n} → Vec A n → Fin n → A → Set a where
-  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
-  there : ∀ {n} {i} {x y} {xs : Vec A n}
-          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x
+data _[_]=_ {A : Set a} : Vec A n → Fin n → A → Set a where
+  here  : ∀     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
+  there : ∀ {i} {x y} {xs : Vec A n}
+    (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x
 
 ------------------------------------------------------------------------
 -- Basic operations
 
-length : ∀ {n} → Vec A n → ℕ
+length : Vec A n → ℕ
 length {n = n} _ = n
 
-head : ∀ {n} → Vec A (1 + n) → A
+head : Vec A (1 + n) → A
 head (x ∷ xs) = x
 
-tail : ∀ {n} → Vec A (1 + n) → Vec A n
+tail : Vec A (1 + n) → Vec A n
 tail (x ∷ xs) = xs
 
-lookup : ∀ {n} → Vec A n → Fin n → A
+lookup : Vec A n → Fin n → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
-insert : ∀ {n} → Vec A n → Fin (suc n) → A → Vec A (suc n)
+insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
 insert xs       zero     v = v ∷ xs
 insert (x ∷ xs) (suc i)  v = x ∷ insert xs i v
 
-remove : ∀ {n} → Vec A (suc n) → Fin (suc n) → Vec A n
+remove : Vec A (suc n) → Fin (suc n) → Vec A n
 remove (_ ∷ xs)     zero     = xs
 remove (x ∷ y ∷ xs) (suc i)  = x ∷ remove (y ∷ xs) i
 
-updateAt : ∀ {n} → Fin n → (A → A) → Vec A n → Vec A n
+updateAt : Fin n → (A → A) → Vec A n → Vec A n
 updateAt zero    f (x ∷ xs) = f x ∷ xs
 updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
 
 -- xs [ i ]%= f  modifies the i-th element of xs according to f
 
 infixl 6 _[_]%=_
 
-_[_]%=_ : ∀ {n} → Vec A n → Fin n → (A → A) → Vec A n
+_[_]%=_ : Vec A n → Fin n → (A → A) → Vec A n
 xs [ i ]%= f = updateAt i f xs
 
 -- xs [ i ]≔ y  overwrites the i-th element of xs with y
 
 infixl 6 _[_]≔_
 
-_[_]≔_ : ∀ {n} → Vec A n → Fin n → A → Vec A n
+_[_]≔_ : Vec A n → Fin n → A → Vec A n
 xs [ i ]≔ y = xs [ i ]%= const y
 
 ------------------------------------------------------------------------
 -- Operations for transforming vectors
 
-map : ∀ {n} → (A → B) → Vec A n → Vec B n
+map : (A → B) → Vec A n → Vec B n
 map f []       = []
 map f (x ∷ xs) = f x ∷ map f xs
 
 -- Concatenation.
 
 infixr 5 _++_
 
-_++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
+_++_ : Vec A m → Vec A n → Vec A (m + n)
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
 
-concat : ∀ {m n} → Vec (Vec A m) n → Vec A (n * m)
+concat : Vec (Vec A m) n → Vec A (n * m)
 concat []         = []
 concat (xs ∷ xss) = xs ++ concat xss
 
 -- Align, Restrict, and Zip.
 
-alignWith : ∀ {m n} → (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n)
+alignWith : (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n)
 alignWith f []         bs       = map (f ∘′ that) bs
 alignWith f as@(_ ∷ _) []       = map (f ∘′ this) as
 alignWith f (a ∷ as)   (b ∷ bs) = f (these a b) ∷ alignWith f as bs
 
-restrictWith : ∀ {m n} → (A → B → C) → Vec A m → Vec B n → Vec C (m ⊓ n)
+restrictWith : (A → B → C) → Vec A m → Vec B n → Vec C (m ⊓ n)
 restrictWith f []       bs       = []
 restrictWith f (_ ∷ _)  []       = []
 restrictWith f (a ∷ as) (b ∷ bs) = f a b ∷ restrictWith f as bs
 
-zipWith : ∀ {n} → (A → B → C) → Vec A n → Vec B n → Vec C n
+zipWith : (A → B → C) → Vec A n → Vec B n → Vec C n
 zipWith f []       []       = []
 zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
 
-unzipWith : ∀ {n} → (A → B × C) → Vec A n → Vec B n × Vec C n
+unzipWith : (A → B × C) → Vec A n → Vec B n × Vec C n
 unzipWith f []       = [] , []
 unzipWith f (a ∷ as) = Prod.zip _∷_ _∷_ (f a) (unzipWith f as)
 
-align : ∀ {m n} → Vec A m → Vec B n → Vec (These A B) (m ⊔ n)
+align : Vec A m → Vec B n → Vec (These A B) (m ⊔ n)
 align = alignWith id
 
-restrict : ∀ {m n} → Vec A m → Vec B n → Vec (A × B) (m ⊓ n)
+restrict : Vec A m → Vec B n → Vec (A × B) (m ⊓ n)
 restrict = restrictWith _,_
 
-zip : ∀ {n} → Vec A n → Vec B n → Vec (A × B) n
+zip : Vec A n → Vec B n → Vec (A × B) n
 zip = zipWith _,_
 
-unzip : ∀ {n} → Vec (A × B) n → Vec A n × Vec B n
+unzip : Vec (A × B) n → Vec A n × Vec B n
 unzip = unzipWith id
 
 -- Interleaving.
 
 infixr 5 _⋎_
 
-_⋎_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m +⋎ n)
+_⋎_ : Vec A m → Vec A n → Vec A (m +⋎ n)
 []       ⋎ ys = ys
 (x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)
 
 -- Pointwise application
 
 infixl 4 _⊛_
 
-_⊛_ : ∀ {n} → Vec (A → B) n → Vec A n → Vec B n
+_⊛_ : Vec (A → B) n → Vec A n → Vec B n
 []       ⊛ []       = []
 (f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)
 
@@ -157,27 +158,27 @@ _⊛_ : ∀ {n} → Vec (A → B) n → Vec A n → Vec B n
 module CartesianBind where
   infixl 1 _>>=_
 
-  _>>=_ : ∀ {m n} → Vec A m → (A → Vec B n) → Vec B (m * n)
+  _>>=_ : Vec A m → (A → Vec B n) → Vec B (m * n)
   xs >>= f = concat (map f xs)
 
 infixl 4 _⊛*_
 
-_⊛*_ : ∀ {m n} → Vec (A → B) m → Vec A n → Vec B (m * n)
+_⊛*_ : Vec (A → B) m → Vec A n → Vec B (m * n)
 fs ⊛* xs = fs CartesianBind.>>= λ f → map f xs
 
-allPairs : ∀ {m n} → Vec A m → Vec B n → Vec (A × B) (m * n)
+allPairs : Vec A m → Vec B n → Vec (A × B) (m * n)
 allPairs xs ys = map _,_ xs ⊛* ys
 
 -- Diagonal
 
-diagonal : ∀ {n} → Vec (Vec A n) n → Vec A n
+diagonal : Vec (Vec A n) n → Vec A n
 diagonal [] = []
 diagonal (xs ∷ xss) = head xs ∷ diagonal (map tail xss)
 
 module DiagonalBind where
   infixl 1 _>>=_
 
-  _>>=_ : ∀ {n} → Vec A n → (A → Vec B n) → Vec B n
+  _>>=_ : Vec A n → (A → Vec B n) → Vec B n
   xs >>= f = diagonal (map f xs)
 
 ------------------------------------------------------------------------
@@ -190,43 +191,37 @@ module _ (A : Set a) (B : ℕ → Set b) where
   FoldrOp = ∀ {n} → A → B n → B (suc n)
   FoldlOp = ∀ {n} → B n → A → B (suc n)
 
-foldr : ∀ (B : ℕ → Set b) {m} →
-        FoldrOp A B →
-        B zero →
-        Vec A m → B m
-foldr B _⊕_ n []       = n
-foldr B _⊕_ n (x ∷ xs) = x ⊕ foldr B _⊕_ n xs
+foldr : ∀ (B : ℕ → Set b) → FoldrOp A B → B zero → Vec A n → B n
+foldr B _⊕_ e []       = e
+foldr B _⊕_ e (x ∷ xs) = x ⊕ foldr B _⊕_ e xs
 
-foldl : ∀ (B : ℕ → Set b) {m} →
-        FoldlOp A B →
-        B zero →
-        Vec A m → B m
-foldl B _⊕_ n []       = n
-foldl B _⊕_ n (x ∷ xs) = foldl (B ∘ suc) _⊕_ (n ⊕ x) xs
+foldl : ∀ (B : ℕ → Set b) → FoldlOp A B → B zero → Vec A n → B n
+foldl B _⊕_ e []       = e
+foldl B _⊕_ e (x ∷ xs) = foldl (B ∘ suc) _⊕_ (e ⊕ x) xs
 
 -- Non-dependent folds
 
-foldr′ : ∀ {n} → (A → B → B) → B → Vec A n → B
-foldr′ _⊕_ = foldr _ λ {n} → _⊕_
+foldr′ : (A → B → B) → B → Vec A n → B
+foldr′ _⊕_ = foldr _ _⊕_
 
-foldl′ : ∀ {n} → (B → A → B) → B → Vec A n → B
-foldl′ _⊕_ = foldl _ λ {n} → _⊕_
+foldl′ : (B → A → B) → B → Vec A n → B
+foldl′ _⊕_ = foldl _ _⊕_
 
 -- Non-empty folds
 
-foldr₁ : ∀ {n} → (A → A → A) → Vec A (suc n) → A
+foldr₁ : (A → A → A) → Vec A (suc n) → A
 foldr₁ _⊕_ (x ∷ [])     = x
 foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)
 
-foldl₁ : ∀ {n} → (A → A → A) → Vec A (suc n) → A
+foldl₁ : (A → A → A) → Vec A (suc n) → A
 foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs
 
 -- Special folds
 
-sum : ∀ {n} → Vec ℕ n → ℕ
+sum : Vec ℕ n → ℕ
 sum = foldr _ _+_ 0
 
-count : ∀ {P : Pred A p} → Decidable P → ∀ {n} → Vec A n → ℕ
+count : ∀ {P : Pred A p} → Decidable P → Vec A n → ℕ
 count P? []       = zero
 count P? (x ∷ xs) with does (P? x)
 ... | true  = suc (count P? xs)
@@ -238,11 +233,11 @@ count P? (x ∷ xs) with does (P? x)
 [_] : A → Vec A 1
 [ x ] = x ∷ []
 
-replicate : ∀ {n} → A → Vec A n
+replicate : A → Vec A n
 replicate {n = zero}  x = []
 replicate {n = suc n} x = x ∷ replicate x
 
-tabulate : ∀ {n} → (Fin n → A) → Vec A n
+tabulate : (Fin n → A) → Vec A n
 tabulate {n = zero}  f = []
 tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)
 
@@ -275,18 +270,18 @@ group (suc n) k .(ys ++ zs)         | (ys , zs , refl) with group n k zs
 group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
   ((ys ∷ zss) , refl)
 
-split : ∀ {n} → Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
+split : Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
 split []           = ([]     , [])
 split (x ∷ [])     = (x ∷ [] , [])
 split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)
 
-uncons : ∀ {n} → Vec A (suc n) → A × Vec A n
+uncons : Vec A (suc n) → A × Vec A n
 uncons (x ∷ xs) = x , xs
 
 ------------------------------------------------------------------------
 -- Operations for converting between lists
 
-toList : ∀ {n} → Vec A n → List A
+toList : Vec A n → List A
 toList []       = List.[]
 toList (x ∷ xs) = List._∷_ x (toList xs)
 
@@ -301,42 +296,40 @@ fromList (List._∷_ x xs) = x ∷ fromList xs
 
 infixl 5 _∷ʳ_
 
-_∷ʳ_ : ∀ {n} → Vec A n → A → Vec A (suc n)
+_∷ʳ_ : Vec A n → A → Vec A (suc n)
 []       ∷ʳ y = [ y ]
 (x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)
 
 -- vanilla reverse
 
-reverse : ∀ {n} → Vec A n → Vec A n
-reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
+reverse : Vec A n → Vec A n
+reverse = foldl (Vec _) (λ rev x → x ∷ rev) []
 
 -- reverse-append
 
 infix 5 _ʳ++_
 
-_ʳ++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
-_ʳ++_ {A = A} {n = n} xs ys = foldl ((Vec A) ∘ (_+ n)) (λ rev x → x ∷ rev) ys xs
+_ʳ++_ : Vec A m → Vec A n → Vec A (m + n)
+xs ʳ++ ys = foldl (Vec _ ∘ (_+ _)) (λ rev x → x ∷ rev) ys xs
 
 -- init and last
 
-initLast : ∀ {n} (xs : Vec A (1 + n)) →
-           ∃₂ λ (ys : Vec A n) (y : A) → xs ≡ ys ∷ʳ y
-initLast {n = zero}  (x ∷ [])         = ([] , x , refl)
-initLast {n = suc n} (x ∷ xs)         with initLast xs
-initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | (ys , y , refl) =
-  ((x ∷ ys) , y , refl)
+initLast : ∀ (xs : Vec A (1 + n)) → ∃₂ λ ys y → xs ≡ ys ∷ʳ y
+initLast {n = zero}  (x ∷ []) = ([] , x , refl)
+initLast {n = suc n} (x ∷ xs) with initLast xs
+... | (ys , y , refl) = (x ∷ ys , y , refl)
 
-init : ∀ {n} → Vec A (1 + n) → Vec A n
-init xs         with initLast xs
-init .(ys ∷ʳ y) | (ys , y , refl) = ys
+init : Vec A (1 + n) → Vec A n
+init xs with initLast xs
+... | (ys , y , refl) = ys
 
-last : ∀ {n} → Vec A (1 + n) → A
-last xs         with initLast xs
-last .(ys ∷ʳ y) | (ys , y , refl) = y
+last : Vec A (1 + n) → A
+last xs with initLast xs
+... | (ys , y , refl) = y
 
 ------------------------------------------------------------------------
 -- Other operations
 
-transpose : ∀ {m n} → Vec (Vec A n) m → Vec (Vec A m) n
+transpose : Vec (Vec A n) m → Vec (Vec A m) n
 transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass