Port Andreas' work on reverseAcc to vectors too

[gallais]

Vectors in the stdlib could benefit from the work done by @andreasabel in #899.
Looks like we have none of the properties of reverse for vectors.

(Some may be hard to prove because of the nat index? So I will not tag this
one as a low-hanging-fruit)

[jamesmckinna]

I had a quick look at this over the weekend.
There are two issues: on (much) easier to deal with than the other:

• the 'usual' problem with suc m + n ≡ m + suc n etc. in concrete instances of indices in proofs; this can (must?) be solved by introducing heterogeneous equality on vectors... etc. (or have things improved since the 1990s?); I played around with a version of this which cooperates nicely with subst/transport ideas;
• much worse, IMHO, esp. with instances of (dependent!) foldl: the functions reflecting the indices in these proofs for the associated return type families such as λ n → Vec A (m + suc n) and λ n → Vec A (suc m + n) also need to be coerced between...
  Ie. it's not enough for the individual (heterogeneous) equations to be correctly stated to permit equal-but-not-convertible indices, but the functions-as-folds themselves need to be appropriately massaged to support the extensional comparison of functions whose return types are only extensionally equal. The latter proved very much to not be low-hanging fruit... unless I am missing a trick in terms of a (much) more general (and much more grandiose) statement about the universality of foldr/l than what is currently there... which is presumably why Ohad and friends (and you!) are working so hard on frex as a solution to this kind of thing. Any likelihood of a grand unification between Tactic.*Solver and frex-based methods anytime soon? ;-)

[jamesmckinna]

Up to the CHANGELOG.md, I now have a branch issue942 which would close this, apart from the lemmas which Andreas proved which would require heteregeneous equality to be type-correct. These lemmas could go in Data.Vec.Properties.WithK, but there is still something to do to finish their proofs. I've opened PR #1668 for discussion/review.

[jamesmckinna]

Pushed instead to Data.Vec.Properties.Heterogeneous, as no dependency on --with-K.
But the proofs need a lot of tidying up!

[jamesmckinna]

Latest commits indeed tidy (most) things up, including new syntax for heterogeneous equality on Vec, together with ≡ᵥ-Reasoning by analogy with ≡-Reasoning. Some of the proofs still a bit ugly, though.

[jamesmckinna]

This issue, and the (seemingly un-) related issue #602 point to a lack of systematically keeping Properties in sync between Data.List and Data.Vec. The un-smart way is to reduplicate effort (although that has its own satisfactions), the smart way might be a (much?) more ambitious approach via ornamentation. Consider opening a generic issue about this?