2 files changed, 39 insertions, 0 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 1f8b76cb6..c49451776 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -147,6 +147,16 @@ Definition shiftrepeat {A} := @rectS _ (fun n _ => t A (S (S n)))
   (fun h =>  h :: h :: []) (fun h _ _ H => h :: H).
 Global Arguments shiftrepeat {A} {n} v.
 
+(** Take first [p] elements of a vector *)
+Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := 
+  match p as p return p <= n -> t A p with 
+  | 0 => fun _ => [] 
+  | S p' => match v in t _ n return S p' <= n -> t A (S p') with
+    | []=> fun le => False_rect _ (Nat.nle_succ_0 p' le)
+    | x::xs => fun le => x::take p' (le_S_n p' _ le) xs
+    end 
+  end le.
+
 (** Remove [p] last elements of a vector *)
 Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
   -> t A (n - p).
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index c5278b918..869d0fb5a 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -122,3 +122,32 @@ induction l.
 - reflexivity.
 - unfold to_list; simpl. now f_equal.
 Qed.
+
+Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = [].
+Proof. 
+  reflexivity.
+Qed. 
+
+Lemma take_idem : forall {A} p n (v:t A n)  le le', 
+  take p le' (take p le v) = take p le v.
+Proof. 
+  induction p; intros n v le le'.
+  - auto. 
+  - destruct v. inversion le. simpl. apply f_equal. apply IHp. 
+Qed.
+
+Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v.
+Proof. 
+  induction v; intros m w le.
+  - reflexivity. 
+  - simpl. apply f_equal. apply IHv. 
+Qed.
+
+(* Proof is irrelevant for [take] *)
+Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v.
+Proof. 
+  induction p; intros n v le le'. 
+  - reflexivity.  
+  - destruct v. inversion le. simpl. apply f_equal. apply IHp. 
+Qed.
+