[Add] truncate properties to Data.Vec.Properties #2795

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:45:37Z

CHANGELOG.md

+  take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
+  updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)


Several things (which will be recapitulated below):

indentation/alignment so that updateAt in LHS aligns with beginning of type signature on line above

omit {m n : ℕ} from type signature:

they're inferrable, and/so should be captured by a variable declaration already

such arguments should, where possible, never be non-prenex (otherwise, turning them into variables would be a breaking change!)

I'll double down on my comment on [Add] padRight properties to Data.Vec.Properties #2769 , and say that the argument order (in particular, the position of the f binding) should mirror that for updateAt itself, if only for consistency's sake

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

CHANGELOG.md

+  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:48:45Z

CHANGELOG.md

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


Besides alignment, and the quantifier prefix!, here you need to inline the let binding for o≤n, as otherwise it's out of scope:

Suggested change

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

zipWith f (truncate o≤n xs) (truncate o≤m ys)

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

zipWith f (truncate (≤-trans o≤m m≤n) xs) (truncate o≤m ys)

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

CHANGELOG.md

+  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

CHANGELOG.md

+  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

src/Data/Vec/Properties.agda

+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

src/Data/Vec/Properties.agda

@@ -472,6 +541,20 @@ toList-map : ∀ (f : A → B) (xs : Vec A n) →
 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

src/Data/Vec/Properties.agda

@@ -472,6 +541,20 @@ toList-map : ∀ (f : A → B) (xs : Vec A n) →
 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) →
+  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

src/Data/Vec/Properties.agda

+    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

src/Data/Vec/Properties.agda

+    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.

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

Open

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

Open

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

		take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
		updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)

		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)

		truncate-zipWith-truncate : truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
		zipWith f (truncate o≤n xs) (truncate o≤m 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 =

[Add] truncate properties to Data.Vec.Properties #2795

Are you sure you want to change the base?

[Add] truncate properties to Data.Vec.Properties #2795

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!

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!

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!

e-mniang commented Jul 30, 2025 •

edited

Loading

jamesmckinna commented Jul 31, 2025 •

edited

Loading