Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 15 commits into from
Aug 5, 2025

Conversation

e-mniang
Copy link
Contributor

@e-mniang e-mniang commented Jul 14, 2025

This PR adds several equational properties for padRight to Data.Vec.Properties, extending the standard vector operations toolkit with useful lemmas for reasoning about padding on the right.

Added properties:


-     padRight-lookup: accessing a padded vector retrieves the original values at valid indices

-     padRight-map : padRight commutes with map

-     padRight-zipWith : padRight commutes with zipWith

-     padRight-zipWith₁: generalizes padRight-zipWith for different vector lengths

-     padRight-take: recovers the original prefix with take

-     padRight-drop: the suffix added by padding equals replicate

-     padRight-updateAt: updates on padded vectors correspond to updates on the original vectors

Each property is proven by structural induction and uses standard lemmas such as zipWith-replicate, map-replicate, and inject≤.


Authored by : @jmougeot

@e-mniang e-mniang changed the title Add padRight properties to Data.Vec.Properties [Add] padRight properties to Data.Vec.Properties Jul 14, 2025
@jamesmckinna
Copy link
Contributor

jamesmckinna commented Jul 15, 2025

See also: #2770 . Even if the types of the Base operations are not (yet) changed, their properties should, where possible, be written to reflect that they only make irrelevant use of their m ≤ n arguments... UPDATED hmm, but it's not quite as simple as I'd hoped (and suggested as changes) unless we also make the changes proposed in #2770 which allow padRight to reduce more eagerly under weaker assumptions about the proofs of m ≤ n...

That being the case, I'll shout out to @JacquesCarette as to whether we go for this PR as is, and refactor downstream, or mark this blocking on #2770 ?

UPDATED: see also #2787

@jamesmckinna
Copy link
Contributor

I should have minded my manners better, and thanked you for the PR before piling in with my nitpicks! These are all, in whatever form they eventually take, a useful contribution... and since padRight goes hand-in-hand with truncate, we should perhaps welcome a follow-up PR with the corresponding lemmas for truncate too?

Copy link
Contributor Author

@e-mniang e-mniang left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi!
Thanks for your comments! I've made the necessary changes based on your feedback. I just had a small issue with the last point — the irrelevant part of the type signature.
Looking forward to your review of this version!

Great idea for the lemmas for truncate, will definitely look into that!

Copy link
Contributor

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

More nitpicks, I'm afraid, but otherwise looks good to go...
... but you'll need to write CHANGELOG entries as well. Suggest you do this once the reset after the v2.3 release is complete, though...

... UPDATED which has now taken place. So, if you look at CHANGELOG.md, you'll see under Additions to existing modules... please add the lemma names with their types, and you can see existing versions under eg CHANGELOG/v2.2.md to see formatting conventions etc.

@jamesmckinna jamesmckinna added this to the v2.4 milestone Jul 20, 2025
@jamesmckinna
Copy link
Contributor

jamesmckinna commented Aug 2, 2025

As I already wrote on #2795 ...
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.

UPDATED: I resolved the merge conflicts (which were easy), so I'll re-review, but this looks good now.

Copy link
Contributor

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good now
(I'd still change the m, n, o order in padRight-zipWith₁, but hey...)

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Aug 3, 2025
@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Aug 5, 2025
Merged via the queue into agda:master with commit 08bc2b8 Aug 5, 2025
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants