Separate/upstream Util directory

[jadephilipoom]

Some relevant discussion in #910

Right now, we have a lot of code in cava/Cava/Util that is not specific to our project. That means our dependency structure is a little strange; a lot of things that are defined in cava2 have dependencies on cava/ anyway because they use the Util files. Restructuring our directories so that Util is a separate library that cava and cava2 both depend on will simplify this and speed up our CI.

Additionally, some of the stuff in Util might be useful for other Coq projects, especially the list/vector lemmas and some of the tactics. If we want to be good open-source citizens, we could upstream some of those things to coqutil (it would be good to address #896 first, because the list/vector infrastructure makes heavy use of autorewrite).

[samuelgruetter]

Regarding upstreaming to coqutil, that'd be very welcome, I think. I'm just not sure about vector lemmas, I think neither @andres-erbsen nor myself endorse usage of dependently typed vectors, so we might want to keep them out of coqutil.

[jadephilipoom]

Fair enough about the vector lemmas -- I agree it might do people a disservice to point them in that direction.

[andres-erbsen]

coqutil also already has primitive tuples and hlists, so it's not like we have a principled record of favoring less dependent types. But I do pretty much agree with the impression one would get from rocq-prover/stdlib#54 regarding stdlib vectors. 🤷

[jadephilipoom]

We since moved away from vectors on this project because of those issues. In the meantime, we did write some things that make standard library vectors more sane to work with (for instance, the example in that issue, rev (rev x), works fine with the alternate definition, reverse, that we've defined, which recurses on the length of the vector instead of using eq_rect_r nonsense):

Compute (rev (rev [1;2;3])). (* huge ugly expression with proof terms *)
Compute (reverse (reverse [1;2;3])). (* [1; 2; 3] *)

The proof for the general case is also totally reasonable (and in our library), goes by simple induction on length. We have a definition called resize_default which resizes a vector by padding/truncating it and rewrites to the identity in proofs if the lengths are equal (used for, for instance, changing a vector of length n+m to a vector of length m+n in a way that doesn't wreck computation). My general stance here is that standard library vectors are best avoided, but that if someone is already committed to using them we've developed some useful tools that make them easier. I'm not sure there's a good way to communicate "don't use this unless you really have to", though, so happy to leave them out.

I think in an ideal world, the best way to upstream the work we've done on vectors would be to write a new vector library in coqutil that replaces the standard library one, has all of our lemmas/automation, and is more computation-friendly. This would probably be a much more effective "use this, not the standard library" signal, but is also considerably more work. I'm not sure I'm ready to commit to doing it, but would coqutil accept such a library if I found myself with the time/inclination?

[samuelgruetter]

I just saw that coq-ext-lib, which is used by Cava, also has its own vector, so maybe instead of writing yet another definition of vectors, that could be a place for it?

But given that we're moving from Cava1 to Cava2, which does not use vectors any more, would there still be a project using these vectors? As in, would you keep eating your own dogfood?

[jadephilipoom]

I just saw that coq-ext-lib, which is used by Cava, also has its own vector, so maybe instead of writing yet another definition of vectors, that could be a place for it?

I think coq-ext-lib is not focused on being computation-friendly, and my impression is that its main focus is to implement things that make Coq look more like Haskell for people who are approaching Coq with a Haskell background. I think it's a somewhat different purpose than coqutil, which I see (very selfishly) as providing the useful lemmas and tactics that should be in the standard library but that I'd otherwise have to define for myself every time I start a new project.

But given that we're moving from Cava1 to Cava2, which does not use vectors any more, would there still be a project using these vectors? As in, would you keep eating your own dogfood?

That's a good point -- I think there would probably be no immediate use for them. Leaning "not worth it".