Sync insert, remove, and update functionalities for List and Vec

CHANGELOG.md

@@ -2133,7 +2133,7 @@ Other minor changes
   gcd-zero  : Zero 1ℤ gcd
   ```
 
-* Added new functions in `Data.List`:
+* Added new functions in `Data.List.Base`:
   ```agda
   takeWhileᵇ   : (A → Bool) → List A → List A
   dropWhileᵇ   : (A → Bool) → List A → List A
@@ -2145,14 +2145,15 @@ Other minor changes
   wordsByᵇ     : (A → Bool) → List A → List (List A)
   derunᵇ       : (A → A → Bool) → List A → List A
   deduplicateᵇ : (A → A → Bool) → List A → List A
-  ```
 
-* Added new functions and definitions to `Data.List.Base`:
-  ```agda
-  catMaybes : List (Maybe A) → List A
-  ap : List (A → B) → List A → List B
-  ++-rawMagma : Set a → RawMagma a _
+  catMaybes       : List (Maybe A) → List A
+  ap              : List (A → B) → List A → List B
+  ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
+
+  insert   : (xs : List A) → Fin (length xs) → A → List A
+  remove   : (xs : List A) → Fin (length xs) → List A
+  updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
 
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
@@ -2558,6 +2559,8 @@ Other minor changes
   _ʳ++_              : Vec A m → Vec A n → Vec A (m + n)
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
+
+  _─_ : Vec A (suc n) → Fin (suc n) → Vec A n
   ```
 
 * Added new instance in `Data.Vec.Categorical`:

src/Data/Fin/Subset.agda

@@ -14,7 +14,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base using (List; foldr; foldl)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product using (∃; _×_)
-open import Data.Vec.Base hiding (foldr; foldl)
+open import Data.Vec.Base hiding (foldr; foldl; _─_)
 open import Relation.Nullary
 
 private

src/Data/Fin/Subset/Properties.agda

@@ -25,7 +25,7 @@ open import Data.Nat.Base hiding (∣_-_∣)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product as Product using (∃; ∄; _×_; _,_; proj₁)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Data.Vec.Base
+open import Data.Vec.Base hiding (_─_)
 open import Data.Vec.Properties
 open import Function.Base using (_∘_; const; id; case_of_)
 open import Function.Bundles using (_⇔_; mk⇔)

src/Data/List/Base.agda

@@ -195,6 +195,14 @@ tails : List A → List (List A)
 tails []       = [] ∷ []
 tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
 
+insert : (xs : List A) → Fin (length xs) → A → List A
+insert (x ∷ xs) zero    v = v ∷ x ∷ xs
+insert (x ∷ xs) (suc k) v = v ∷ insert xs k v
+
+updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
+updateAt (x ∷ xs) zero    f = f x ∷ xs
+updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f
+
 -- Scans
 
 scanr : (A → B → B) → B → List A → List B
@@ -329,6 +337,10 @@ splitAt zero    xs       = ([] , xs)
 splitAt (suc n) []       = ([] , [])
 splitAt (suc n) (x ∷ xs) = Prod.map₁ (x ∷_) (splitAt n xs)
 
+remove : (xs : List A) → Fin (length xs) → List A
+remove (x ∷ xs) zero     = xs
+remove (x ∷ xs) (suc i)  = x ∷ remove xs i
+
 -- The following are functions which split a list up using boolean
 -- predicates. However, in practice they are difficult to use and
 -- prove properties about, and are mainly provided for advanced use
@@ -441,16 +453,20 @@ deduplicate R? = deduplicateᵇ (does ∘₂ R?)
 
 infixl 5 _[_]%=_ _[_]∷=_ _─_
 
+-- xs [ i ]%= f  modifies the i-th element of xs according to f
+
 _[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
-(x ∷ xs) [ zero  ]%= f = f x ∷ xs
-(x ∷ xs) [ suc k ]%= f = x ∷ (xs [ k ]%= f)
+xs [ i ]%= f = updateAt xs i f
+
+-- xs [ i ]≔ y  overwrites the i-th element of xs with y
 
 _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
 xs [ k ]∷= v = xs [ k ]%= const v
 
+-- xs ─ i removes the i-th element of xs
+
 _─_ : (xs : List A) → Fin (length xs) → List A
-(x ∷ xs) ─ zero  = xs
-(x ∷ xs) ─ suc k = x ∷ (xs ─ k)
+xs ─ i = remove xs i
 
 ------------------------------------------------------------------------
 -- Conditional versions of cons and snoc

src/Data/List/Countdown.agda

@@ -20,7 +20,7 @@ open import Function.Base
 open import Function.Bundles
   using (Injection; module Injection)
 open import Data.Bool.Base using (true; false)
-open import Data.List.Base hiding (lookup)
+open import Data.List.Base hiding (lookup; insert)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product

src/Data/List/Relation/Unary/All/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Bool.Properties using (T-∧)
 open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List hiding (lookup)
+open import Data.List.Base as List hiding (lookup; updateAt)
 open import Data.List.Properties as Listₚ using (partition-defn)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties

src/Data/Vec/Base.agda

@@ -78,18 +78,21 @@ 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 _[_]%=_
+infixl 6 _[_]%=_ _[_]≔_ _─_
 
 _[_]%=_ : 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 _[_]≔_
-
 _[_]≔_ : Vec A n → Fin n → A → Vec A n
 xs [ i ]≔ y = xs [ i ]%= const y
 
+-- xs ─ i removes the i-th element of xs
+
+_─_ : Vec A (suc n) → Fin (suc n) → Vec A n
+xs ─ i = remove xs i
+
 ------------------------------------------------------------------------
 -- Operations for transforming vectors