[Add] truncate properties to Data.Vec.Properties by e-mniang · Pull Request #2795 · agda/agda-stdlib

e-mniang · 2025-07-30T18:48:59Z

As suggested by @jamesmckinna, this PR adds several equational properties for truncate to Data.Vec.Properties, extending the standard vector operations toolkit with useful lemmas for reasoning about truncate.

Added properties:

- take-updateAt : applying updateAt before or after take yields the same result on valid indices

- truncate-zipWith : truncate commutes with zipWith on vectors of equal length

- truncate-zipWith-truncate : generalizes truncate-zipWith when one vector is already truncated

- zipWith-truncate : zipWith followed by truncate equals truncating the inputs first, when lengths match

- zipWith-truncate₁ : a more general version of zipWith-truncate with shifted truncation offsets

- updateAt-truncate : rewriting updateAt after truncate via take equivalence

- truncate++drop≡id : a vector can be recovered by appending its truncated prefix and dropped suffix

- truncate-map : truncate commutes with map

jamesmckinna · 2025-07-31T12:01:56Z

@MatthewDaggitt are you happy to proceed with this PR, and its predecessor #2769 for v2.4, and only consider #2770 / #2787 downstream, or should we move to reconcile them all together?

UPDATED: I'll review once the direction of travel is (a bit) clearer...

MatthewDaggitt · 2025-08-02T05:16:06Z

Yes, I'm happy to add these now and then the breaking changes in v3.0.

jamesmckinna

Lots of things to fix, hopefully all (most?) of which will simplify what's here.

jamesmckinna · 2025-08-02T12:46:00Z

+  truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
+  truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)


Ditto. re: alignment

jamesmckinna · 2025-08-02T12:51:18Z

+  zipWith-truncate : zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡
+  truncate p≤p+q (zipWith f xs ys)


I don't understand why you've changed to p and q here, rather than m and n?
Also, we 'know' that p ≤ p + q, so the (presumably) mnemonic name must be carrying other information? If not, simply use m≤n?

jamesmckinna · 2025-08-02T12:52:07Z

+  zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
+  truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)


Similarly here, the names are getting very unwieldy... I'll look at the code to see what might be going on...

jamesmckinna · 2025-08-02T13:31:14Z

+truncate++drop≡id {m = m} {n} xs = begin
+  truncate (m≤m+n m n) xs ++ drop m xs ≡⟨ cong (_++ drop m xs) (take≡truncate m xs) ⟨
+  take m xs ++ drop m xs               ≡⟨ take++drop≡id m xs ⟩
+  xs ∎ where open ≡-Reasoning


jamesmckinna · 2025-08-02T13:33:25Z

 toList-map f [] = refl
 toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)

+truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →


Suggested change

truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →

truncate-map : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →

jamesmckinna · 2025-08-02T13:34:07Z


+truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →
+  map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+truncate-map {n = n} f m m≤n xs =


... with corresponding

Suggested change

truncate-map {n = n} f m m≤n xs =

truncate-map {m = m} {n = n} f m≤n xs =

jamesmckinna · 2025-08-02T13:35:27Z

+    take m (cast eq (map f xs)) ≡⟨ truncate≡take m≤n (map f xs) eq ⟨
+    truncate m≤n (map f xs) ∎
+ where
+   .eq : n ≡ m + (n ∸ m)


No need to mark eq as irrelevant; it's the proof which is ignored by cast etc.

Suggested change

.eq : n ≡ m + (n ∸ m)

eq : n ≡ m + (n ∸ m)

jamesmckinna · 2025-08-02T13:39:18Z

+    truncate m≤n (map f xs) ∎
+ where
+   .eq : n ≡ m + (n ∸ m)
+   eq = sym (proj₂ (m≤n⇒∃[o]m+o≡n m≤n))


In fact, Data.Nat.Properties.guarded-∸≗∸ is (more like) what you need here... and could then be inlined?

See also padRight-drop′ and padRight-take′ that I've added to #2787 for comparison.

jamesmckinna · 2025-08-02T13:43:02Z

Thanks for the second contribution!
Once the backports #2799 from v2.3 have been merged into master, it will make sense to fix up the CHANGELOG conflicts, merge master into this branch, and then look at the suggested fixes.

…e `truncate-irrelevant`

e-mniang · 2025-08-06T18:53:15Z

Hi!
Thanks for your review. I made some changes based on what you said and deleted most of the things that could conflict with the Fairbairn threshold.
Let me know if anything else needs corrections.

jamesmckinna

Sorry for the last nitpicks, but otherwise all looks good!
(But: you'll need to fix the CHANGELOG again... happens a lot at the beginning of a new cycle of vx.y developemnt :-()

jamesmckinna

All looks good!
Thanks very much for this final round of nitpicks.

…ht}` irrelevant (#2787) * refactor: make `truncate` and `padRight` take irrelevant argument * fix: proofs of properties following #2769 and #2795; deprecate `truncate-irrelevant` * fix: deprecation in `CHANGELOG` * fix: duplication after resolving merge conflict * fix: alignment * add: specialised versions of `padRight-drop` and `padRight-take` * fix: whitespace * reset: `CHANGELOG` * restore: new `CHANGELOG` entries * refactor: weaken types of `truncate` properties * fix:`CHANGELOG` to reflect weakened types * fix: whitespace * final tweak * final tweak

* adding truncate's properties * update changelog * cleaning whitespaces * Recleaning * corrections after reviews * correction of changelog * changes after review

…ht}` irrelevant (#2787) * refactor: make `truncate` and `padRight` take irrelevant argument * fix: proofs of properties following #2769 and #2795; deprecate `truncate-irrelevant` * fix: deprecation in `CHANGELOG` * fix: duplication after resolving merge conflict * fix: alignment * add: specialised versions of `padRight-drop` and `padRight-take` * fix: whitespace * reset: `CHANGELOG` * restore: new `CHANGELOG` entries * refactor: weaken types of `truncate` properties * fix:`CHANGELOG` to reflect weakened types * fix: whitespace * final tweak * final tweak

e-mniang added 2 commits July 30, 2025 14:11

adding truncate's properties

e23bb4b

update changelog

ead92ab

e-mniang marked this pull request as ready for review July 30, 2025 18:52

MatthewDaggitt requested a review from jamesmckinna July 31, 2025 00:28

MatthewDaggitt added this to the v2.4 milestone Jul 31, 2025

MatthewDaggitt added the addition label Jul 31, 2025

e-mniang added 2 commits July 31, 2025 14:00

cleaning whitespaces

d2e46d8

Recleaning

fd1d7f2

jamesmckinna requested changes Aug 2, 2025

View reviewed changes

This was referenced Aug 2, 2025

[Add] padRight properties to Data.Vec.Properties #2769

Merged

[Add] Properties for DCPOs in Relation.Binary.Properties.Domain #2734

Closed

[ refactor ] make m ≤ n argument to Data.Vec.Base.{truncate|padRight} irrelevant #2787

Merged

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Aug 3, 2025

fix: proofs of properties following agda#2769 and agda#2795; deprecat…

ab03dc0

…e `truncate-irrelevant`

corrections after reviews

ac32928

jamesmckinna reviewed Aug 8, 2025

View reviewed changes

Comment thread CHANGELOG.md Outdated

jamesmckinna approved these changes Aug 8, 2025

View reviewed changes

e-mniang added 2 commits August 10, 2025 08:30

correction of changelog

56b9f0b

Merge branch 'master' into TruncateProperties

70b85de

jamesmckinna reviewed Oct 5, 2025

View reviewed changes

Comment thread src/Data/Vec/Properties.agda Outdated

changes after review

f05746c

jamesmckinna approved these changes Oct 9, 2025

View reviewed changes

jamesmckinna requested a review from MatthewDaggitt October 9, 2025 06:16

JacquesCarette approved these changes Oct 10, 2025

View reviewed changes

JacquesCarette added this pull request to the merge queue Oct 10, 2025

Merged via the queue into agda:master with commit 2ce5eb3 Oct 10, 2025
12 checks passed

andreasabel mentioned this pull request Apr 18, 2026

Update experimental branch; allow GHC 9.14 #2985

Merged

		truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
		truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)

		zipWith-truncate : zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡
		truncate p≤p+q (zipWith f xs ys)

		zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
		truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)

	truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →
	truncate-map : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →

	truncate-map {n = n} f m m≤n xs =
	truncate-map {m = m} {n = n} f m≤n xs =

Uh oh!

Conversation

e-mniang commented Jul 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna commented Jul 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MatthewDaggitt commented Aug 2, 2025

Uh oh!

jamesmckinna left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Aug 2, 2025

Uh oh!

e-mniang commented Aug 6, 2025

Uh oh!

Uh oh!

jamesmckinna left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jamesmckinna left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

e-mniang commented Jul 30, 2025 •

edited

Loading

jamesmckinna commented Jul 31, 2025 •

edited

Loading

jamesmckinna left a comment •

edited

Loading