summaryrefslogtreecommitdiff
path: root/theories/Vectors
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Vectors')
-rw-r--r--theories/Vectors/Fin.v10
-rw-r--r--theories/Vectors/Vector.v12
-rw-r--r--theories/Vectors/VectorDef.v22
-rw-r--r--theories/Vectors/VectorEq.v10
-rw-r--r--theories/Vectors/VectorSpec.v39
-rw-r--r--theories/Vectors/vo.itarget5
6 files changed, 70 insertions, 28 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 17:52:30 +0000