[Add] padRight properties to Data.Vec.Properties

[e-mniang]

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

[jamesmckinna]

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

Tat 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 ?

[jamesmckinna]

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?

[e-mniang]

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!

[jamesmckinna]

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]

As previously, please don't use p here, when o would conventionally be better.

Suggested change

	padRight-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) →
	padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs)
	padRight-trans : ∀ (m≤n : m ≤ n) (n≤o : n ≤ o) (a : A) (xs : Vec A m) →
	padRight (≤-trans m≤n n≤o) a xs ≡ padRight n≤o a (padRight m≤n a xs)

[jamesmckinna]

LIkewise

Suggested change

	padRight-trans z≤n n≤p a [] = padRight-replicate n≤p a
	padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs)
	padRight-trans z≤n n≤o a [] = padRight-replicate n≤o a
	padRight-trans (s≤s m≤n) (s≤s n≤o) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤o a xs)

[jamesmckinna]

Whatever else above regarding m n o/p ordering of the variables...

Suggested change

	padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))
	padRight-zipWith₁ f m≤n p≤m a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys))

Implicit p isn't even used here, so it's much better to omit it to make your code less brittle.

[jamesmckinna]

Ugh!

• p shouldn't be used here as an implicit; it's previously bound at module-level scope as a variable of type Level, while o is bound at type Nat, so use that instead
• what's the correct order of assumptions here? that m ≤ n precede p ≤ m, or that you instead order them so that m ≤ n ≤ o and then fix up the relevant assumption uses to reflect that?

[jamesmckinna]

Please don't use p here as a pattenr variable for an equation, especially given that it is already implicitly bound above at type Level... etc.
Instead use eq or the assumption name you have already chosen in the lemma statement (reduce cognitive load on the reader as the implied design heuristic here)

[jamesmckinna]

Suggested change

	padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f zero x = refl
	padRight-updateAt {n = suc n} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)
	padRight-updateAt {n = suc _} (s≤s m≤n) (y ∷ xs) f zero x = refl
	padRight-updateAt {n = suc _} (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x)

The actual n isn't used subsequently on the LHS, nor on the RHS, so omitting it in favour of a wildcard _ makes the code less brittle.

[jamesmckinna]

What's the right argument order here? A heuristic I learnt from @JacquesCarette would be: args that vary most should be rightmost, those that are invariant/vary less should be leftmost, together with the heuristic that says that argument order for lemmas should try to follow the argument order for the 'main' function being characterised, so here at least something like:

Suggested change

	padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) →
	updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
	padRight m≤n x (updateAt xs i f)
	padRight-updateAt : ∀ (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
	updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
	padRight m≤n x (updateAt xs i f)

with the position of f being moot, but perhaps should be rightmost to reflect its arg position in the function calls?

[jamesmckinna]

Alignment?

Suggested change

	cast-replicate {m = zero} {n = zero} _ _ = refl
	cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x)
	cast-replicate {m = zero} {n = zero} _ _ = refl
	cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x)