Many, many useful proofs about vectors

[jadephilipoom]

In the course of proving specifications for various arrow combinators, I accumulated a whole bunch of general Vector.t proofs. This PR adds those to VectorUtils.v. In order to make the proofs easier, I changed some of the custom vector functions (vreverse, vsnoc, and vunsnoc) to recurse on the length of the vector, instead of on the vector itself.

The one other change here is that I took fold_left_S out of the vsimpl set of rewrite hints. The problem is that it triggers any time it sees fold_left with a length that matches S _ -- and 4 is just a notation for S (S (S (S 0))), so if you have a fold_left with length 8 it'll apply itself 8 times and make your goal huge. It's still added to the push_vector_fold set of hints, so you can get the same behavior as before by writing autorewrite with push_vector_fold vsimpl instead of just autorewrite with vsimpl, but you have more control over whether that particular lemma gets used.

[blaxill]

Lgtm! In retrospect, I think my prefixing of names was a mistake, I should have used a module, feel free to change the names here or I'll do it later.

[blaxill]

Just out of curiosity, what makes this style of definition more annoying in proof?

[jadephilipoom]

It's not so much that one is better or worse, as much as it's important that as many implementations as possible recurse in the same way (i.e. all on length, or all on vector structure). In a proof, I can choose to do either induction n or induction v, and it's nice if the same one matches all the definitions I'm reasoning about. Of course, it's possible to do proofs where you use Vector.eta to change a vector of length (S n) into hd v :: tl v and reason from there, but especially if there are multiple of the vector-recursive definition in context and the argument is a complicated expression this kind of manipulation can get tricky.