Imported Upstream version 8.5~beta1+dfsg

6 files changed, 271 insertions, 134 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index a5e37f34..b9bf6c7f 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -8,13 +8,14 @@
 
 Require Arith_base.
 
-(** [fin n] is a convinient way to represent \[1 .. n\]
+(** [fin n] is a convenient way to represent \[1 .. n\]
 
-[fin n] can be seen as a n-uplet of unit where [F1] is the first element of
-the n-uplet and [FS] set (n-1)-uplet of all the element but the first.
+[fin n] can be seen as a n-uplet of unit. [F1] is the first element of
+the n-uplet. If [f] is the k-th element of the (n-1)-uplet, [FS f] is the
+(k+1)-th element of  the n-uplet.
 
    Author: Pierre Boutillier
-   Institution: PPS, INRIA 12/2010-01/2012
+   Institution: PPS, INRIA 12/2010-01/2012-07/2012
 *)
 
 Inductive t : nat -> Set :=
@@ -23,76 +24,68 @@ Inductive t : nat -> Set :=
 
 Section SCHEMES.
 Definition case0 P (p: t 0): P p :=
-  match p as p' in t n return
-    match n as n' return t n' -> Type
-  with |0 => fun f0 => P f0 |S _ => fun _ => @ID end p'
-  with |F1 _ => @id |FS _ _ => @id end.
+  match p with | F1 | FS  _ => fun devil => False_rect (@IDProp) devil (* subterm !!! *) end.
 
-Definition caseS (P: forall {n}, t (S n) -> Type)
-  (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
-  {n} (p: t (S n)): P p :=
+Definition caseS' {n : nat} (p : t (S n)) : forall (P : t (S n) -> Type) 
+  (P1 : P F1) (PS : forall (p : t n), P (FS p)), P p :=
   match p with
-  |F1 k => P1 k
-  |FS k pp => PS pp
+  | @F1 k => fun P P1 PS => P1
+  | FS pp => fun P P1 PS => PS pp
   end.
 
+Definition caseS (P: forall {n}, t (S n) -> Type)
+  (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
+  {n} (p: t (S n)) : P p := caseS' p P (P1 n) PS.
+
 Definition rectS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t (S n)), P p -> P (FS p)):
   forall {n} (p: t (S n)), P p :=
 fix rectS_fix {n} (p: t (S n)): P p:=
   match p with
-  |F1 k => P1 k
-  |FS 0 pp => case0 (fun f => P (FS f)) pp
-  |FS (S k) pp => PS pp (rectS_fix pp)
+  | @F1 k => P1 k
+  | @FS 0 pp => case0 (fun f => P (FS f)) pp
+  | @FS (S k) pp => PS pp (rectS_fix pp)
   end.
 
-Definition rect2 (P: forall {n} (a b: t n), Type)
-  (H0: forall n, @P (S n) F1 F1)
-  (H1: forall {n} (f: t n), P F1 (FS f))
-  (H2: forall {n} (f: t n), P (FS f) F1)
-  (HS: forall {n} (f g : t n), P f g -> P (FS f) (FS g)):
-    forall {n} (a b: t n), P a b :=
-fix rect2_fix {n} (a: t n): forall (b: t n), P a b :=
-match a with
-  |F1 m => fun (b: t (S m)) => match b as b' in t n'
-                   return match n',b' with
-                            |0,_ => @ID
-                            |S n0,b0 => P F1 b0
-                          end with
-                     |F1 m' => H0 m'
-                     |FS m' b' => H1 b'
-                   end
-  |FS m a' => fun (b: t (S m)) => match b with
-                         |F1 m' => fun aa: t m' => H2 aa
-                         |FS m' b' => fun aa: t m' => HS aa b' (rect2_fix aa b')
-                       end a'
-end.
+Definition rect2 (P : forall {n} (a b : t n), Type)
+  (H0 : forall n, @P (S n) F1 F1)
+  (H1 : forall {n} (f : t n), P F1 (FS f))
+  (H2 : forall {n} (f : t n), P (FS f) F1)
+  (HS : forall {n} (f g : t n), P f g -> P (FS f) (FS g)) :
+    forall {n} (a b : t n), P a b :=
+  fix rect2_fix {n} (a : t n) {struct a} : forall (b : t n), P a b :=
+    match a with
+    | @F1 m => fun (b : t (S m)) => caseS' b (P F1) (H0 _) H1
+    | @FS m a' => fun (b : t (S m)) =>
+      caseS' b (fun b => P (@FS m a') b) (H2 a') (fun b' => HS _ _ (rect2_fix a' b'))
+    end.
+
 End SCHEMES.
 
 Definition FS_inj {n} (x y: t n) (eq: FS x = FS y): x = y :=
 match eq in _ = a return
   match a as a' in t m return match m with |0 => Prop |S n' => t n' -> Prop end
-  with @F1 _ =>  fun _ => True |@FS _ y => fun x' => x' = y end x with
+  with F1 =>  fun _ => True |FS y => fun x' => x' = y end x with
   eq_refl => eq_refl
 end.
 
 (** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
 Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
-  match n in t k return {i | i< k} with
-    |F1 j => exist (fun i => i< S j) 0 (Lt.lt_0_Sn j)
-    |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
+  match n with
+    |@F1 j => exist _ 0 (Lt.lt_0_Sn j)
+    |FS p => match to_nat p with |exist _ i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
   end.
 
 (** [of_nat p n] answers the p{^ th} element of [fin n] if p < n or a proof of
 p >= n else *)
 Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
   match n with
-   |0 => inright _ (ex_intro (fun x => p = 0 + x) p (@eq_refl _ p))
+   |0 => inright _ (ex_intro _ p eq_refl)
    |S n' => match p with
       |0 => inleft _ (F1)
       |S p' => match of_nat p' n' with
         |inleft f => inleft _ (FS f)
-        |inright arg => inright _ (match arg with |ex_intro m e =>
+        |inright arg => inright _ (match arg with |ex_intro _ m e =>
           ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end)
       end
     end
@@ -109,13 +102,35 @@ Fixpoint of_nat_lt {p n : nat} : p < n -> t n :=
     end
   end.
 
+Lemma of_nat_ext {p}{n} (h h' : p < n) : of_nat_lt h = of_nat_lt h'.
+Proof.
+ now rewrite (Peano_dec.le_unique _ _ h h').
+Qed.
+
 Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p.
 Proof.
-induction p.
- reflexivity.
- simpl; destruct (to_nat p). simpl. subst p; repeat f_equal. apply Peano_dec.le_unique.
+induction p; simpl.
+- reflexivity.
+- destruct (to_nat p); simpl in *. f_equal. subst p. apply of_nat_ext.
+Qed.
+
+Lemma to_nat_of_nat {p}{n} (h : p < n) : to_nat (of_nat_lt h) = exist _ p h.
+Proof.
+ revert n h.
+ induction p; (destruct n ; intros h; [ destruct (Lt.lt_n_O _ h) | cbn]);
+ [ | rewrite (IHp _ (Lt.lt_S_n p n h))];  f_equal; apply Peano_dec.le_unique.
+Qed.
+
+Lemma to_nat_inj {n} (p q : t n) :
+ proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q.
+Proof.
+ intro H.
+ rewrite <- (of_nat_to_nat_inv p), <- (of_nat_to_nat_inv q).
+ destruct (to_nat p) as (np,hp), (to_nat q) as (nq,hq); simpl in *.
+ revert hp hq. rewrite H. apply of_nat_ext.
 Qed.
 
+
 (** [weak p f] answers a function witch is the identity for the p{^  th} first
 element of [fin (p + m)] and [FS (FS .. (FS (f k)))] for [FS (FS .. (FS k))]
 with p FSs *)
@@ -124,15 +139,15 @@ Fixpoint weak {m}{n} p (f : t m -> t n) :
 match p as p' return t (p' + m) -> t (p' + n) with
   |0 => f
   |S p' => fun x => match x with
-     |F1 n' => fun eq : n' = p' + m => F1
-     |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
+     |@F1 n' => fun eq : n' = p' + m => F1
+     |@FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
   end (eq_refl _)
 end.
 
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (m + n)] *)
 Fixpoint L {m} n (p : t m) : t (m + n) :=
-  match p with |F1 _ => F1 |FS _ p' => FS (L n p') end.
+  match p with |F1 => F1 |FS p' => FS (L n p') end.
 
 Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
 Proof.
@@ -145,12 +160,13 @@ Qed.
 [fin (n + m)]
 Really really ineficient !!! *)
 Definition L_R {m} n (p : t m) : t (n + m).
+Proof.
 induction n.
   exact p.
   exact ((fix LS k (p: t k) :=
     match p with
-      |F1 k' => @F1 (S k')
-      |FS _ p' => FS (LS _ p')
+      |@F1 k' => @F1 (S k')
+      |FS p' => FS (LS _ p')
     end) _ IHn).
 Defined.
 
@@ -168,8 +184,8 @@ Qed.
 
 Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
 match o with
-  |F1 m' => L (m' * n) p
-  |FS m' o' => R n (depair o' p)
+  |@F1 m' => L (m' * n) p
+  |FS o' => R n (depair o' p)
 end.
 
 Lemma depair_sanity {m n} (o : t m) (p : t n) :
@@ -182,3 +198,55 @@ induction o ; simpl.
   rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.
     now rewrite (Plus.plus_comm n).
 Qed.
+
+Fixpoint eqb {m n} (p : t m) (q : t n) :=
+match p, q with
+| @F1 m', @F1 n' => EqNat.beq_nat m' n'
+| FS _, F1 => false
+| F1, FS _ => false
+| FS p', FS q' => eqb p' q'
+end.
+
+Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
+Proof.
+intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal.
++ now apply EqNat.beq_nat_true.
++ easy.
++ easy.
++ eapply IHp. eassumption.
+Qed.
+
+Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q.
+Proof.
+apply rect2; simpl; intros.
+- split; intros ; [ reflexivity | now apply EqNat.beq_nat_true_iff ].
+- now split.
+- now split.
+- eapply iff_trans.
+ + eassumption.
+ + split.
+  * intros; now f_equal.
+  * apply FS_inj.
+Qed.
+
+Lemma eq_dec {n} (x y : t n): {x = y} + {x <> y}.
+Proof.
+ case_eq (eqb x y); intros.
+  + left; now apply eqb_eq.
+  + right. intros Heq. apply <- eqb_eq in Heq. congruence.
+Defined.
+
+Definition cast: forall {m} (v: t m) {n}, m = n -> t n.
+Proof.
+refine (fix cast {m} (v: t m) {struct v} :=
+ match v in t m' return forall n, m' = n -> t n with
+ |F1 => fun n => match n with
+   | 0 => fun H => False_rect _ _
+   | S n' => fun H => F1
+ end
+ |FS f => fun n => match n with
+   | 0 => fun H => False_rect _ _
+   | S n' => fun H => FS (cast f n' (f_equal pred H))
+ end
+end); discriminate.
+Defined.
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
index f3e5e338..672858fa 100644
--- a/theories/Vectors/Vector.v
+++ b/theories/Vectors/Vector.v
@@ -18,5 +18,7 @@ Based on contents from Util/VecUtil of the CoLoR contribution *)
 Require Fin.
 Require VectorDef.
 Require VectorSpec.
+Require VectorEq.
 Include VectorDef.
 Include VectorSpec.
+Include VectorEq.
\ No newline at end of file
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 32ffcb3d..45c13e5c 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -21,6 +21,8 @@ Require Vectors.Fin.
 Import EqNotations.
 Local Open Scope nat_scope.
 
+(* Set Universe Polymorphism. *)
+
 (**
 A vector is a list of size n whose elements belong to a set A. *)
 
@@ -40,72 +42,61 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
  fix rectS_fix {n} (v: t A (S n)) : P v :=
  match v with
- |nil => fun devil => False_rect (@ID) devil
- |cons a 0 v =>
-   match v as vnn in t _ nn
-       return
-         match nn,vnn with
-         |0,vm =>  P (a :: vm)
-         |S _,_ => _
-         end
-     with
-     |nil => bas a
-     |_ :: _ => fun devil => False_rect (@ID) devil
-     end
- |cons a (S nn') v => rect a v (rectS_fix v)
+ |@cons _ a 0 v =>
+   match v with
+     |nil _ => bas a
+     |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
+   end
+ |@cons _ a (S nn') v => rect a v (rectS_fix v)
+ |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
  end.
 
-(** An induction scheme for 2 vectors of same length *)
-Definition rect2 {A B} (P:forall {n}, t A n -> t B n -> Type)
-  (bas : P [] []) (rect : forall {n v1 v2}, P v1 v2 ->
-    forall a b, P (a :: v1) (b :: v2)) :=
-fix rect2_fix {n} (v1:t A n):
-  forall v2 : t B n, P v1 v2 :=
-match v1 as v1' in t _ n1
-  return forall v2 : t B n1, P v1' v2 with
-  |[] => fun v2 =>
-     match v2 with
-       |[] => bas
-       |_ :: _ => fun devil => False_rect (@ID) devil
-     end
-  |h1 :: t1 => fun v2 =>
-    match v2 with
-      |[] => fun devil => False_rect (@ID) devil
-      |h2 :: t2 => fun t1' =>
-        rect (rect2_fix t1' t2) h1 h2
-    end t1
-end.
-
 (** A vector of length [0] is [nil] *)
 Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
 match v with
   |[] => H
+  |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
 end.
 
 (** A vector of length [S _] is [cons] *)
 Definition caseS {A} (P : forall {n}, t A (S n) -> Type)
   (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v :=
-match v as v' in t _ m return match m, v' with |0, _ => False -> True |S _, v0 => P v' end with
-  |[] => fun devil => False_rect _ devil (* subterm !!! *)
+match v with
   |h :: t => H h t
+  |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
 end.
+
+Definition caseS' {A} {n : nat} (v : t A (S n)) : forall (P : t A (S n) -> Type)
+  (H : forall h t, P (h :: t)), P v :=
+  match v with
+  | h :: t => fun P H => H h t
+  | _ => fun devil => False_rect (@IDProp) devil
+  end.
+
+(** An induction scheme for 2 vectors of same length *)
+Definition rect2 {A B} (P:forall {n}, t A n -> t B n -> Type)
+  (bas : P [] []) (rect : forall {n v1 v2}, P v1 v2 ->
+    forall a b, P (a :: v1) (b :: v2)) :=
+  fix rect2_fix {n} (v1 : t A n) : forall v2 : t B n, P v1 v2 :=
+  match v1 with
+  | [] => fun v2 => case0 _ bas v2
+  | @cons _ h1 n' t1 => fun v2 =>
+    caseS' v2 (fun v2' => P (h1::t1) v2') (fun h2 t2 => rect (rect2_fix t1 t2) h1 h2)
+  end.
+
 End SCHEMES.
 
 Section BASES.
 (** The first element of a non empty vector *)
-Definition hd {A} {n} (v:t A (S n)) := Eval cbv delta beta in
-(caseS (fun n v => A) (fun h n t => h) v).
+Definition hd {A} := @caseS _ (fun n v => A) (fun h n t => h).
+Global Arguments hd {A} {n} v.
 
 (** The last element of an non empty vector *)
-Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in
-(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) v).
+Definition last {A} := @rectS _ (fun _ _ => A) (fun a => a) (fun _ _ _ H => H).
+Global Arguments last {A} {n} v.
 
 (** Build a vector of n{^ th} [a] *)
-Fixpoint const {A} (a:A) (n:nat) :=
-  match n return t A n with
-  | O => nil A
-  | S n => a :: (const a n)
-  end.
+Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 
 (** The [p]{^ th} element of a vector of length [m].
 
@@ -114,8 +105,8 @@ ocaml function. *)
 Definition nth {A} := 
 fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
 match p in Fin.t m' return t A m' -> A with
- |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v
- |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
+ |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
+ |Fin.FS p' => fun v => (caseS (fun n v' => Fin.t n -> A)
    (fun h n t p0 => nth_fix t p0) v) p'
 end v'.
 
@@ -126,9 +117,9 @@ Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=
 (** Put [a] at the p{^ th} place of [v] *)
 Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
   match p with
-  |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) v'
-  |Fin.FS k p' => fun v' =>
-    (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) v') p'
+  | @Fin.F1 k => fun v': t A (S k) => caseS' v' _ (fun h t => a :: t)
+  | @Fin.FS k p' => fun v' : t A (S k) =>
+    (caseS' v' (fun _ => t A (S k)) (fun h t => h :: (replace t p' a)))
   end v.
 
 (** Version of replace with [lt] *)
@@ -136,13 +127,13 @@ Definition replace_order {A n} (v: t A n) {p} (H: p < n) :=
 replace v (Fin.of_nat_lt H).
 
 (** Remove the first element of a non empty vector *)
-Definition tl {A} {n} (v:t A (S n)) := Eval cbv delta beta in
-(caseS (fun n v => t A n) (fun h n t => t) v).
+Definition tl {A} := @caseS _ (fun n v => t A n) (fun h n t => t).
+Global Arguments tl {A} {n} v.
 
 (** Remove last element of a non-empty vector *)
-Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n :=
-Eval cbv delta beta in (rectS (fun n _ => t A n) (fun a => [])
-  (fun h _ _ H => h :: H) v).
+Definition shiftout {A} := @rectS _ (fun n _ => t A n) (fun a => [])
+  (fun h _ _ H => h :: H).
+Global Arguments shiftout {A} {n} v.
 
 (** Add an element at the end of a vector *)
 Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) :=
@@ -152,9 +143,9 @@ match v with
 end.
 
 (** Copy last element of a vector *)
-Definition shiftrepeat {A} {n} (v:t A (S n)) : t A (S (S n)) :=
-Eval cbv delta beta in (rectS (fun n _ => t A (S (S n)))
-  (fun h =>  h :: h :: []) (fun h _ _ H => h :: H) v).
+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.
 
 (** Remove [p] last elements of a vector *)
 Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
@@ -221,10 +212,10 @@ Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
   end.
 
 (** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *)
-Definition map2 {A B C} (g:A -> B -> C) {n} (v1:t A n) (v2:t B n)
-  : t C n :=
-Eval cbv delta beta in rect2 (fun n _ _ => t C n) (nil C)
-  (fun _ _ _ H a b => (g a b) :: H) v1 v2.
+Definition map2 {A B C} (g:A -> B -> C) :
+  forall (n : nat), t A n -> t B n -> t C n :=
+@rect2 _ _ (fun n _ _ => t C n) (nil C) (fun _ _ _ H a b => (g a b) :: H).
+Global Arguments map2 {A B C} g {n} v1 v2.
 
 (** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *)
 Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B :=
@@ -242,24 +233,19 @@ Definition fold_right {A B : Type} (f : A->B->B) :=
     | a :: w => f a (fold_right_fix w b)
   end.
 
-(** fold_right2 g [x1 .. xn] [y1 .. yn] c = g x1 y1 (g x2 y2 .. (g xn yn c) .. ) *)
-Definition fold_right2 {A B C} (g:A -> B -> C -> C) {n} (v:t A n)
-  (w : t B n) (c:C) : C :=
-Eval cbv delta beta in rect2 (fun _ _ _ => C) c
-  (fun _ _ _ H a b => g a b H) v w.
+(** fold_right2 g c [x1 .. xn] [y1 .. yn] = g x1 y1 (g x2 y2 .. (g xn yn c) .. )
+    c is before the vectors to be compliant with "refolding". *)
+Definition fold_right2 {A B C} (g:A -> B -> C -> C) (c: C) :=
+@rect2 _ _ (fun _ _ _ => C) c (fun _ _ _ H a b => g a b H).
+
 
 (** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *)
 Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) :=
 fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A :=
 match v in t _ n0 return t C n0 -> A with
-  |[] => fun w => match w in t _ n1
-    return match n1 with |0 => A |S _ => @ID end with
-    |[] => a
-    |_ :: _ => @id end
-  |cons vh vn vt => fun w => match w in t _ n1
-    return match n1 with |0 => @ID |S n => t B n -> A end with
-    |[] => @id
-    |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt end vt
+  |[] => fun w => case0 (fun _ => A) a w
+  |@cons _ vh vn vt => fun w =>
+    caseS' w (fun _ => A) (fun wh wt => fold_left2_fix (f a vh wh) vt wt)
 end.
 
 End ITERATORS.
diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v
new file mode 100644
index 00000000..04c57073
--- /dev/null
+++ b/theories/Vectors/VectorEq.v
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Equalities and Vector relations
+
+   Author: Pierre Boutillier
+   Institution: PPS, INRIA 07/2012
+*)
+
+Require Import VectorDef.
+Require Import VectorSpec.
+Import VectorNotations.
+
+Section BEQ.
+
+ Variables (A: Type) (A_beq: A -> A -> bool).
+ Hypothesis A_eqb_eq: forall x y, A_beq x y = true <-> x = y.
+
+ Definition eqb:
+   forall {m n} (v1: t A m) (v2: t A n), bool :=
+   fix fix_beq {m n} v1 v2 :=
+   match v1, v2 with
+     |[], [] => true
+     |_ :: _, [] |[], _ :: _ => false
+     |h1 :: t1, h2 :: t2 => A_beq h1 h2 && fix_beq t1 t2
+   end%bool.
+
+ Lemma eqb_nat_eq: forall m n (v1: t A m) (v2: t A n)
+  (Hbeq: eqb v1 v2 = true), m = n.
+ Proof.
+   intros m n v1; revert n.
+   induction v1; destruct v2;
+     [now constructor | discriminate | discriminate | simpl].
+   intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq.
+   f_equal; eauto.
+ Qed.
+
+ Lemma eqb_eq: forall n (v1: t A n) (v2: t A n),
+  eqb v1 v2 = true <-> v1 = v2.
+ Proof.
+   refine (@rect2 _ _ _ _ _); [now constructor | simpl].
+   intros ? ? ? Hrec h1 h2; destruct Hrec; destruct (A_eqb_eq h1 h2); split.
+   + intros Hbeq. apply andb_prop in Hbeq; destruct Hbeq.
+     f_equal; now auto.
+   + intros Heq. destruct (cons_inj Heq). apply andb_true_intro.
+     split; now auto.
+ Qed.
+
+ Definition eq_dec n (v1 v2: t A n): {v1 = v2} + {v1 <> v2}.
+ Proof.
+ case_eq (eqb v1 v2); intros.
+  + left; now apply eqb_eq.
+  + right. intros Heq. apply <- eqb_eq in Heq. congruence.
+ Defined.
+
+End BEQ.
+
+Section CAST.
+
+ Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n.
+ Proof.
+ refine (fix cast {A m} (v: t A m) {struct v} :=
+  match v in t _ m' return forall n, m' = n -> t A n with
+  |[] => fun n => match n with
+    | 0 => fun _ => []
+    | S _ => fun H => False_rect _ _
+  end
+  |h :: w => fun n => match n with
+    | 0 => fun H => False_rect _ _
+    | S n' => fun H => h :: (cast w n' (f_equal pred H))
+  end
+ end); discriminate.
+ Defined.
+
+End CAST.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 2f4086e5..7f4228dd 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -16,7 +16,7 @@ Require Fin.
 Require Import VectorDef.
 Import VectorNotations.
 
-Definition cons_inj A a1 a2 n (v1 v2 : t A n)
+Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
  (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 :=
    match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1
    with | eq_refl => conj eq_refl eq_refl
@@ -59,15 +59,15 @@ Qed.
 Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
   nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
 Proof.
-refine (@Fin.rectS _ _ _); intros.
+refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
   revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
   revert p H.
-  refine (match v as v' in t _ m return match m as m' return t A m' -> Type with
+  refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
     |S (S n) => fun v => forall p : Fin.t (S n),
       (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
       (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
-    |_ => fun _ => @ID end v' with
-  |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl.
+    |_ => fun _ => True end v' with
+  |[] => I |h :: t => _ end). destruct n0. exact I. now simpl.
 Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
@@ -105,7 +105,7 @@ Proof.
 assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
   induction v0.
     now simpl.
-    intros; simpl. rewrite<- IHv0. now f_equal.
+    intros; simpl. rewrite<- IHv0, assoc. now f_equal.
   induction v.
     reflexivity.
     simpl. intros; now rewrite<- (IHv).
diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget
index 7f00d016..779b1821 100644
--- a/theories/Vectors/vo.itarget
+++ b/theories/Vectors/vo.itarget
@@ -1,4 +1,5 @@
 Fin.vo
 VectorDef.vo
 VectorSpec.vo
+VectorEq.vo
 Vector.vo