    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some Vector-related properties
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Vec.Functional.Properties where

    open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ<; reduce≥;
      _↑ˡ_; _↑ʳ_; punchIn; punchOut)
    open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
    import Data.Nat.Properties as ℕ
    open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
    open import Data.List.Base as List using (List)
    import Data.List.Properties as List
    open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
    open import Data.Vec.Base as Vec using (Vec)
    import Data.Vec.Properties as Vec
    open import Data.Vec.Functional using (Vector; head; tail; updateAt;
      map; _++_; insertAt; removeAt; toVec; fromVec; toList; fromList)
    open import Function.Base using (_∘_; id)
    open import Level using (Level)
    open import Relation.Binary.Definitions using (DecidableEquality; Decidable)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; _≗_; refl; _≢_; cong)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)
    open import Relation.Nullary.Decidable
      using (Dec; does; yes; no; map′; _×-dec_)
    open import Relation.Nullary.Negation using (contradiction)

    import Data.Fin.Properties as Finₚ

    private
      variable
        a b c : Level
        A B C : Set a
        m n : ℕ

    ------------------------------------------------------------------------

    module _ {xs ys : Vector A (suc n)} where

      ∷-cong : head xs ≡ head ys → tail xs ≗ tail ys → xs ≗ ys
      ∷-cong eq _ zero    = eq
      ∷-cong _ eq (suc i) = eq i

      ∷-injective : xs ≗ ys → head xs ≡ head ys × tail xs ≗ tail ys
      ∷-injective eq = eq zero , eq ∘ suc

    ≗-dec : DecidableEquality A → Decidable {A = Vector A n} _≗_
    ≗-dec {n = zero}  _≟_ xs ys = yes λ ()
    ≗-dec {n = suc n} _≟_ xs ys =
      map′ (Product.uncurry ∷-cong) ∷-injective
           (head xs ≟ head ys ×-dec ≗-dec _≟_ (tail xs) (tail ys))

    ------------------------------------------------------------------------
    -- updateAt

    -- (+) updateAt i actually updates the element at index i.

    updateAt-updates : ∀ (i : Fin n) {f : A → A} (xs : Vector A n) →
                       updateAt xs i f i ≡ f (xs i)
    updateAt-updates zero    xs = refl
    updateAt-updates (suc i) xs = updateAt-updates i (tail xs)

    -- (-) updateAt i does not touch the elements at other indices.

    updateAt-minimal : ∀ (i j : Fin n) {f : A → A} (xs : Vector A n) →
                       i ≢ j → updateAt xs j f i ≡ xs i
    updateAt-minimal zero    zero    xs 0≢0 = contradiction refl 0≢0
    updateAt-minimal zero    (suc j) xs _   = refl
    updateAt-minimal (suc i) zero    xs _   = refl
    updateAt-minimal (suc i) (suc j) xs i≢j = updateAt-minimal i j (tail xs) (i≢j ∘ cong suc)

    -- updateAt i is a monoid morphism from A → A to Vector A n → Vector A n.

    updateAt-id-local : ∀ (i : Fin n) {f : A → A} (xs : Vector A n) →
                        f (xs i) ≡ xs i →
                        updateAt xs i f ≗ xs
    updateAt-id-local zero    xs eq zero    = eq
    updateAt-id-local zero    xs eq (suc j) = refl
    updateAt-id-local (suc i) xs eq zero    = refl
    updateAt-id-local (suc i) xs eq (suc j) = updateAt-id-local i (tail xs) eq j

    updateAt-id : ∀ (i : Fin n) (xs : Vector A n) →
                  updateAt xs i id ≗ xs
    updateAt-id i xs = updateAt-id-local i xs refl

    updateAt-updateAt-local : ∀ (i : Fin n) {f g h : A → A} (xs : Vector A n) →
                              f (g (xs i)) ≡ h (xs i) →
                              updateAt (updateAt xs i g) i f ≗ updateAt xs i h
    updateAt-updateAt-local zero    xs eq zero    = eq
    updateAt-updateAt-local zero    xs eq (suc j) = refl
    updateAt-updateAt-local (suc i) xs eq zero    = refl
    updateAt-updateAt-local (suc i) xs eq (suc j) = updateAt-updateAt-local i (tail xs) eq j

    updateAt-updateAt : ∀ (i : Fin n) {f g : A → A} (xs : Vector A n) →
                        updateAt (updateAt xs i g) i f ≗ updateAt xs i (f ∘ g)
    updateAt-updateAt i xs = updateAt-updateAt-local i xs refl

    updateAt-cong-local : ∀ (i : Fin n) {f g : A → A} (xs : Vector A n) →
                          f (xs i) ≡ g (xs i) →
                          updateAt xs i f ≗ updateAt xs i g
    updateAt-cong-local zero    xs eq zero    = eq
    updateAt-cong-local zero    xs eq (suc j) = refl
    updateAt-cong-local (suc i) xs eq zero    = refl
    updateAt-cong-local (suc i) xs eq (suc j) = updateAt-cong-local i (tail xs) eq j

    updateAt-cong : ∀ (i : Fin n) {f g : A → A} → f ≗ g → (xs : Vector A n) →
                    updateAt xs i f ≗ updateAt xs i g
    updateAt-cong i eq xs = updateAt-cong-local i xs (eq (xs i))

    -- The order of updates at different indices i ≢ j does not matter.

    updateAt-commutes : ∀ (i j : Fin n) {f g : A → A} → i ≢ j → (xs : Vector A n) →
                        updateAt (updateAt xs j g) i f ≗ updateAt (updateAt xs i f) j g
    updateAt-commutes zero    zero    0≢0 xs k       = contradiction refl 0≢0
    updateAt-commutes zero    (suc j) _   xs zero    = refl
    updateAt-commutes zero    (suc j) _   xs (suc k) = refl
    updateAt-commutes (suc i) zero    _   xs zero    = refl
    updateAt-commutes (suc i) zero    _   xs (suc k) = refl
    updateAt-commutes (suc i) (suc j) _   xs zero    = refl
    updateAt-commutes (suc i) (suc j) i≢j xs (suc k) = updateAt-commutes i j (i≢j ∘ cong suc) (tail xs) k

    ------------------------------------------------------------------------
    -- map

    map-id : (xs : Vector A n) → map id xs ≗ xs
    map-id xs = λ _ → refl

    map-cong : ∀ {f g : A → B} → f ≗ g → (xs : Vector A n) → map f xs ≗ map g xs
    map-cong f≗g xs = f≗g ∘ xs

    map-∘ : ∀ {f : B → C} {g : A → B} (xs : Vector A n) →
            map (f ∘ g) xs ≗ map f (map g xs)
    map-∘ xs = λ _ → refl

    lookup-map : ∀ (i : Fin n) (f : A → B) (xs : Vector A n) →
                 map f xs i ≡ f (xs i)
    lookup-map i f xs = refl

    map-updateAt-local : ∀ {f : A → B} {g : A → A} {h : B → B}
                         (xs : Vector A n) (i : Fin n) →
                         f (g (xs i)) ≡ h (f (xs i)) →
                         map f (updateAt xs i g) ≗ updateAt (map f xs) i h
    map-updateAt-local {n = suc n}       {f = f} xs zero    eq zero    = eq
    map-updateAt-local {n = suc n}       {f = f} xs zero    eq (suc j) = refl
    map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq zero    = refl
    map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq (suc j) = map-updateAt-local {f = f} (tail xs) i eq j

    map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B} →
                   f ∘ g ≗ h ∘ f →
                   (xs : Vector A n) (i : Fin n) →
                   map f (updateAt xs i g) ≗ updateAt (map f xs) i h
    map-updateAt {f = f} {g = g} f∘g≗h∘f xs i = map-updateAt-local {f = f} {g = g} xs i (f∘g≗h∘f (xs i))

    ------------------------------------------------------------------------
    -- _++_

    lookup-++-< : ∀ (xs : Vector A m) (ys : Vector A n) →
                  ∀ i (i<m : toℕ i ℕ.< m) →
                  (xs ++ ys) i ≡ xs (fromℕ< i<m)
    lookup-++-< {m = m} xs ys i i<m = cong Sum.[ xs , ys ] (Finₚ.splitAt-< m i i<m)

    lookup-++-≥ : ∀ (xs : Vector A m) (ys : Vector A n) →
                  ∀ i (i≥m : toℕ i ℕ.≥ m) →
                  (xs ++ ys) i ≡ ys (reduce≥ i i≥m)
    lookup-++-≥ {m = m} xs ys i i≥m = cong Sum.[ xs , ys ] (Finₚ.splitAt-≥ m i i≥m)

    lookup-++ˡ : ∀ (xs : Vector A m) (ys : Vector A n) i →
                 (xs ++ ys) (i ↑ˡ n) ≡ xs i
    lookup-++ˡ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ˡ m i n)

    lookup-++ʳ : ∀ (xs : Vector A m) (ys : Vector A n) i →
                 (xs ++ ys) (m ↑ʳ i) ≡ ys i
    lookup-++ʳ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ʳ m n i)

    module _ {ys ys′ : Vector A m} where

      ++-cong : ∀ (xs xs′ : Vector A n) →
                xs ≗ xs′ → ys ≗ ys′ → xs ++ ys ≗ xs′ ++ ys′
      ++-cong {n} xs xs′ eq₁ eq₂ i with toℕ i ℕ.<? n
      ... | yes i<n = begin
        (xs ++ ys) i      ≡⟨ lookup-++-< xs ys i i<n ⟩
        xs (fromℕ< i<n)   ≡⟨ eq₁ (fromℕ< i<n) ⟩
        xs′ (fromℕ< i<n)  ≡⟨ lookup-++-< xs′ ys′ i i<n ⟨
        (xs′ ++ ys′) i    ∎
        where open ≡-Reasoning
      ... | no i≮n = begin
        (xs ++ ys) i               ≡⟨ lookup-++-≥ xs ys i (ℕ.≮⇒≥ i≮n) ⟩
        ys (reduce≥ i (ℕ.≮⇒≥ i≮n))   ≡⟨ eq₂ (reduce≥ i (ℕ.≮⇒≥ i≮n)) ⟩
        ys′ (reduce≥ i (ℕ.≮⇒≥ i≮n))  ≡⟨ lookup-++-≥ xs′ ys′ i (ℕ.≮⇒≥ i≮n) ⟨
        (xs′ ++ ys′) i             ∎
        where open ≡-Reasoning

      ++-injectiveˡ : ∀ (xs xs′ : Vector A n) →
                      xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′
      ++-injectiveˡ xs xs′ eq i = begin
        xs i                   ≡⟨ lookup-++ˡ xs ys i ⟨
        (xs ++ ys) (i ↑ˡ m)    ≡⟨ eq (i ↑ˡ m) ⟩
        (xs′ ++ ys′) (i ↑ˡ m)  ≡⟨ lookup-++ˡ xs′ ys′ i ⟩
        xs′ i                  ∎
        where open ≡-Reasoning

      ++-injectiveʳ : ∀ (xs xs′ : Vector A n) → xs ++ ys ≗ xs′ ++ ys′ → ys ≗ ys′
      ++-injectiveʳ {n} xs xs′ eq i = begin
        ys i                   ≡⟨ lookup-++ʳ xs ys i ⟨
        (xs ++ ys) (n ↑ʳ i)    ≡⟨ eq (n ↑ʳ i)   ⟩
        (xs′ ++ ys′) (n ↑ʳ i)  ≡⟨ lookup-++ʳ xs′ ys′ i ⟩
        ys′ i                  ∎
        where open ≡-Reasoning

      ++-injective : ∀ (xs xs′ : Vector A n) →
                     xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′ × ys ≗ ys′
      ++-injective xs xs′ eq = ++-injectiveˡ xs xs′ eq , ++-injectiveʳ xs xs′ eq

    ------------------------------------------------------------------------
    -- insertAt

    insertAt-lookup : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A) →
                      insertAt xs i v i ≡ v
    insertAt-lookup {n = n}     xs zero    v = refl
    insertAt-lookup {n = suc n} xs (suc i) v = insertAt-lookup (tail xs) i v

    insertAt-punchIn : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A)
                       (j : Fin n) →
                       insertAt xs i v (punchIn i j) ≡ xs j
    insertAt-punchIn {n = suc n} xs zero    v j       = refl
    insertAt-punchIn {n = suc n} xs (suc i) v zero    = refl
    insertAt-punchIn {n = suc n} xs (suc i) v (suc j) = insertAt-punchIn (tail xs) i v j

    ------------------------------------------------------------------------
    -- removeAt

    removeAt-punchOut : ∀ (xs : Vector A (suc n))
                      {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
                      removeAt xs i (punchOut i≢j) ≡ xs j
    removeAt-punchOut {n = n}     xs {zero}  {zero}  i≢j = contradiction refl i≢j
    removeAt-punchOut {n = suc n} xs {zero}  {suc j} i≢j = refl
    removeAt-punchOut {n = suc n} xs {suc i} {zero}  i≢j = refl
    removeAt-punchOut {n = suc n} xs {suc i} {suc j} i≢j = removeAt-punchOut (tail xs) (i≢j ∘ cong suc)

    removeAt-insertAt : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A) →
                        removeAt (insertAt xs i v) i ≗ xs
    removeAt-insertAt xs zero    v j       = refl
    removeAt-insertAt xs (suc i) v zero    = refl
    removeAt-insertAt xs (suc i) v (suc j) = removeAt-insertAt (tail xs) i v j

    insertAt-removeAt : ∀ (xs : Vector A (suc n)) (i : Fin (suc n)) →
                        insertAt (removeAt xs i) i (xs i) ≗ xs
    insertAt-removeAt {n = n}     xs zero    zero    = refl
    insertAt-removeAt {n = n}     xs zero    (suc j) = refl
    insertAt-removeAt {n = suc n} xs (suc i) zero    = refl
    insertAt-removeAt {n = suc n} xs (suc i) (suc j) = insertAt-removeAt (tail xs) i j

    ------------------------------------------------------------------------
    -- Conversion functions

    toVec∘fromVec : (xs : Vec A n) → toVec (fromVec xs) ≡ xs
    toVec∘fromVec = Vec.tabulate∘lookup

    fromVec∘toVec : (xs : Vector A n) → fromVec (toVec xs) ≗ xs
    fromVec∘toVec = Vec.lookup∘tabulate

    toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
    toList∘fromList = List.tabulate-lookup

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    updateAt-id-relative = updateAt-id-local
    {-# WARNING_ON_USAGE updateAt-id-relative
    "Warning: updateAt-id-relative was deprecated in v2.0.
    Please use updateAt-id-local instead."
    #-}
    updateAt-compose-relative = updateAt-updateAt-local
    {-# WARNING_ON_USAGE updateAt-compose-relative
    "Warning: updateAt-compose-relative was deprecated in v2.0.
    Please use updateAt-updateAt-local instead."
    #-}
    updateAt-compose = updateAt-updateAt
    {-# WARNING_ON_USAGE updateAt-compose
    "Warning: updateAt-compose was deprecated in v2.0.
    Please use updateAt-updateAt instead."
    #-}
    updateAt-cong-relative = updateAt-cong-local
    {-# WARNING_ON_USAGE updateAt-cong-relative
    "Warning: updateAt-cong-relative was deprecated in v2.0.
    Please use updateAt-cong-local instead."
    #-}

    insert-lookup = insertAt-lookup
    {-# WARNING_ON_USAGE insert-lookup
    "Warning: insert-lookup was deprecated in v2.0.
    Please use insertAt-lookup instead."
    #-}
    insert-punchIn = insertAt-punchIn
    {-# WARNING_ON_USAGE insert-punchIn
    "Warning: insert-punchIn was deprecated in v2.0.
    Please use insertAt-punchIn instead."
    #-}
    remove-punchOut = removeAt-punchOut
    {-# WARNING_ON_USAGE remove-punchOut
    "Warning: remove-punchOut was deprecated in v2.0.
    Please use removeAt-punchOut instead."
    #-}
    remove-insert = removeAt-insertAt
    {-# WARNING_ON_USAGE remove-insert
    "Warning: remove-insert was deprecated in v2.0.
    Please use removeAt-insertAt instead."
    #-}
    insert-remove = insertAt-removeAt
    {-# WARNING_ON_USAGE insert-remove
    "Warning: insert-remove was deprecated in v2.0.
    Please use insertAt-removeAt instead."
    #-}