First release of Vector library.

To avoid names&notations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.

SetoidVector at least remains to do.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 20 insertions, 175 deletions

diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 694ed15b4..0c2181638 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -9,6 +9,8 @@
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
 Require Export Bool Sumbool.
+Require Vector.
+Export Vector.VectorNotations.
 Require Import Minus.
 
 Open Local Scope nat_scope.
@@ -27,161 +29,6 @@ as definition, since the type inference mechanism for pattern-matching
 is sometimes weaker that the one implemented for elimination tactiques.
 *)
 
-Section VECTORS.
-
-(**
-A vector is a list of size n whose elements belongs to a set A.
-If the size is non-zero, we can extract the first component and the
-rest of the vector, as well as the last component, or adding or
-removing a component (carry) or repeating the last component at the
-end of the vector.
-We can also truncate the vector and remove its p last components or
-reciprocally extend the vector by concatenation.
-A unary function over A generates a function on vectors of size n by
-applying f pointwise.
-A binary function over A generates a function on pairs of vectors of
-size n by applying f pointwise.
-*)
-
-Variable A : Type.
-
-Inductive vector : nat -> Type :=
-  | Vnil : vector 0
-  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
-
-Definition Vhead (n:nat) (v:vector (S n)) :=
-  match v with
-  | Vcons a _ _ => a
-  end.
-
-Definition Vtail (n:nat) (v:vector (S n)) :=
-  match v with
-  | Vcons _ _ v => v
-  end.
-
-Definition Vlast : forall n:nat, vector (S n) -> A.
-Proof.
-  induction n as [| n f]; intro v.
-  inversion v.
-  exact a.
-
-  inversion v as [| n0 a H0 H1].
-  exact (f H0).
-Defined.
-
-Fixpoint Vconst (a:A) (n:nat) :=
-  match n return vector n with
-  | O => Vnil
-  | S n => Vcons a _ (Vconst a n)
-  end.
-
-(** Shifting and truncating *)
-
-Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
-Proof.
-  induction n as [| n f]; intro v.
-  exact Vnil.
-
-  inversion v as [| a n0 H0 H1].
-  exact (Vcons a n (f H0)).
-Defined.
-
-Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
-Proof.
-  induction n as [| n f]; intros a v.
-  exact (Vcons a 0 v).
-
-  inversion v as [| a0 n0 H0 H1 ].
-  exact (Vcons a0 (S n) (f a H0)).
-Defined.
-
-Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)).
-Proof.
-  induction n as [| n f]; intro v.
-  inversion v.
-  exact (Vcons a 1 v).
-
-  inversion v as [| a n0 H0 H1 ].
-  exact (Vcons a (S (S n)) (f H0)).
-Defined.
-
-Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p).
-Proof.
-  induction p as [| p f]; intros H v.
-  rewrite <- minus_n_O.
-  exact v.
-
-  apply (Vshiftout (n - S p)).
-
-  rewrite minus_Sn_m.
-  apply f.
-  auto with *.
-  exact v.
-  auto with *.
-Defined.
-
-(** Concatenation of two vectors *)
-
-Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) :=
-  match v with
-  | Vnil => w
-  | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w)
-  end.
-
-(** Uniform application on the arguments of the vector *)
-
-Variable f : A -> A.
-
-Fixpoint Vunary n (v:vector n) : vector n :=
-  match v with
-  | Vnil => Vnil
-  | Vcons a n' v' => Vcons (f a) n' (Vunary n' v')
-  end.
-
-Variable g : A -> A -> A.
-
-Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
-Proof.
-  induction n as [| n h]; intros v v0.
-  exact Vnil.
-
-  inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
-  exact (Vcons (g a a0) n (h H0 H2)).
-Defined.
-
-(** Eta-expansion of a vector *)
-
-Definition Vid n : vector n -> vector n :=
-  match n with
-  | O => fun _ => Vnil
-  | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v)
-  end.
-
-Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
-Proof.
-  destruct v; auto.
-Qed.
-
-Lemma VSn_eq :
-  forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v).
-Proof.
-  intros.
-  exact (Vid_eq _ v).
-Qed.
-
-Lemma V0_eq : forall (v : vector 0), v = Vnil.
-Proof.
-  intros.
-  exact (Vid_eq _ v).
-Qed.
-
-End VECTORS.
-
-(* suppressed: incompatible with Coq-Art book
-Implicit Arguments Vnil [A].
-Implicit Arguments Vcons [A n].
-*)
-
 Section BOOLEAN_VECTORS.
 
 (**
@@ -197,38 +44,38 @@ NOTA BENE: all shift operations expect predecessor of size as parameter
 (they only work on non-empty vectors).
 *)
 
-Definition Bvector := vector bool.
+Definition Bvector := Vector.t bool.
 
-Definition Bnil := @Vnil bool.
+Definition Bnil := @Vector.nil bool.
 
-Definition Bcons := @Vcons bool.
+Definition Bcons := @Vector.cons bool.
 
-Definition Bvect_true := Vconst bool true.
+Definition Bvect_true := Vector.const true.
 
-Definition Bvect_false := Vconst bool false.
+Definition Bvect_false := Vector.const false.
 
-Definition Blow := Vhead bool.
+Definition Blow := @Vector.hd bool.
 
-Definition Bhigh := Vtail bool.
+Definition Bhigh := @Vector.tl bool.
 
-Definition Bsign := Vlast bool.
+Definition Bsign := @Vector.last bool.
 
-Definition Bneg := Vunary bool negb.
+Definition Bneg n (v : Bvector n) := Vector.map negb v.
 
-Definition BVand := Vbinary bool andb.
+Definition BVand n (v : Bvector n) := Vector.map2 andb v.
 
-Definition BVor := Vbinary bool orb.
+Definition BVor n (v : Bvector n) := Vector.map2 orb v.
 
-Definition BVxor := Vbinary bool xorb.
+Definition BVxor n (v : Bvector n) := Vector.map2 xorb v.
 
 Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
-  Bcons carry n (Vshiftout bool n bv).
+  Bcons carry n (Vector.shiftout bv).
 
 Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
-  Bhigh (S n) (Vshiftin bool (S n) carry bv).
+  Bhigh (S n) (Vector.shiftin carry bv).
 
 Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
-  Bhigh (S n) (Vshiftrepeat bool n bv).
+  Bhigh (S n) (Vector.shiftrepeat bv).
 
 Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
@@ -250,5 +97,3 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
 
 End BOOLEAN_VECTORS.
 
-Implicit Arguments Vcons [[A] [n]] [].
-Implicit Arguments Vnil [[A]] [].
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 6550a4955..6872eaea3 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -45,4 +45,4 @@ Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
 destruct b; intro H.
 left; inversion H; auto with bool.
 right; inversion H; auto with bool.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 942607faf..73a092143 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -66,4 +66,4 @@ Definition bool_of_sumbool :
   intros A B H.
   elim H; intro; [exists true | exists false]; assumption.
 Defined.
-Implicit Arguments bool_of_sumbool.
\ No newline at end of file
+Implicit Arguments bool_of_sumbool.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index a7c739625..bac4c0d69 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -37,4 +37,4 @@ Hint Resolve zerob_false_intro: bool.
 Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
 Proof.
   destruct n; [ inversion 1 | auto with bool ].
-Qed.
\ No newline at end of file
+Qed.