Skip to content

Commit 698dfee

Browse files
Saransh-cppandreasabel
authored andcommitted
Sync insert, remove, and update functionalities for List and Vec (#2049)
1 parent 33cb598 commit 698dfee

File tree

11 files changed

+489
-251
lines changed

11 files changed

+489
-251
lines changed

CHANGELOG.md

+95-15
Original file line numberDiff line numberDiff line change
@@ -797,6 +797,50 @@ Non-backwards compatible changes
797797
IO.Instances
798798
```
799799

800+
### Standardisation of `insertAt`/`updateAt`/`removeAt`
801+
802+
* Previously, the names and argument order of index-based insertion, update and removal functions for
803+
various types of lists and vectors were inconsistent.
804+
805+
* To fix this the names have all been standardised to `insertAt`/`updateAt`/`removeAt`.
806+
807+
* Correspondingly the following changes have occurred:
808+
809+
* In `Data.List.Base` the following have been added:
810+
```agda
811+
insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
812+
updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
813+
removeAt : (xs : List A) → Fin (length xs) → List A
814+
```
815+
and the following has been deprecated
816+
```
817+
_─_ ↦ removeAt
818+
```
819+
820+
* In `Data.Vec.Base`:
821+
```agda
822+
insert ↦ insertAt
823+
remove ↦ removeAt
824+
825+
updateAt : Fin n → (A → A) → Vec A n → Vec A n
826+
827+
updateAt : Vec A n → Fin n → (A → A) → Vec A n
828+
```
829+
830+
* In `Data.Vec.Functional`:
831+
```agda
832+
remove : Fin (suc n) → Vector A (suc n) → Vector A n
833+
834+
removeAt : Vector A (suc n) → Fin (suc n) → Vector A n
835+
836+
updateAt : Fin n → (A → A) → Vector A n → Vector A n
837+
838+
updateAt : Vector A n → Fin n → (A → A) → Vector A n
839+
```
840+
841+
* The old names (and the names of all proofs about these functions) have been deprecated appropriately.
842+
843+
800844
### Changes to triple reasoning interface
801845

802846
* The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
@@ -1321,6 +1365,11 @@ Deprecated names
13211365
+-isAbelianGroup ↦ +-0-isAbelianGroup
13221366
```
13231367

1368+
* In `Data.List.Base`:
1369+
```
1370+
_─_ ↦ removeAt
1371+
```
1372+
13241373
* In `Data.List.Properties`:
13251374
```agda
13261375
map-id₂ ↦ map-id-local
@@ -1337,7 +1386,10 @@ Deprecated names
13371386
13381387
ʳ++-++ ↦ ++-ʳ++
13391388
1340-
take++drop ↦ take++drop≡id
1389+
take++drop ↦ take++drop≡id
1390+
1391+
length-─ ↦ length-removeAt
1392+
map-─ ↦ map-removeAt
13411393
```
13421394

13431395
* In `Data.List.NonEmpty.Properties`:
@@ -1350,8 +1402,8 @@ Deprecated names
13501402
* In `Data.List.Relation.Unary.All.Properties`:
13511403
```agda
13521404
updateAt-id-relative ↦ updateAt-id-local
1353-
updateAt-compose-relative ↦ updateAt--local
1354-
updateAt-compose ↦ updateAt-
1405+
updateAt-compose-relative ↦ updateAt-updateAt-local
1406+
updateAt-compose ↦ updateAt-updateAt
13551407
updateAt-cong-relative ↦ updateAt-cong-local
13561408
```
13571409

@@ -1497,6 +1549,12 @@ Deprecated names
14971549
map-compose ↦ map-∘
14981550
```
14991551

1552+
* In `Data.Vec.Base`:
1553+
```
1554+
remove ↦ removeAt
1555+
insert ↦ insertAt
1556+
```
1557+
15001558
* In `Data.Vec.Properties`:
15011559
```
15021560
take-distr-zipWith ↦ take-zipWith
@@ -1505,8 +1563,8 @@ Deprecated names
15051563
drop-distr-map ↦ drop-map
15061564
15071565
updateAt-id-relative ↦ updateAt-id-local
1508-
updateAt-compose-relative ↦ updateAt--local
1509-
updateAt-compose ↦ updateAt-
1566+
updateAt-compose-relative ↦ updateAt-updateAt-local
1567+
updateAt-compose ↦ updateAt-updateAt
15101568
updateAt-cong-relative ↦ updateAt-cong-local
15111569
15121570
[]%=-compose ↦ []%=-∘
@@ -1516,7 +1574,15 @@ Deprecated names
15161574
idIsFold ↦ id-is-foldr
15171575
sum-++-commute ↦ sum-++
15181576
1519-
take-drop-id ↦ take++drop≡id
1577+
take-drop-id ↦ take++drop≡id
1578+
1579+
map-insert ↦ map-insertAt
1580+
1581+
insert-lookup ↦ insertAt-lookup
1582+
insert-punchIn ↦ insertAt-punchIn
1583+
remove-PunchOut ↦ removeAt-punchOut
1584+
remove-insert ↦ removeAt-insertAt
1585+
insert-remove ↦ insertAt-removeAt
15201586
15211587
lookup-inject≤-take ↦ lookup-take-inject≤
15221588
```
@@ -1532,11 +1598,17 @@ Deprecated names
15321598
* In `Data.Vec.Functional.Properties`:
15331599
```
15341600
updateAt-id-relative ↦ updateAt-id-local
1535-
updateAt-compose-relative ↦ updateAt--local
1536-
updateAt-compose ↦ updateAt-
1601+
updateAt-compose-relative ↦ updateAt-updateAt-local
1602+
updateAt-compose ↦ updateAt-updateAt
15371603
updateAt-cong-relative ↦ updateAt-cong-local
15381604
15391605
map-updateAt ↦ map-updateAt-local
1606+
1607+
insert-lookup ↦ insertAt-lookup
1608+
insert-punchIn ↦ insertAt-punchIn
1609+
remove-punchOut ↦ removeAt-punchOut
1610+
remove-insert ↦ removeAt-insertAt
1611+
insert-remove ↦ insertAt-removeAt
15401612
```
15411613
NB. This last one is complicated by the *addition* of a 'global' property `map-updateAt`
15421614

@@ -2312,7 +2384,7 @@ Additions to existing modules
23122384
gcd-zero : Zero 1ℤ gcd
23132385
```
23142386

2315-
* Added new functions in `Data.List`:
2387+
* Added new functions in `Data.List.Base`:
23162388
```agda
23172389
takeWhileᵇ : (A → Bool) → List A → List A
23182390
dropWhileᵇ : (A → Bool) → List A → List A
@@ -2331,14 +2403,14 @@ Additions to existing modules
23312403
find : Decidable P → List A → Maybe A
23322404
findIndex : Decidable P → (xs : List A) → Maybe $ Fin (length xs)
23332405
findIndices : Decidable P → (xs : List A) → List $ Fin (length xs)
2334-
```
23352406
2336-
* Added new functions and definitions to `Data.List.Base`:
2337-
```agda
2338-
catMaybes : List (Maybe A) → List A
2339-
ap : List (A → B) → List A → List B
2340-
++-rawMagma : Set a → RawMagma a _
2407+
catMaybes : List (Maybe A) → List A
2408+
ap : List (A → B) → List A → List B
2409+
++-rawMagma : Set a → RawMagma a _
23412410
++-[]-rawMonoid : Set a → RawMonoid a _
2411+
2412+
insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
2413+
updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
23422414
```
23432415

23442416
* Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
@@ -2405,6 +2477,11 @@ Additions to existing modules
24052477
map-replicate : map f (replicate n x) ≡ replicate n (f x)
24062478
24072479
drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
2480+
2481+
length-insertAt : length (insertAt xs i v) ≡ suc (length xs)
2482+
length-removeAt′ : length xs ≡ suc (length (removeAt xs k))
2483+
removeAt-insertAt : removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs
2484+
insertAt-removeAt : insertAt (removeAt xs i) (cast (sym (lengthAt-removeAt xs i)) i) (lookup xs i) ≡ xs
24082485
```
24092486

24102487
* Added new patterns and definitions to `Data.Nat.Base`:
@@ -2841,6 +2918,9 @@ Additions to existing modules
28412918
fromList-map : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs)
28422919
fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
28432920
2921+
length-toList : List.length (toList xs) ≡ length xs
2922+
toList-insertAt : toList (insertAt xs i v) ≡ List.insertAt (toList xs) (Fin.cast (cong suc (sym (length-toList xs))) i) v
2923+
28442924
truncate≡take : .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs)
28452925
take≡truncate : take m xs ≡ truncate (m≤m+n m n) xs
28462926
lookup-truncate : lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n)

src/Algebra/Properties/CommutativeMonoid/Sum.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ open import Algebra.Properties.Monoid.Sum monoid public
4646

4747
-- When summing over a function from a finite set, we can pull out any
4848
-- value and move it to the front.
49-
sum-remove : {n} {i : Fin (suc n)} t sum t ≈ t i + sum (remove i t)
49+
sum-remove : {n} {i : Fin (suc n)} t sum t ≈ t i + sum (removeAt t i)
5050
sum-remove {_} {zero} xs = refl
5151
sum-remove {suc n} {suc i} xs = begin
5252
t₀ + ∑t ≈⟨ +-congˡ (sum-remove t) ⟩
@@ -57,7 +57,7 @@ sum-remove {suc n} {suc i} xs = begin
5757
t₀ = head xs
5858
tᵢ = t i
5959
∑t = sum t
60-
∑t′ = sum (remove i t)
60+
∑t′ = sum (removeAt t i)
6161

6262
-- The '∑' operator distributes over addition.
6363
∑-distrib-+ : {n} (f g : Vector Carrier n) ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
@@ -93,10 +93,10 @@ sum-permute {suc m} {suc n} f π = begin
9393
f 0F + sum f/0 ≡˘⟨ P.cong (_+ sum f/0) (P.cong f (Perm.inverseʳ π)) ⟩
9494
πf π₀ + sum f/0 ≈⟨ +-congˡ (sum-permute f/0 (Perm.remove π₀ π)) ⟩
9595
πf π₀ + sum (rearrange (π/0 ⟨$⟩ʳ_) f/0) ≡˘⟨ P.cong (πf π₀ +_) (sum-cong-≗ (P.cong f ∘ Perm.punchIn-permute′ π 0F)) ⟩
96-
πf π₀ + sum (remove π₀ πf) ≈⟨ sym (sum-remove πf) ⟩
96+
πf π₀ + sum (removeAt πf π₀) ≈⟨ sym (sum-remove πf) ⟩
9797
sum πf ∎
9898
where
99-
f/0 = remove 0F f
99+
f/0 = removeAt f 0F
100100
π₀ = π ⟨$⟩ˡ 0F
101101
π/0 = Perm.remove π₀ π
102102
πf = rearrange (π ⟨$⟩ʳ_) f

src/Algebra/Properties/Semiring/Binomial.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ sum₂ n = ∑[ k ≤ suc n ] term₂ n k
7171
------------------------------------------------------------------------
7272
-- Properties
7373

74-
term₂[n,n+1]≈0# : n term₂ n (fromℕ (suc n)) ≈ 0#
74+
term₂[n,n+1]≈0# : n term₂ n (fromℕ (suc n)) ≈ 0#
7575
term₂[n,n+1]≈0# n rewrite view-fromℕ (suc n) = refl
7676

7777
lemma₁ : n x * binomialExpansion n ≈ sum₁ n
@@ -117,7 +117,7 @@ x*lemma {n} i = begin
117117
------------------------------------------------------------------------
118118
-- Next, a lemma which does require commutativity
119119

120-
y*lemma : x * y ≈ y * x {n : ℕ} (j : Fin n)
120+
y*lemma : x * y ≈ y * x {n : ℕ} (j : Fin n)
121121
y * binomialTerm n (suc j) ≈ (n C toℕ (suc j)) × binomial (suc n) (suc (inject₁ j))
122122
y*lemma x*y≈y*x {n} j = begin
123123
y * binomialTerm n (suc j)

src/Data/List/Base.agda

+27-7
Original file line numberDiff line numberDiff line change
@@ -196,6 +196,14 @@ tails : List A → List (List A)
196196
tails [] = [] ∷ []
197197
tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
198198

199+
insertAt : (xs : List A) Fin (suc (length xs)) A List A
200+
insertAt xs zero v = v ∷ xs
201+
insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v
202+
203+
updateAt : (xs : List A) Fin (length xs) (A A) List A
204+
updateAt (x ∷ xs) zero f = f x ∷ xs
205+
updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f
206+
199207
-- Scans
200208

201209
scanr : (A B B) B List A List B
@@ -330,6 +338,10 @@ splitAt zero xs = ([] , xs)
330338
splitAt (suc n) [] = ([] , [])
331339
splitAt (suc n) (x ∷ xs) = Prod.map₁ (x ∷_) (splitAt n xs)
332340

341+
removeAt : (xs : List A) Fin (length xs) List A
342+
removeAt (x ∷ xs) zero = xs
343+
removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i
344+
333345
-- The following are functions which split a list up using boolean
334346
-- predicates. However, in practice they are difficult to use and
335347
-- prove properties about, and are mainly provided for advanced use
@@ -469,19 +481,18 @@ findIndices P? = findIndicesᵇ (does ∘ P?)
469481
------------------------------------------------------------------------
470482
-- Actions on single elements
471483

472-
infixl 5 _[_]%=_ _[_]∷=_ _─_
484+
infixl 5 _[_]%=_ _[_]∷=_
485+
486+
-- xs [ i ]%= f modifies the i-th element of xs according to f
473487

474488
_[_]%=_ : (xs : List A) Fin (length xs) (A A) List A
475-
(x ∷ xs) [ zero ]%= f = f x ∷ xs
476-
(x ∷ xs) [ suc k ]%= f = x ∷ (xs [ k ]%= f)
489+
xs [ i ]%= f = updateAt xs i f
490+
491+
-- xs [ i ]≔ y overwrites the i-th element of xs with y
477492

478493
_[_]∷=_ : (xs : List A) Fin (length xs) A List A
479494
xs [ k ]∷= v = xs [ k ]%= const v
480495

481-
_─_ : (xs : List A) Fin (length xs) List A
482-
(x ∷ xs) ─ zero = xs
483-
(x ∷ xs) ─ suc k = x ∷ (xs ─ k)
484-
485496
------------------------------------------------------------------------
486497
-- Conditional versions of cons and snoc
487498

@@ -527,3 +538,12 @@ _∷ʳ'_ = InitLast._∷ʳ′_
527538
"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
528539
Please use _∷ʳ′_ (ending in a prime) instead."
529540
#-}
541+
542+
-- Version 2.0
543+
544+
infixl 5 _─_
545+
_─_ = removeAt
546+
{-# WARNING_ON_USAGE _─_
547+
"Warning: _─_ was deprecated in v2.0.
548+
Please use removeAt instead."
549+
#-}

src/Data/List/Properties.agda

+45-9
Original file line numberDiff line numberDiff line change
@@ -746,17 +746,41 @@ map-∷= (x ∷ xs) zero v f = refl
746746
map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)
747747

748748
------------------------------------------------------------------------
749-
-- _─_
749+
-- insertAt
750750

751-
length-─ : (xs : List A) k length (xs ─ k) ≡ pred (length xs)
752-
length-─ (x ∷ xs) zero = refl
753-
length-─ (x ∷ y ∷ xs) (suc k) = cong suc (length-─ (y ∷ xs) k)
751+
length-insertAt : (xs : List A) (i : Fin (suc (length xs))) v
752+
length (insertAt xs i v) ≡ suc (length xs)
753+
length-insertAt xs zero v = refl
754+
length-insertAt (x ∷ xs) (suc i) v = cong suc (length-insertAt xs i v)
754755

755-
map-─ : xs k (f : A B)
756-
let eq = sym (length-map f xs) in
757-
map f (xs ─ k) ≡ map f xs ─ cast eq k
758-
map-─ (x ∷ xs) zero f = refl
759-
map-─ (x ∷ xs) (suc k) f = cong (f x ∷_) (map-─ xs k f)
756+
------------------------------------------------------------------------
757+
-- removeAt
758+
759+
length-removeAt : (xs : List A) k length (removeAt xs k) ≡ pred (length xs)
760+
length-removeAt (x ∷ xs) zero = refl
761+
length-removeAt (x ∷ xs@(_ ∷ _)) (suc k) = cong suc (length-removeAt xs k)
762+
763+
length-removeAt′ : (xs : List A) k length xs ≡ suc (length (removeAt xs k))
764+
length-removeAt′ xs@(_ ∷ _) k rewrite length-removeAt xs k = refl
765+
766+
map-removeAt : xs k (f : A B)
767+
let eq = sym (length-map f xs) in
768+
map f (removeAt xs k) ≡ removeAt (map f xs) (cast eq k)
769+
map-removeAt (x ∷ xs) zero f = refl
770+
map-removeAt (x ∷ xs) (suc k) f = cong (f x ∷_) (map-removeAt xs k f)
771+
772+
------------------------------------------------------------------------
773+
-- insertAt and removeAt
774+
775+
removeAt-insertAt : (xs : List A) (i : Fin (suc (length xs))) v
776+
removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs
777+
removeAt-insertAt xs zero v = refl
778+
removeAt-insertAt (x ∷ xs) (suc i) v = cong (_ ∷_) (removeAt-insertAt xs i v)
779+
780+
insertAt-removeAt : (xs : List A) (i : Fin (length xs))
781+
insertAt (removeAt xs i) (cast (length-removeAt′ xs i) i) (lookup xs i) ≡ xs
782+
insertAt-removeAt (x ∷ xs) zero = refl
783+
insertAt-removeAt (x ∷ xs) (suc i) = cong (x ∷_) (insertAt-removeAt xs i)
760784

761785
------------------------------------------------------------------------
762786
-- take
@@ -1224,3 +1248,15 @@ take++drop = take++drop≡id
12241248
"Warning: take++drop was deprecated in v2.0.
12251249
Please use take++drop≡id instead."
12261250
#-}
1251+
1252+
length-─ = length-removeAt
1253+
{-# WARNING_ON_USAGE length-─
1254+
"Warning: length-─ was deprecated in v2.0.
1255+
Please use length-removeAt instead."
1256+
#-}
1257+
1258+
map-─ = map-removeAt
1259+
{-# WARNING_ON_USAGE map-─
1260+
"Warning: map-─ was deprecated in v2.0.
1261+
Please use map-removeAt instead."
1262+
#-}

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ open import Data.Bool.Base using (Bool; T; true; false)
1313
open import Data.Bool.Properties using (T-∧)
1414
open import Data.Empty
1515
open import Data.Fin.Base using (Fin; zero; suc)
16-
open import Data.List.Base as List hiding (lookup)
16+
open import Data.List.Base as List hiding (lookup; updateAt)
1717
open import Data.List.Properties as Listₚ using (partition-defn)
1818
open import Data.List.Membership.Propositional
1919
open import Data.List.Membership.Propositional.Properties

0 commit comments

Comments
 (0)