Polish contents of Util

[jadephilipoom]

Similar to #639: now that we're exporting Util/, it would be nice to clean it up a bit. This issue tracks those efforts.

• Remove experimental code and unused definitions (unused lemmas can stay)
• Write tests for all tactics
• Organize files more logically

A bit more on the last point: many files in Util (looking at you, Vector.v) contain proofs and code interleaved chaotically. Any consistent structure is a good structure, but my first suggestion for Util files would be the style in List.v, with a separate section for each definition and its proofs, or just the proofs if it's from the standard library. Example snippet illustrating the pattern:

silveroak/cava/Cava/Util/List.v

Lines 164 to 227 in b0dc9fd

	Section Forall2.
	Lemma Forall2_length_eq {A B} (R : A -> B -> Prop) ls1 ls2 :
	Forall2 R ls1 ls2 -> length ls1 = length ls2.
	Proof.
	revert ls2; induction ls1; destruct ls2; auto;
	inversion 1; subst; cbn [length]; auto.
	Qed.
	Lemma Forall2_eq_map_r {A B} (f : A -> B) ls1 ls2 :
	Forall2 (fun a b => a = f b) ls1 ls2 ->
	ls1 = map f ls2.
	Proof.
	revert ls2; induction ls1; destruct ls2; auto;
	inversion 1; subst; cbn [map]; f_equal; eauto.
	Qed.
	Lemma Forall2_eq_map_l {A B} (f : A -> B) ls1 ls2 :
	Forall2 (fun b a => a = f b) ls1 ls2 ->
	ls2 = map f ls1.
	Proof.
	revert ls2; induction ls1; destruct ls2; auto;
	inversion 1; subst; cbn [map]; f_equal; eauto.
	Qed.
	End Forall2.
	Hint Resolve Forall2_length_eq : length.
	(* Definition and proofs of [extend], which pads a list to a specified length *)
	Section Extend.
	Definition extend {A} (l : list A) (d : A) (n : nat) : list A :=
	l ++ repeat d (n - length l).
	Lemma extend_nil {A} (d : A) n : extend [] d n = repeat d n.
	Proof. cbv [extend]. autorewrite with push_length natsimpl. reflexivity. Qed.
	Lemma extend_cons_S {A} x0 x (d : A) n :
	extend (x0 :: x) d (S n) = x0 :: extend x d n.
	Proof.
	cbv [extend]. autorewrite with push_length natsimpl.
	rewrite <-app_comm_cons; reflexivity.
	Qed.
	Lemma extend_le {A} l (d : A) n : n <= length l -> extend l d n = l.
	Proof.
	cbv [extend]; intros.
	rewrite (proj2 (Nat.sub_0_le _ _)) by lia.
	cbn [repeat]; autorewrite with listsimpl.
	reflexivity.
	Qed.
	Lemma extend_to_match {A B} l1 l2 (a : A) (b : B) :
	length (extend l1 a (length l2)) = length (extend l2 b (length l1)).
	Proof.
	cbv [extend]; intros. autorewrite with push_length.
	destruct (Nat.min_dec (length l1) (length l2));
	autorewrite with natsimpl; lia.
	Qed.
	Lemma extend_length {A} (l : list A) a n:
	length (extend l a n) = Nat.max (length l) n.
	Proof.
	cbv [extend]. autorewrite with push_length natsimpl.
	lia.
	Qed.
	End Extend.

[blaxill]

At this point we have cava2 succeeding cava but depending on it for Cava/Util. AFAIK Cava/Util has no dependencies and could be made into a standalone library.

[jadephilipoom]

At this point we have cava2 succeeding cava but depending on it for Cava/Util. AFAIK Cava/Util has no dependencies and could be made into a standalone library.

There's already an issue for this: #914