Port reverse lemmas to Data.Vec (fixes #942)

[jamesmckinna]

Up to, but not including, those lemmas of Andreas which would require heterogeneous equality.
And the CHANGELOG...

[jamesmckinna]

I renamed idIsFold to ``idIsFoldr`: suggest possible deprecation warning neded?

[MatthewDaggitt]

Awesome work! Added some thoughts 😄

[jamesmckinna]

Many thanks for the fine-toothed comb! Agree, there are lots of things which need improvement/reworking esp. wrt implicit/explicit arguments, so I'm grateful for your second look. I'll try to do that slowly over the next few days.

And yes, there is a reason (those scary types!) why these lemmas were not low-hanging fruit, and I'm still not entirely satisfied with the current formulation. But I would rather these were merged and then had a chance for others to look/play, before any further drastic reorganisation, eg merging the lemmas in from WithK, which I am sure could be ported to the Heterogeneous developing without having to appeal to K...

[MatthewDaggitt]

A few more (minor) comments

[MatthewDaggitt]

In general I think we're not very consistent about whether we call such properties map-++ or map-++-commute. I think the majority of properties go with the former, and it's also slightly shorter, and I haven't come across any places where the naming scheme breaks down, so I would probably go with the map-++ variety if we can?

Obviously if people have a different opinion happy to hear them!

[jamesmckinna]

Fair enough. As with some of the other style comments above, I think I found myself attempting, not always faithfully, to emulate the naming conventions of Data.List.Properties... and I confess I'd prefer short names if possible, but your remark about reverse-foldr etc. had me wondering, in such a 'commute'/'complex=>simple' unfolding, which order even the commuting operations should be named. I had also wondered whether (see Data.Vec.Base for example) whether reorganising this file so that everything was stated in terms of foldr and foldl might be a good idea, or a terrible one...

[jamesmckinna]

Hmm. Originally, there was also a sum-++-commute... another deprecation opportunity?
Edited: sum-++-commute now deprecated in favour of sum-++.

[MatthewDaggitt]

Yes, in a perfect world we would be consistent about the ordering as well. I think lets hold off any reorganisation in terms of foldr and foldl for at least in this PR!

[MatthewDaggitt]

I think it's probably readable the way you have it at the moment 👍

[jamesmckinna]

But see my comment above. BTW, _∷ʳ_ was already defined; it was the foldl-based definition of _ʳ++_ which had me reconsidering those functions defined as foldrs... towards some grand (folly of a) general foldl/foldr commutation result.

[jamesmckinna]

So here's a strange thing: I was doing some more reorganising, to try to see if unfold-reverse and unfold-ʳ++ could be rewritten in terms of foldr-reverse (you'd think, right? at least in view of the above ;-)) and find myself in a situation where agda seems reluctant to unfold the recursion equations for foldl correctly, even with every argument fully written out... starting to wonder if there is a bug?

[jamesmckinna]

Or then again, it perhaps would require _∷ʳ_ to be written as a foldr for that idea to work... instead of being, clause for clause, identical to a foldr instance... hmmm.

[jamesmckinna]

Above conjecture correct. So... functions defined by pattern-matching are not intensionally equal to (suitable instances of slightly more higher-order) functions with the same pattern-matching behaviour. Hmmm. Generativity bites again? Oh well.

[jamesmckinna]

And... List.Properties again leads the way with a bunch of *-is-foldr lemmas. I'll leave those to another day perhaps

[JacquesCarette]

(For when you get back to Heterogeneous: Data.Fin.cast can be your friend, because it computers. subst is evil and not a good way to do anything.)

[jamesmckinna]

OK, thanks @JacquesCarette for the tip... but you might need to make the hint more explicit. As it is, I end up using subst only in two/three places: once/twice to show the equivalence of xs [ m ]≡ᵥ[ n ] ys with the transport definition on the Sigma-type, and only once 'in anger', to resolve the very painful 'unfolding reverse-append on cons' lemma

ʳ++-∷ : ∀ {m n} y (xs : Vec A m) {ys : Vec A n} →
        (xs ʳ++ (y ∷ ys)) [ m + suc n ]≡ᵥ[ suc m + n ] ((y ∷ xs) ʳ++ ys)

I take, reading between the lines, @MatthewDaggitt 's hint that much of what was in Heterogeneous a) belongs elsewhere (but nailing that down precisely is making me scratch my head a bit), and b) only a fraction is actually new (to do with _ʳ++_...), or c) even requires explicit index arithmetic (the above result may be the only one; all the rest seem to come 'for free'). That leaves the equational reasoning syntax, and I'm not quite sure where that belongs, either (or if it clashes with/is made redundant by existing usage)

So if you can see a way to prove the above lemma without appealing to subst... I'd welcome a nudge!
Happy New Year! (This won't get fixed before then ;-))

[JacquesCarette]

cast is basically a subst that computes -- see https://agda.zulipchat.com/#narrow/stream/238741-general/topic/subst.20puzzle for the originating discussion, suitable for when you're fighting with weird Fin lemmas that also struggle with Nat equalities.

For your ≡ᵥ, have you considered parametrizing the equality not by 2 (explicit) numbers, but instead by 2 implicit numbers and 1 explicit proof that they are equal? That's what I ended up doing when formalizing multicategories, and it worked rather nicely.

[MatthewDaggitt]

Thanks for all the changes @jamesmckinna. I've gone through and had a very minor tidy-up. The things I did do were:

• rename foldr₀ and foldl₀ as per the conclusions in Standardisation of folds #278 and generalise their types so that the output type can differ from the input type
• renamed unfold-reverse to reverse-::

Once the tests go green, I'll merge it in!

[jamesmckinna]

@MatthewDaggitt Happy New Year! with many thanks for all the shepherding through last year of my various PRs, not least this particular beast. Here's to many more such... ;-)

[jamesmckinna]

Oh... regarding unfold-reverse (and its friend unfold-ʳ++): I agree these two items now stick out a bit, but I had been trying to follow @gallais's precept in issue #1252 but perhaps that has not enjoyed widespread uptake? But your choice of name is also a good one... so what about its friend?

[jamesmckinna]

@JacquesCarette thanks for the suggestion regarding _[_]≡ᵥ[_]_ which I had not previously considered.

I think that my only (defensible?) reasons for introducing the new notation were:

• to experiment with introducing new syntax;
• and hence, to be able to have top-level lemma statements (moreover wanting only syntax for such statements) which draw attention to these lemmas being 'special', because they involve 'tricky' index arithmetic, with the syntax designed to expose the indices, rather than their (provable) equality;
• to see what was/might be needed for heterogeneous reasoning combinators;
• to see whether explicitly mentioning Vec A indices helped make the proofs clearer: this it didn't seem to do, or at least was not necessary, in view of the previous point.

All in all, the eventual reworking of Heterogeneous might see all of this vanish in a puff of blue smoke... although @MatthewDaggitt 's point about seeing these lemmas as instances of Relation.Binary.Pointwise.Inductive reasoning might see a role of the syntax, at least... and then your observation becomes 'too interesting' for the definitions already there.

Much food for thought, however, for which my thanks. But the mention of issue #568 above indicates that perhaps even more thought is required...

[MatthewDaggitt]

@MatthewDaggitt Happy New Year! with many thanks for all the shepherding through last year of my various PRs, not least this particular beast. Here's to many more such... ;-)

And to you too 🎉

Oh... regarding unfold-reverse (and its friend unfold-ʳ++): I agree these two items now stick out a bit, but I had been trying to follow @gallais's precept in issue #1252 but perhaps that has not enjoyed widespread uptake? But your choice of name is also a good one... so what about its friend?

Will reply in the issue #1252 but long story short, I think I'm happy the names as they are now!

[MatthewDaggitt]

Let's get this landed!

[JacquesCarette]

@jamesmckinna I'm all for exploration. Especially around where people currently pull out Heterogeneous equality (and, worse, subst) when it's not needed. I just happened to have explored this a bit myself, so I reported on what I'd learned.

Your instincts perfectly matched my previous thinking (on Permutation) where making the indices explicit (and having 2 of them, even though they are always provably equal) was key to making everything go smoothly. And failed me when I tried the same thing with multicategories.

I think the main lesson (for me) is/was that none of the constructions around permutations actually care that the two indices are the same, but they do preserve that 'sameness'. Whereas in other settings, why they are the same matters. There are, after all, n! proofs that n = n. Permutations don't care because they are exactly a record of how to shuffle things around.

In other cases, such as vector operations, 'index shuffling' matters - so recording which permutation you've used may indeed matter. At least, that's my current thinking. [It's also an insight that was there in my work with Brent Yorgey in Species a long time ago... but we got referees who didn't like Species, so it never got published. One day, people will see that there's more to the world than just polynomials...]

[jamesmckinna]

Thanks @JacquesCarette for the reinforcement of the lessons imparted in issue #1610... on which I (still) need to meditate. As indeed on Species... having failed to learn the lessons of Brent's "Oh My!" Pearl a few years back.

Regarding Data.Fin.cast: none of the proofs I wrote paid any attention to the structure of Fin n; rather the indices are 'merely' vanilla ℕaturals, so I (had) hope(d) to have avoided any more subtle considerations of Fin-arithmetic.

Interesting to learn, albeit second-hand, the contrasting experiences of Permutation and those for multicategories, though your account makes sense (and might the situation be any 'better'/'worse', in the sense of drawing attention to the necessary structure, in the general operadic case?).

Concretely, I still have two open questions about the Heterogeneous experiment:

• where should the results actually best go (as instances of Pointwise _≡_ reasoning, or more generally, for arbitrary (reflexive!) Pointwise _∼_;
• is there (still) any value in retaining the syntax extensions?

Happy to take this discussion offline!

[MatthewDaggitt]

Sorry I've taken so long to reply to this.

• where should the results actually best go (as instances of Pointwise ≡ reasoning, or more generally, for arbitrary >> (reflexive!) Pointwise ∼;

So everything should go to the most general place it can live. If it holds for arbitrary binary relations then it should go in the Pointwise module. If it only holds for equality then it should live in the Equality modules. You can add specialisations of the Pointwise results in the Equality modules if you like.

• is there (still) any value in retaining the syntax extensions?

Err I have to confess you can probably answer that one better than I can right now, as I haven't looked closely at these modules for a while. I suspect that you probably don't need it as much.

[jamesmckinna]

No worries, it's a slightly stake thread for me atm, so this is a 'keepalive' as much to myself as anything: OK re 'most general' policy, but I haven't had the time to investigate how general the results are; and... duly noted regarding the syntax extensions, although are the 'usual' ≡-Reasoning combinators available for arbitrary refl, sym, trans, relations, or only for _≡_? (I suppose that in part depends on answers such as 'reflexive wrt what underlying setoid 'equality'', as well as whether they make sense for heterogeneous relations... it seems as though they should; nothing special about Vec here, I think?)

[MatthewDaggitt]

Yes, reasoning combinators are available over many arbitrary binary relations, see the Relation.Binary.Reasoning subfolder. However there also reasoning over heterogeneous equality here, but as you point out, it's only over a very specific propositional equality. I guess it should be possible to generalise your heterogeneous reasoning combinators over an indexed setoid from Relation.Binary.Indexed?