From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Vectors/Fin.v        | 10 ++++++----
 theories/Vectors/Vector.v     | 12 +++++++-----
 theories/Vectors/VectorDef.v  | 22 ++++++++++++++++------
 theories/Vectors/VectorEq.v   | 10 ++++++----
 theories/Vectors/VectorSpec.v | 39 +++++++++++++++++++++++++++++++++++----
 theories/Vectors/vo.itarget   |  5 -----
 6 files changed, 70 insertions(+), 28 deletions(-)
 delete mode 100644 theories/Vectors/vo.itarget

(limited to 'theories/Vectors')

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 2955184f..4088843a 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Arith_base.
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
index 672858fa..08158769 100644
--- a/theories/Vectors/Vector.v
+++ b/theories/Vectors/Vector.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Vectors.
@@ -21,4 +23,4 @@ Require VectorSpec.
 Require VectorEq.
 Include VectorDef.
 Include VectorSpec.
-Include VectorEq.
\ No newline at end of file
+Include VectorEq.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 1f8b76cb..f6f3cafa 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Definitions of Vectors and functions to use them
@@ -147,6 +149,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).
@@ -295,12 +307,10 @@ End VECTORLIST.
 Module VectorNotations.
 Delimit Scope vector_scope with vector.
 Notation "[ ]" := [] (format "[ ]") : vector_scope.
-Notation "[]" := [] (compat "8.5") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
 Notation "[ x ]" := (x :: []) : vector_scope.
 Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
-Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope.
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
 Open Scope vector_scope.
 End VectorNotations.
diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v
index 04c57073..317f3f1c 100644
--- a/theories/Vectors/VectorEq.v
+++ b/theories/Vectors/VectorEq.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Equalities and Vector relations
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index c5278b91..34dbaf36 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Proofs of specification for functions defined over Vector
@@ -122,3 +124,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.
+
diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget
deleted file mode 100644
index 779b1821..00000000
--- a/theories/Vectors/vo.itarget
+++ /dev/null
@@ -1,5 +0,0 @@
-Fin.vo
-VectorDef.vo
-VectorSpec.vo
-VectorEq.vo
-Vector.vo
-- 
cgit v1.2.3