Vector Forall Lemmas, for all!

CHANGELOG.md

@@ -3,6 +3,7 @@ API-breaking change is listed.
 
 ## std++ master
 
+- Add lemmas `Forall_vinsert` and `Forall_vreplicate`. (by Rudy Peterson)
 - Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel)
 - Add lemma `lookup_total_fmap`.
 - Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,

stdpp/vector.v

@@ -297,6 +297,12 @@ Lemma vmap_insert {A B} (f : A → B) (n : nat) i x (v : vec A n) :
   vmap f (vinsert i x v) = vinsert i (f x) (vmap f v).
 Proof. induction v; inv_fin i; intros; f_equal/=; auto. Qed.
 
+Lemma Forall_vinsert {A} (P : A → Prop) {n} (v : vec A n) (i : fin n) (x : A) :
+  Forall P (vec_to_list v) →
+  P x →
+  Forall P (vec_to_list (vinsert i x v)).
+Proof. rewrite vec_to_list_insert. apply Forall_insert. Qed.
+
 (** The functions [vtake i v] and [vdrop i v] take the first [i] elements of
 a vector [v], respectively remove the first [i] elements of a vector [v]. *)
 Fixpoint vtake {A n} (i : fin n) : vec A n → vec A i :=
@@ -333,6 +339,11 @@ Lemma vmap_replicate {A B} (f : A → B) n (x : A) :
   vmap f (vreplicate n x) = vreplicate n (f x).
 Proof. induction n; f_equal/=; auto. Qed.
 
+Lemma Forall_vreplicate {A} (P : A → Prop) n (x : A) :
+  P x →
+  Forall P (vec_to_list (vreplicate n x)).
+Proof. rewrite vec_to_list_replicate. apply Forall_replicate. Qed.
+
 (** Vectors are inhabited and countable *)
 Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#].
 Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) :=