Open mildsunrise opened 3 days ago
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...
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!
Thinking a little bit more about your question... it seems to me that
cast eq xs ≡ ys
eq
-free derived form, as potentially more usable?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 :thinking: 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
I think providing proofs of eq
s 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 eq
s 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
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)?
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.
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...
@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 :pray:
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?
@MatthewDaggitt A good thing is that the exact equality here doesn't block any other equalities due to eq
s 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.
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 https://github.com/agda/agda-stdlib/commit/a1238401b42979d57b7377665438a990eca01742, do you remember why you made the equalities generic?
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.
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 ++-∷ʳ
):
++-∷ʳ′
)it's the first time I deal with deprecations, but it would look something like this. WDYT?
Looking at
Data.Vec.Properties
, I see many properties accept an irrelevanteq
parameter that is actually a well-known property on naturals and has nothing relevant to the particular input. For example: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:This not only makes
++-∷ʳ
easier to use, it also simplifies the code for the proof itself (no extraeq
argument, no need forrefl
andcong pred eq
). And becauseeq
is irrelevant incast
, we don't lose generality -- the original statement is justconst ++-∷ʳ
: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:
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?