Proofs in Data.Vec.Properties take general properties as inputs

[mildsunrise]

Looking at Data.Vec.Properties, I see many properties accept an irrelevant eq parameter that is actually a well-known property on naturals and has nothing relevant to the particular input. For example:

++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
++-∷ʳ {m = zero}  eq z []       []       = refl
++-∷ʳ {m = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
++-∷ʳ {m = suc m} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)

Instead of requesting a proof for suc (m + n) ≡ m + suc n, we could fill it in ourselves with +-suc which is already in scope:

++-∷ʳ : ∀ z (xs : Vec A m) (ys : Vec A n) → let eq = sym (+-suc m n) in
        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
++-∷ʳ {m = zero}  z []       []       = refl
++-∷ʳ {m = zero}  z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ′ z [] ys)
++-∷ʳ {m = suc m} z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ′ z xs ys)

This not only makes ++-∷ʳ easier to use, it also simplifies the code for the proof itself (no extra eq argument, no need for refl and cong pred eq). And because eq is irrelevant in cast, we don't lose generality -- the original statement is just const ++-∷ʳ:

++-∷ʳ′ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
         cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
++-∷ʳ′ _ = ++-∷ʳ

So I wanted to ask, what's the motivation for writing properties the current way? Was it because of limitations of Agda back when these proofs were written (wrt irrelevancy and so on)? Am I myself missing limitations of irrelevancy or something else? Later in the file I can see properties that use the second style:

fromList-reverse : (xs : List A) → cast (List.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)

And the follow up question is: would it be a good idea to change the properties to the second style in the next compat-breaking version?

[jamesmckinna]

Great question!
See the discussion on #2067 ... but, given that equality on Nat is irrelevant, I can't think of a good argument against your approach... but this is something we have also discussed in the context of (picking specific witnesses to) irrelevant instance resolution, so shout outs to @MatthewDaggitt and @JacquesCarette for their input...

[mildsunrise]

thanks for the link! I took a quick look at all of the comments and threads and was unable to find discussion on the eq, and from what I see, this style of proof predates #2067. later I'll take a deeper look :)

also as an offtopic, shout out to @shhyou for the reasoning system, it is really nice documented and a pleasure to use!

[jamesmckinna]

Thinking a little bit more about your question... it seems to me that

• the 'library of combinators' approach does (seem to) mean/require that properties all be stated in a particular stereotyped form cast eq xs ≡ ys
• so, while individual lemmas might permit your trick/simplification to work, the general case will/might not work in general
• for your particular example, and others, it might be good to offer an eq-free derived form, as potentially more usable?

[mildsunrise]

the 'library of combinators' approach does (seem to) mean/require that properties all be stated in a particular stereotyped form cast eq xs ≡ ys

hmm, I'm struggling to see where the conflict is here 🤔 the style I'm suggesting doesn't change the fact that properties are stated as cast eq xs ≡ ys, it just means the user doesn't have to provide an eq to get the proof.

so, while individual lemmas might permit your trick/simplification to work, the general case will/might not work in general

do you have an example of a lemma that might not permit the second style? I was able to rewrite all proofs in Vec.Properties to the second style without an issue, even ones that use the combinators (such as reverse-++). also bear in mind we have many proofs already using the second style!

for your particular example, and others, it might be good to offer an eq-free derived form, as potentially more usable?

agreed. I would in fact derive the eq-taking (current) form from the eq-free form, as I did above, as it also simplifies the code a bit

[shhyou]

I think providing proofs of eqs in the lemmas is going to be a nice improvement.

When I originally added some of the cast proofs, I did not think that much and simply followed the patterns of existing lemmas. In the old proofs, some eqs exist since they are inevitable. Here are some examples:

cast-∷ʳ : ∀ .(eq : suc n ≡ suc m) x (xs : Vec A n) →
          cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x

cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
           cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys

cast-++ʳ : ∀ .(eq : n ≡ o) (xs : Vec A m) {ys : Vec A n} →
           cast (cong (m +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys

lookup-cast : .(eq : m ≡ n) (xs : Vec A m) (i : Fin m) →
              lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i

Of course, these are not the cases for the lemmas you observed. From what I can see, for example, these properties can also have their eq proofs be specialized to +-assoc and +-identityʳ from Data.Nat.Properties since they are irrelevant in cast anyway:

++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
           cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)

++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs

[shhyou]

Naming the revised lemmas with primes (like ∷ʳ-++′) is quite inconvenient. Are they going to just replace the old ones in some major version (like v3.0)?

[MatthewDaggitt]

There is a good reason for having the proofs be irrelevant and generic in the exact equality. The problem is that if you hard code the equality (e.g. by using the corresponding property from Data.Nat.Properties) then if you have a different proof of the equality then you suddenly become unable to use the lemma without a terribly convoluted subst.

These lemmas were ported across from my own library, where I frequently came across places where for various reasons (e.g. the equality was sourced from another related equality upstream with a different proof, and only reduced to suc (m + n) ≡ m + suc n locally) I had no control over the equality at that spot.

If people think that having the instantiated equality would be useful, then yes, it would be possible to add additional lemmas. I'm agnostic to the naming of those, i.e. would be happy with primed versions, but if someone can come up with a more meaningful version then we'd be keen to hear suggestions.

[mildsunrise]

From what I can see, for example, these properties can also have their eq proofs be specialized to +-assoc and +-identityʳ from Data.Nat.Properties since they are irrelevant in cast anyway

yeah, those are handled in the rewrite

Naming the revised lemmas with primes (like ∷ʳ-++′) is quite inconvenient. Are they going to just replace the old ones in some major version (like v3.0)?

that's what I'd like to happen as well...

[mildsunrise]

@MatthewDaggitt sorry, I missed your comment!

The problem is that if you hard code the equality (e.g. by using the corresponding property from Data.Nat.Properties) then if you have a different proof of the equality then you suddenly become unable to use the lemma without a terribly convoluted subst.

hmm, can you point to an example? I thought irrelevancy solved this... I'm probably missing something, but I've been using the eq-free lemmas for a while now and have so far never found a situation where I needed to use the eq-generic ones

in the end, I'd like us to be consistent. if there's a reason to provide eq-generic lemmas, then let's provide them everywhere (right now we have many lemmas that are eq-free) and adopt a uniform naming convention 🙏

[jamesmckinna]

Trying to navigate a path between @MatthewDaggitt and @mildsunrise ... I have the impression that both forms of the lemma statements may be useful (even: necessary), but also that the inversion of dependency which makes the eq-free ones conceptually prior, and the eq-qualified ones being given as constant functions (thanks to irrelevance), might also be a useful refactoring?

Mind you, the search for a workable, consistent, naming scheme, together with a suitable deprecation strategy of the 'old ways' of doing things suggests to me that this might best be badged as a v3.0 issue?

[shhyou]

@MatthewDaggitt A good thing is that the exact equality here doesn't block any other equalities due to eqs being irrelevant in cast. That is, it's okay for the equality-specialized lemmas to be used with arbitrary equalities.

For example, ++-identityʳ-with-eq below is using a specific equality +-identityʳ n. At the use site usage, however, eq is a different equality.

++-identityʳ-with-eq : ∀ {A : Set} {n} →
                       (xs : Vec A n) →
                       cast (+-identityʳ n) (xs ++ []) ≡ xs
++-identityʳ-with-eq {n = zero}  []       = refl
++-identityʳ-with-eq {n = suc n} (x ∷ xs) = cong (x ∷_) (++-identityʳ-with-eq xs)

usage : ∀ {A : Set} {m} (xs : Vec A m) → (eq : m + zero ≡ m) → cast eq (xs ++ []) ≡ xs
usage xs _ = ++-identityʳ-with-eq xs

In other words, equality-specific lemmas subsume the equality-agnostic ones due to irrelevancy.

[MatthewDaggitt]

hmm, can you point to an example? I thought irrelevancy solved this... I'm probably missing something, but I've been using the eq-free lemmas for a while now and have so far never found a situation where I needed to use the eq-generic ones

A good thing is that the exact equality here doesn't block any other equalities due to eqs being irrelevant in cast

Ah right, yes, we're talking about the new Vector specific version of cast, not the generic version I was thinking of. Yes, indeed the fact that the equality is irrelevant in cast means that maybe my objection isn't quite right.

@gallais as the author of these lemmas 2 years ago in a123840, do you remember why you made the equalities generic?

[gallais]

Probably because I was thinking along the same lines as you:

The problem is that if you hard code the equality (e.g. by using the corresponding property from Data.Nat.Properties) then if you have a different proof of the equality then you suddenly become unable to use the lemma

But as this discussion highlights, it was probably a mistake given that irrelevance should
indeed solve that issue.

[mildsunrise]

given that we seem to have reached a consensus, I'd suggest this course of action:

• for every eq-generic lemma we're currently providing (say ++-∷ʳ):

  • add an eq-free lemma named with a prime suffix (++-∷ʳ′)
  • deprecate the eq-generic lemma, telling users to move to the eq-free lemma
    (or report an issue if they find difficulties doing so)
  • in the next breaking version, remove the eq-generic lemma and have the eq-free lemma take its name

it's the first time I deal with deprecations, but it would look something like this. WDYT?

[jamesmckinna]

I'm in favour of the general tenor if your proposal, but really don't like the use of primes...

might even go as far as suggesting an 'obtrusive' modifier such as -eqfree, and thereby remind us all of the need to fix this sooner rather than later...? ;-)

[mildsunrise]

I like the idea of being more explicit that this is transitional, but, can we pick a suffix that's a little shorter? 👉👈

[MatthewDaggitt]

I agree with proposal except that this:

in the next breaking version, remove the eq-generic lemma and have the eq-free lemma take its name

should be:

in the next breaking version, remove the eq-generic lemma and have the eq-free lemma take its name, and deprecate the eq-free lemma.

I like the suffix eqFree (1 character shorter!). It's still much faster to type than most of the existing lemma names with loads of unicode. @mildsunrise do you have an alternative middle-ground suggestion?

[JacquesCarette]

What a wonderful discussion! My first instinct was to reply along the same lines as what @MatthewDaggitt said, as my experience of wiring in specific proofs lead to subst-hell too. But I am indeed pleased to see that proof-irrelevance is the perfect weapon to take care of that. [I'm still a big fan of proof relevance by default, but for things like the natural numbers, or anything else with decidable equality, that would be a mighty dumb hill to die on. It's not actually that simple, but that's a discussion for another day.]

[mildsunrise]

@MatthewDaggitt ah, I see, you want to do it in 2 steps, right?
in v3, ++-∷ʳ will be changed to the same lemma as ++-∷ʳ-eqFree, and then in v4 we remove ++-∷ʳ-eqFree. did I get that right?

I like the suffix eqFree (1 character shorter!). It's still much faster to type than most of the existing lemma names with loads of unicode. @mildsunrise do you have an alternative middle-ground suggestion?

I'm not feeling very creative today, so let's go with -eqFree :) later I'll prepare the PR

[jamesmckinna]

I'm not feeling very creative today, so let's go with -eqFree :)

Yes... 'rename+deprecate' PRs can slightly drain the creative life out of stdlib development.
But there is (can be?) a kind of 'raking the stones in a Zen garden' aspect to it, too...? ;-)

[MatthewDaggitt]

in v3, ++-∷ʳ will be changed to the same lemma as ++-∷ʳ-eqFree, and then in v4 we remove ++-∷ʳ-eqFree. did I get that right?

Yes, that sounds about right. Slow and steady wins the race.

[mildsunrise]

@JacquesCarette I'm still curious about

I'm still a big fan of proof relevance by default, but for things like the natural numbers, or anything else with decidable equality, that would be a mighty dumb hill to die on. It's not actually that simple, but that's a discussion for another day.

if you ever write about this in the future, I'd be happy to read it :)

[JacquesCarette]

On the 'not that simple', it starts with a simple observation: let G and H be enormous numbers (like Graham's number or TreeT(4), which are expressible in Agda but effectively impossible to write down). Then 2^G * 3^H = 3^H * 2^G is "obviously true" -- but refl is both a) an impossible-to-verify proof of that, and b) equivalent to the obvious proof (using +-comm and enough laziness) by the fact that all proofs of decidable equalities are equivalent.

So there are equalities that are provable in Agda, that are for decidable things, but where refl will never in anyone's lifetime be accepted as a valid proof.