Require Import Le Lt Gt Minus Min Bool Program Heq.

Set Implicit Arguments.

Section Vectors.

  Variable A : Type.

  Inductive vector : nat -> Type :=
    | vnil : vector 0
    | vcons (a:A) n (l:vector n): vector (S n).

  Definition Svec (n:nat) : Type := vector n.

  Infix ":::" := vcons (at level 60, right associativity) : vector_scope.

  Open Scope vector_scope.

  Definition vhead n (l:vector n) :=
    match l with
      | vnil => error
      | vcons x _ _ => value x
    end.

  Definition vhd n (l:vector (S n)) : A :=
   match l with
     | vcons x _ _ => x
   end.

  Definition vtail n (l:vector n) : vector (pred n) :=
    match l with
      | vnil => vnil
      | vcons a _ m => m
    end.

  Fixpoint VIn (a:A) n (l:vector n) {struct l} : Prop :=
    match l with
      | vnil => False
      | vcons b _ m => b = a \/ VIn a m
    end.

  Fixpoint vapp n (l: vector n) n' (l':vector n') {struct l} : vector (n+n') :=
    match l with
      | vnil => l'
      | vcons a _ l1 => a ::: vapp l1 l'
    end.

  Infix "+++" := vapp (right associativity, at level 60) : vector_scope.

End Vectors.

Implicit Arguments Svec [[A]].
Implicit Arguments vnil [A].
Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
Infix "+++" := vapp (right associativity, at level 60) : vector_scope.

Open Scope vector_scope.

Delimit Scope vector_scope with vector.

Bind Scope vector_scope with vector.

Arguments Scope vector [type_scope].

Section Facts.

  Variable A : Type.

  Notation vec := (vector A).

  Theorem vnil_cons : forall (x:A) n (l:vec n), ~ {{ Svec # vnil == x ::: l }}.
  Proof.
    intros; discriminate.
  Qed.

  Theorem destruct_vector : forall n (l : vec n), {x:A & {tl:vec (pred n) | {{ Svec # l == x:::tl }} } }+{ {{Svec # l == vnil}} }.
  Proof.
    induction l as [|a n tl].
    right; reflexivity.
    left; exists a; exists tl; reflexivity.
  Qed.

  Theorem vhead_nil : vhead (@vnil A) = None.
  Proof.
    simpl; reflexivity.
  Qed.

  Theorem vhead_cons : forall n (l : vec n) (x : A), vhead (x:::l) = Some x.
  Proof.
    intros; simpl; reflexivity.
  Qed.

  Theorem vhdtail : forall n (l : vec (S n)), l = vhd l ::: vtail l.
    intros. dependent destruction l. auto.
  Qed.

  Theorem vin_eq : forall (a:A) n (l:vec n), VIn a (a ::: l).
  Proof.
    simpl in |- *; auto.
  Qed.

  Theorem vin_cons : forall (a b:A) n (l:vec n), VIn b l -> VIn b (a ::: l).
  Proof.
    simpl in |- *; auto.
  Qed.

  Theorem vin_nil : forall a:A, ~ VIn a vnil.
  Proof.
    unfold not in |- *; intros a H; inversion_clear H.
  Qed.

  Lemma VIn_split : forall x n (l:vec n), VIn x l -> exists n1, exists l1:vec n1, exists n2, exists l2:vec n2, {{ Svec # l == l1+++x:::l2 }}.
  Proof.
  induction l; simpl; destruct 1.
  subst a; auto.
  eexists; exists (@vnil A); eexists; exists l; auto.
  destruct (IHl H) as (n1,(l1,(n2,(l2,H0)))).
  eexists; exists (a:::l1); eexists; exists l2; simpl; f_equal. Hrewritec H0. auto.
  Qed.

  Theorem vin_inv : forall (a b:A) n (l:vec n), VIn b (a ::: l) -> a = b \/ VIn b l.
  Proof.
    intros a b l H; inversion_clear H; auto.
  Qed.

  Theorem VIn_dec :
    (forall x y:A, {x = y} + {x <> y}) ->
    forall (a:A) n (l:vec n), {VIn a l} + {~ VIn a l}.
  Proof.
    intro H; induction l as [| a0 l IHl].
    right; apply vin_nil.
    destruct (H a0 a); simpl in |- *; auto.
    destruct IHl; simpl in |- *; intuition.
    right; unfold not in |- *; intros [Hc1| Hc2]; auto.
  Defined.

  Theorem vapp_cons_not_nil : forall n (x :vec n) m (y: vec m) (a:A), ~ {{ Svec # vnil == x +++ a ::: y }}.
  Proof.
    unfold not in |- *.
    destruct x as [| a l]; simpl in |- *; intros.
    discriminate H.
    discriminate H.
  Qed.

  Theorem vapp_nil_end : forall n (l:vec n), {{ Svec # l == l +++ vnil }}.
  Proof.
    induction l; simpl in |- *; auto.
    Hrewritec <- IHl; auto.
  Qed.

  Theorem vapp_ass : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), {{ Svec # (l +++ l') +++ l'' == l +++ l' +++ l'' }}.
  Proof.
    intros. induction l; simpl in |- *; auto.
    Hrewritec IHl. auto.
  Qed.
  Hint Resolve vapp_ass.

  Theorem vass_app : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), {{ Svec # l +++ l' +++ l'' == (l +++ l') +++ l'' }}.
  Proof.
    intros. Hrewritec (vapp_ass l l' l''). auto.
  Qed.

  Theorem vapp_comm_cons : forall n (x: vec n) m (y:vec m) (a:A), a ::: (x +++ y) = (a ::: x) +++ y.
  Proof.
    auto.
  Qed.

  Theorem vapp_eq_nil : forall n (l:vec n) n' (l':vec n'), {{Svec # l +++ l' == vnil}} -> {{ Svec # l == vnil }} /\ {{ Svec # l' == vnil }}.
  Proof.
    destruct l as [| x n l]; destruct l' as [| y n' l']; simpl in |- *; auto.
    intro; discriminate.
    intros H; discriminate H.
  Qed.

  Theorem vapp_eq_unit :
    forall n (x: vec n) m (y:vec m) (a:A),
      {{ Svec # x +++ y == a ::: vnil }} -> {{ Svec # x == vnil }} /\ {{ Svec # y == a ::: vnil }} \/ {{ Svec # x == a ::: vnil }} /\ {{ Svec # y == vnil }}.
  Proof.
    destruct x as [| a n l]; [ destruct y as [| a m l] | destruct y as [| a0 m0 l0] ];
      simpl in |- *.
    intros a H; discriminate H.
    left; split; auto.
    right; split; auto.
    Hrewritec <- H. apply vapp_nil_end.
    intros.
    inversion H; Hsubst. destruct n; inversion H1.
  Qed.

  Lemma vapp_inj_head : forall n (x:vec n) m (y:vec m) a b, {{ Svec # a ::: x == b ::: y}} -> {{ Svec # x == y }} /\ a = b.
    intros. inversion H; Hsubst. auto.
  Qed.

  Lemma vapp_inj_tail :
    forall n (x: vec n) m (y:vec m) (a b:A), {{ Svec # x +++ a ::: vnil == y +++ b ::: vnil }} -> {{ Svec # x == y }} /\ a = b.
  Proof.
    induction x as [| x n l IHl];
      [ destruct y as [| a n l] | destruct y as [| a n0 l0] ];
      simpl in |- *; auto.
    intros a b H.
    inversion H; Hsubst.
    auto.
    intros a0 b H.
    inversion H; Hsubst; intros.
    destruct n; inversion H1.
    intros a b H.
    inversion H; Hsubst; intros.
    destruct n; inversion H1.
    intros a0 b H.
    destruct (vapp_inj_head H).
    destruct (IHl _ l0 a0 b H0).
    split; auto.
    rewrite <- H1. Hrewritec <- H2; reflexivity.
  Qed.

  Lemma vin_app_or : forall n (l:vec n) n' (l':vec n') (a:A), VIn a (l +++ l') -> VIn a l \/ VIn a l'.
  Proof.
    intros n l n' l' a.
    elim l; simpl in |- *; auto.
    intros a0 n0 y H H0.
    elim H0; auto.
    intro H1.
    elim (H H1); auto.
  Qed.

  Lemma vin_or_app : forall n (l:vec n) n' (l':vec n') (a:A), VIn a l \/ VIn a l' -> VIn a (l +++ l').
  Proof.
    intros n l n' l' a.
    elim l; simpl in |- *; intro H.
    elim H; auto; intro H0.
    elim H0.     intros n0 y H0 H1.
    elim H1; auto 4.
    intro H2.
    elim H2; auto.
  Qed.

  Lemma vapp_inv_head:
   forall n (l:vec n) n1 (l1:vec n1) n2 (l2: vec n2), {{ Svec # l +++ l1 == l +++ l2 }} -> {{ Svec # l1 == l2 }}.
  Proof.
    induction l; simpl; auto. intros. destruct (vapp_inj_head H). auto.
  Qed.

  Lemma vapp_inv_tail:
    forall n (l:vec n) n1 (l1:vec n1) n2 (l2 : vec n2), {{ Svec # l1 +++ l == l2 +++ l }} -> {{ Svec # l1 == l2 }}.
  Proof.
    intros n l n1 l1 n2 l2; revert n1 l1 n2 l2 n l.
    induction l1 as [ | x1 n1 l1]; destruct l2 as [ | x2 n2 l2];
      simpl; auto; intros n l H.
    Hsubst. absurd (S (n2+n) <= n); [idtac|rewrite <- H0]; auto with arith.
    Hsubst. absurd (S (n1+n) <= n); [idtac|rewrite H0]; auto with arith.
    destruct (vapp_inj_head H). rewrite H1. Hrewritec (IHl1 _ _ _ _ H0). auto.
  Qed.

End Facts.

Hint Resolve vapp_nil_end vass_app vapp_ass vnil_cons: datatypes v62.
Hint Resolve vapp_comm_cons vapp_cons_not_nil: datatypes v62.
Hint Immediate vapp_eq_nil: datatypes v62.
Hint Resolve vapp_eq_unit vapp_inj_tail: datatypes v62.
Hint Resolve vin_eq vin_cons vin_inv vin_nil vin_app_or vin_or_app: datatypes v62.

Section Elts.

  Variable A : Type.

  Notation vec := (vector A).

  Fixpoint vnth (n:nat) m (l:vec m) (default:A) {struct l} : A :=
    match n, l with
      | O, vcons x _ l' => x
      | O, other => default
      | S m, vnil => default
      | S m, vcons x _ t => vnth m t default
    end.

  Fixpoint vnth_ok (n:nat) m (l:vec m) (default:A) {struct l} : bool :=
    match n, l with
      | O, vcons x _ l' => true
      | O, other => false
      | S m, vnil => false
      | S m, vcons x _ t => vnth_ok m t default
    end.

  Lemma vnth_in_or_default :
    forall (n:nat) m (l:vec m) (d:A), {VIn (vnth n l d) l} + {vnth n l d = d}.
  Proof.
    intros n m l d; generalize n; induction l; intro n1.
    right; case n1; trivial.
    case n1; simpl in |- *.
    auto.
    intro n2; elim (IHl n2); auto.
  Qed.

  Lemma vnth_S_cons :
    forall (n:nat) m (l:vec m) (d a:A),
      VIn (vnth n l d) l -> VIn (vnth (S n) (a ::: l) d) (a ::: l).
  Proof.
    simpl in |- *; auto.
  Qed.

  Fixpoint vnth_error m (l:vec m) (n:nat) {struct n} : Exc A :=
    match n, l with
      | O, vcons x _ _ => value x
      | S n, vcons _ _ l => vnth_error l n
      | _, _ => error
    end.

  Definition vnth_default (default:A) m (l:vec m) (n:nat) : A :=
    match vnth_error l n with
      | Some x => x
      | None => default
    end.

  Lemma vnth_In :
    forall (n:nat) m (l:vec m) (d:A), n < m -> VIn (vnth n l d) l.

  Proof.
    unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
    destruct l; simpl in |- *; [ inversion 2 | auto ].
    destruct l as [| a m l hl]; simpl in |- *.
    inversion 2.
    intros d ie; right; apply hn; auto with arith.
  Qed.

  Lemma vnth_overflow : forall m (l:vec m) n d, m <= n -> vnth n l d = d.
  Proof.
    induction l.
      destruct n; auto.
      destruct n0; intros; inversion H; simpl; apply IHl; auto with arith.
  Qed.

  Lemma vnth_indep :
    forall m (l:vec m) n d d', n < m -> vnth n l d = vnth n l d'.
  Proof.
    induction l; simpl; intros; auto.
    inversion H.
    destruct n0; simpl; auto with arith.
  Qed.

  Lemma vapp_nth1 :
    forall m (l:vec m) m' (l':vec m') d n, n < m -> vnth n (l+++l') d = vnth n l d.
  Proof.
    induction l.
    intros.
    inversion H.
    intros m' l' d n0.
    case n0; simpl; auto.
    intros; rewrite IHl; auto with arith.
  Qed.

  Lemma vapp_nth2 :
    forall m (l:vec m) m' (l':vec m') d n, n >= m -> vnth n (l+++l') d = vnth (n-m) l' d.
  Proof.
    induction l.
    intros.
    simpl.
    destruct n; auto.
    intros m' l' d n0.
    case n0; simpl; auto.
    intros.
    inversion H.
    intros.
    rewrite IHl; auto with arith.
  Qed.

  Section Remove.

    Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.

    Fixpoint vremove (x : A) n (l : vec n) {struct l} : { n : nat & Svec n } :=
      match l with
        | vnil => {{ Svec # _, vnil }}
        | vcons y _ tl => if (eq_dec x y) then vremove x tl else {{ Svec # _, y ::: projT2 (vremove x tl) }}
      end.

    Theorem vremove_In : forall n (l : vec n) (x : A), ~ VIn x (projT2 (vremove x l)).
    Proof.
      induction l as [|x n l]; auto.
      intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
      apply IHl.
      unfold not; intro HF; simpl in HF; destruct HF; auto.
      apply (IHl y); assumption.
    Qed.

  End Remove.

  Fixpoint vlast n (l:vec n) (d:A) {struct l} : A :=
  match l with
    | vnil => d
    | vcons a _ l' => match l' with
                       | vnil => a
                       | _ => vlast l' d
                     end
  end.

  Fixpoint vremovelast n (l:vec n) {struct l} : vec (pred n) :=
    match l in vector _ n return vec (pred n) with
      | vnil => vnil
      | vcons a n' l' => match n' return vec (pred n') -> vec n' with
                          | 0 => fun _ => vnil
                          | _ => fun tl => a ::: tl
                        end (vremovelast l')
    end.

  Lemma vapp_removelast_last :
    forall n (l:vec n) d, ~ {{ Svec # l == vnil }} -> {{ Svec # l == vremovelast l +++ (vlast l d ::: vnil) }}.
  Proof.
    induction l.
    destruct 1; auto.
    intros d _.
    destruct l; auto.
    assert (~ {{Svec # a0 ::: l == vnil}}) by discriminate.
    pattern (a0:::l) at 1; Hrewritec (IHl d H); auto.
  Qed.

  Lemma vexists_last :
    forall n (l:vec n), ~ {{ Svec # l == vnil }} -> { l' : vec (pred n) & { a : A | {{ Svec # l == l'+++a:::vnil }} } }.
  Proof.
    induction l.
    destruct 1; auto.
    intros _.
    destruct l.
    exists (@vnil A); exists a; auto.
    destruct IHl as [l' (a',H)]; try discriminate.
    Hrewrite H. intro.
    exists (a:::l'); exists a'; Hsimplc; auto.
  Qed.

  Lemma vremovelast_app :
    forall n (l:vec n) n' (l':vec n'), ~ {{ Svec # l' == vnil }} -> {{ Svec # vremovelast (l+++l') == l +++ vremovelast l' }}.
  Proof.
    induction l.
    simpl; auto.
    simpl; intros.
    assert (~ {{ Svec # l+++l' == vnil }}).
    destruct l.
    simpl; auto.
    simpl; discriminate.
    specialize (IHl _ l' H).
    destruct (l+++l'); [elim H0; auto | Hrewritec <- IHl; auto].
  Qed.

  Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.

  Fixpoint vcount_occ n (l : vec n) (x : A){struct l} : nat :=
    match l with
      | vnil => 0
      | vcons y _ tl =>
        let n := vcount_occ tl x in
          if eqA_dec y x then S n else n
    end.

  Theorem vcount_occ_In : forall n (l : vec n) (x : A), VIn x l <-> vcount_occ l x > 0.
  Proof.
    induction l as [|y n l].
    simpl; intros; split; [destruct 1 | apply gt_irrefl].
    simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
    rewrite Heq; intuition.
    pose (IHl x). intuition.
  Qed.

  Theorem vcount_occ_inv_nil : forall n (l : vec n), (forall x:A, vcount_occ l x = 0) <-> {{ Svec # l == vnil }}.
  Proof.
    split.
    induction l as [|x n l].
    auto.
    intro H.
    elim (O_S (vcount_occ l x)).
    apply sym_eq.
    generalize (H x).
    simpl. destruct (eqA_dec x x) as [|HF].
    trivial.
    elim HF; reflexivity.
    intro H; Hrewritec H; simpl; reflexivity.
  Qed.

  Lemma vcount_occ_nil : forall (x : A), vcount_occ vnil x = 0.
  Proof.
    intro x; simpl; reflexivity.
  Qed.

  Lemma count_occ_cons_eq : forall n (l : vec n) (x y : A), x = y -> vcount_occ (x:::l) y = S (vcount_occ l y).
  Proof.
    intros n l x y H; simpl.
    destruct (eqA_dec x y); [reflexivity | contradiction].
  Qed.

  Lemma count_occ_cons_neq : forall n (l : vec n) (x y : A), x <> y -> vcount_occ (x:::l) y = vcount_occ l y.
  Proof.
    intros n l x y H; simpl.
    destruct (eqA_dec x y); [contradiction | reflexivity].
  Qed.

End Elts.

Definition plus_n_O n : n = n + 0.
fix 1. intros. destruct n. reflexivity. simpl. apply f_equal. apply plus_n_O.
Defined.

Definition plus_Snm_nSm n m : S n + m = n + S m.
fix 1. destruct n. reflexivity. intro. simpl. apply f_equal. apply plus_Snm_nSm.
Defined.

Definition plus_assoc n m l : n + (m + l) = n + m + l.
fix 1. destruct n. reflexivity. intros. simpl. apply f_equal. apply plus_assoc.
Defined.

Definition plus_comm n m : n + m = m + n.
fix 2. destruct m. symmetry. apply plus_n_O.
eapply trans_eq. symmetry. apply plus_Snm_nSm. simpl. apply f_equal. apply plus_comm.
Defined.

Section VectorOps.

  Variable A : Type.

  Notation vec := (vector A).

  Fixpoint vrev n (l:vec n) : vec n :=
    match l in vector _ n return vec n with
      | vnil => vnil
      | vcons x _ l' => << Svec # plus_comm _ 1 >> vrev l' +++ x ::: vnil
    end.

  Lemma vdistr_rev : forall n (x:vec n) m (y:vec m), {{ Svec # vrev (x +++ y) == vrev y +++ vrev x }}.
  Proof.
    induction x as [| a n l IHl].
    destruct y as [| a n l].
    simpl in |- *.
    auto.

    simpl in |- *.
    apply vapp_nil_end; auto.

    intros m y.
    simpl in |- *.
    Hsimplc. Hrewritec (IHl _ y).
    apply (vapp_ass (vrev y) (vrev l) (a ::: vnil)).
  Qed.

  Remark vrev_unit : forall n (l:vec n) (a:A), {{ Svec # vrev (l +++ a ::: vnil) == a ::: vrev l }}.
  Proof.
    intros.
    apply (vdistr_rev l (a ::: vnil)); simpl in |- *; auto.
  Qed.

  Lemma vrev_involutive : forall n (l:vec n), vrev (vrev l) = l.
  Proof.
    induction l as [| a n l IHl].
    simpl in |- *; auto.

    simpl in |- *.
    Hsimpl. Hrefl (a:::l : Svec _). Helimc C0. Hrewritec (vrev_unit (vrev l) a).
    rewrite IHl; auto.
  Qed.

  Lemma VIn_rev : forall n (l:vec n) x, VIn x l <-> VIn x (vrev l).
  Proof.
    induction l.
    simpl; intuition.
    intros.
    simpl.
    intuition.
    subst.
    Hsimplc. apply vin_or_app; right; simpl; auto.
    Hsimplc. apply vin_or_app; left; firstorder.
    revert H. Hsimplc. intro. destruct (vin_app_or _ _ _ H); firstorder.
  Qed.

  Lemma vrev_nth : forall m (l:vec m) d n, n < m ->
    vnth n (vrev l) d = vnth (m - S n) l d.
  Proof.
    induction l.
    intros; inversion H.
    intros.
    simpl (vrev (a ::: l)). Hsimplc.
    inversion H.
    rewrite <- minus_n_n; simpl.
    rewrite vapp_nth2; auto.
    rewrite <- minus_n_n; auto.
    rewrite vapp_nth1; auto.
    rewrite <- minus_Sn_m; auto with arith.
    apply IHl ; auto with arith.
  Qed.

  Fixpoint vrev_append n (l:vec n) n' (l': vec n') {struct l} : vec (n+n') :=
    match l in vector _ n return vec (n+n') with
      | vnil => l'
      | vcons a _ l => << Svec # sym_eq (plus_Snm_nSm _ _) >> vrev_append l (a:::l')
    end.

  Definition vrev' n (l : vec n) : vec n := << Svec # sym_eq (plus_n_O _) >> vrev_append l vnil.

  Notation vrev_acc := vrev_append (only parsing).

  Lemma vrev_append_rev : forall n (l:vec n) n' (l':vec n'), vrev_acc l l' = vrev l +++ l'.
  Proof.
    induction l; simpl vrev; simpl vrev_append; auto; intros.
    apply (Heq_eq Svec). Hsimplc. rewrite (Hrw (vapp_ass _ _ _)); Hsimplc. rewrite IHl. auto.
  Qed.

  Notation vrev_acc_rev := vrev_append_rev (only parsing).

  Lemma vrev_alt : forall n (l:vec n), {{ Svec # vrev l == vrev_append l vnil }}.
  Proof.
    intros; rewrite vrev_append_rev.
    apply vapp_nil_end.
  Qed.

  Section Reverse_Induction.

    Unset Implicit Arguments.

    Lemma vrev_vector_ind :
      forall (P: forall n, vec n -> Prop),
        P _ vnil ->
        (forall (a:A) n (l:vec n), P _ (vrev l) -> P _ (vrev (a ::: l))) ->
        forall n (l:vec n), P _ (vrev l).
    Proof.
      induction l; auto.
    Qed.
    Set Implicit Arguments.

    Theorem vrev_ind :
      forall (P: forall n, vec n -> Prop),
        P _ vnil ->
        (forall (x:A) n (l:vec n), P _ l -> P _ (l +++ x ::: vnil)) -> forall n (l:vec n), P _ l.
    Proof.
      intros.
      generalize (vrev_involutive l).
      intros E; rewrite <- E.
      apply (vrev_vector_ind P).
      auto.

      simpl in |- *.
      intros.
      Hsimplc. apply (H0 a _ (vrev l0)).
      auto.
    Qed.

  End Reverse_Induction.

  Section Permutation.

    Inductive VPermutation : forall n, vector A n -> forall m, vector A m -> Prop :=
      | perm_nil: VPermutation vnil vnil
      | perm_skip: forall (x:A) n (l:vector A n) n' (l':vector A n'), VPermutation l l' -> VPermutation (x ::: l) (x ::: l')
      | perm_swap: forall (x y:A) n (l:vector A n), VPermutation (y ::: x ::: l) (x ::: y ::: l)
      | perm_trans: forall n (l :vector A n) n' (l':vector A n') n'' (l'':vector A n''), VPermutation l l' -> VPermutation l' l'' -> VPermutation l l''.

    Hint Constructors VPermutation.

    Theorem VPermutation_nil : forall n (l : vec n), VPermutation vnil l -> {{ Svec # l == vnil }}.
    Proof.
      assert (forall n (l:vec n) n' (l':vec n'), VPermutation l' l -> {{ Svec # l' == vnil }} -> {{Svec # l == vnil}}).
        intros. induction H; auto; inversion H0.
      intros. apply H with _ vnil; auto.
    Qed.

    Theorem VPermutation_nil_cons : forall n (l : vec n) (x : A), ~ VPermutation vnil (x:::l).
    Proof.
      unfold not; intros n l x HF.
      elim (@vnil_cons A x n l). apply sym_eq. exact (VPermutation_nil HF).
    Qed.

    Theorem VPermutation_refl : forall n (l : vec n), VPermutation l l.
    Proof.
      induction l; constructor. exact IHl.
    Qed.

    Theorem VPermutation_sym : forall n (l:vec n) n' (l':vec n'), VPermutation l l' -> VPermutation l' l.
    Proof.
      intros n l n' l' Hperm; induction Hperm; auto.
      apply perm_trans with (l':=l'); assumption.
    Qed.

    Theorem VPermutation_trans : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), VPermutation l l' -> VPermutation l' l'' -> VPermutation l l''.
    Proof.
      exact perm_trans.
    Qed.

    Hint Resolve VPermutation_refl VPermutation_sym VPermutation_trans.

    Theorem VPermutation_in : forall n (l:vec n) n' (l': vec n') (x : A), VPermutation l l' -> VIn x l -> VIn x l'.
    Proof.
      intros n l n' l' x Hperm; induction Hperm; simpl; tauto.
    Qed.

    Lemma VPermutation_app_tail : forall n (l:vec n) n' (l':vec n') m (tl : vec m), VPermutation l l' -> VPermutation (l+++tl) (l'+++tl).
    Proof.
      intros n l n' l' m tl Hperm; induction Hperm as [|x n l n' l'|x y n l|n l n' l' n'' l'']; simpl; auto.
      eapply VPermutation_trans with (l':=l'+++tl); trivial.
    Qed.

    Lemma VPermutation_app_head : forall n (l:vec n) m (tl:vec m) m' (tl': vec m'), VPermutation tl tl' -> VPermutation (l+++tl) (l+++tl').
    Proof.
      intros n l m tl m' tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
    Qed.

    Theorem VPermutation_app : forall n (l:vec n) m (r:vec m) n' (l':vec n') m' (r':vec m'), VPermutation l l' -> VPermutation r r' -> VPermutation (l+++r) (l'+++r').
    Proof.
      intros n l m r n' l' m' r' Hpermll' Hpermmm'; induction Hpermll' as [|x n l n' l'|x y n l|n l n' l' n'' l''];
        repeat rewrite <- app_comm_cons; try constructor; auto.
      apply VPermutation_trans with (l' := ((x ::: y ::: l) +++ r)); repeat rewrite app_comm_cons;
        [apply VPermutation_app_tail | apply VPermutation_app_head]; auto.
      eapply VPermutation_trans. apply IHHpermll'1. eapply VPermutation_trans; [idtac | apply IHHpermll'2].
        apply VPermutation_app_head; auto.
    Qed.

    Theorem VPermutation_app_swap : forall n (l:vec n) n' (l' : vec n'), VPermutation (l+++l') (l'+++l).
    Proof.
      induction l as [|x n l].
      simpl; intros n' l'; Hrewritec <- (vapp_nil_end l'); trivial.
      induction l' as [|y n' l'].
      simpl; Hrewritec <- (vapp_nil_end l); trivial.
      simpl; apply VPermutation_trans with (l' := x ::: y ::: l' +++ l).
      constructor; rewrite vapp_comm_cons; apply IHl.
      apply VPermutation_trans with (l' := y ::: x ::: l' +++ l); constructor.
      apply VPermutation_trans with (l' := x ::: l +++ l'); auto.
    Qed.

    Theorem VPermutation_cons_app : forall n (l:vec n) n1 (l1:vec n1) n2 (l2:vec n2) a,
      VPermutation l (l1 +++ l2) -> VPermutation (a ::: l) (l1 +++ a ::: l2).
    Proof.
    intros n l n1 l1; revert n l.
    induction l1.
    simpl.
    intros; apply perm_skip; auto.
    simpl; intros.
    apply perm_trans with _ (a0:::a:::l1+++l2).
    apply perm_skip; auto.
    apply perm_trans with _ (a:::a0:::l1+++l2).
    apply perm_swap; auto.
    apply perm_skip; auto.
    Qed.
    Hint Resolve VPermutation_cons_app.

    Theorem VPermutation_length : forall n (l: vec n) n' (l' : vec n'), VPermutation l l' -> n = n'.
    Proof.
      intros n l n' l' Hperm; induction Hperm; try (rewrite IHHperm1); auto.
    Qed.

    Theorem VPermutation_rev : forall n (l : vec n), VPermutation l (vrev l).
    Proof.
      induction l as [| x n l]; simpl; trivial.
      apply VPermutation_trans with (l' := (x:::vnil)+++vrev l).
      simpl; auto.
      Hsimplc. apply VPermutation_app_swap.
    Qed.

    Theorem VPermutation_ind_bis :
     forall (P : forall n, vec n -> forall m, vec m -> Prop),
       P _ (@vnil A) _ (@vnil A) ->
       (forall x n l n' l', VPermutation l l' -> P n l n' l' -> P _ (x ::: l) _ (x ::: l')) ->
       (forall x y n l n' l', VPermutation l l' -> P n l n' l' -> P _ (y ::: x ::: l) _ (x ::: y ::: l')) ->
       (forall n l n' l' n'' l'', VPermutation l l' -> P n l n' l' -> VPermutation l' l'' -> P _ l' n'' l'' -> P _ l _ l'') ->
       forall n l n' l', VPermutation l l' -> P n l n' l'.
    Proof.
    intros P Hnil Hskip Hswap Htrans.
    induction 1; auto.
    apply Htrans with _ (x:::y:::l); auto.
    apply Hswap; auto.
    induction l; auto.
    apply Hskip; auto.
    apply Hskip; auto.
    induction l; auto.
    eauto.
    Qed.

    Ltac break_vector l x n' l' H :=
     destruct l as [|x n' l']; simpl in *;
     inversion H; Hsubst; intros; subst; clear H.

    Theorem VPermutation_app_inv : forall n1 (l1:vec n1) n2 (l2:vec n2) n3 (l3:vec n3) n4 (l4:vec n4) a,
      VPermutation (l1+++a:::l2) (l3+++a:::l4) -> VPermutation (l1+++l2) (l3 +++ l4).
    Proof.
    set (P:=fun n (l:vec n) n' (l':vec n') =>
             forall a n1 (l1:vec n1) n2 (l2:vec n2) n3 (l3:vec n3) n4 (l4:vec n4),
               {{ Svec # l==l1+++a:::l2 }} -> {{ Svec # l'==l3+++a:::l4 }} -> VPermutation (l1+++l2) (l3+++l4)).
    cut (forall n l n' l', VPermutation l l' -> P n l n' l').
    intros; apply (H _ _ _ _ H0 a); auto.
    intros; apply (VPermutation_ind_bis P); unfold P; clear P; try clear H n l n' l'; simpl; auto.
    intros; destruct l1; simpl in *; discriminate.
    intros x n l n' l' H IH; intros.
    break_vector l1 b n1' l1' H0; break_vector l3 c n3' l3' H1.
    auto.
    apply perm_trans with _ (l3'+++c:::l4); auto.
    apply perm_trans with _ (l1'+++a:::l2); auto using VPermutation_cons_app.
    apply perm_skip.
    apply (IH a _ l1' _ l2 _ l3' _ l4); auto.
    intros x y l l' Hp IH; intros.
    break_vector l1 b n1' l1' H1; break_vector l3 c n3' l3' H2.
    simpl; auto.
    break_vector l3' b n3'' l3'' H6.
    auto.
    apply perm_trans with _ (c:::l3''+++b:::l4); auto.
    break_vector l1' c n1'' l1'' H7.
    auto.
    apply perm_trans with _ (b:::l1''+++c:::l2); auto.
    break_vector l3' d n3'' l3'' H10; break_vector l1' e n1'' l1'' H7.
    auto.
    apply perm_trans with _ (e:::a:::l1''+++l2); auto.
    apply perm_trans with _ (e:::l1''+++a:::l2); auto.
    apply perm_trans with _ (d:::a:::l3''+++l4); auto.
    apply perm_trans with _ (d:::l3''+++a:::l4); auto.
    apply perm_trans with _ (e:::d:::l1''+++l2); auto.
    apply perm_skip; apply perm_skip.
    apply (H0 a _ l1'' _ l2 _ l3'' _ l4); auto.
    intros.
    destruct (VIn_split a l') as (n'1,(l'1,(n'2,(l'2,H6)))).
    apply (VPermutation_in a H).
    Hsubst.
    apply vin_or_app; right; red; auto.
    apply perm_trans with _ (l'1+++l'2).
    apply (H0 _ _ _ _ _ _ _ _ _ H3 H6).
    apply (H2 _ _ _ _ _ _ _ _ _ H6 H4).
    Qed.

    Theorem VPermutation_cons_inv :
       forall n (l:vec n) n' (l':vec n') a, VPermutation (a:::l) (a:::l') -> VPermutation l l'.
    Proof.
    intros; exact (VPermutation_app_inv (@vnil _) l (@vnil _) l' a H).
    Qed.

    Theorem VPermutation_cons_app_inv :
       forall n (l:vec n) n1 (l1:vec n1) n2 (l2:vec n2) a, VPermutation (a ::: l) (l1 +++ a ::: l2) -> VPermutation l (l1 +++ l2).
    Proof.
    intros; exact (VPermutation_app_inv (@vnil _) l l1 l2 a H).
    Qed.

    Theorem VPermutation_app_inv_l :
        forall n (l:vec n) n1 (l1:vec n1) n2 (l2:vec n2), VPermutation (l +++ l1) (l +++ l2) -> VPermutation l1 l2.
    Proof.
    induction l; simpl; auto.
    intros.
    apply IHl.
    apply VPermutation_cons_inv with a; auto.
    Qed.

    Theorem VPermutation_app_inv_r :
       forall n (l:vec n) n1 (l1:vec n1) n2 (l2:vec n2), VPermutation (l1 +++ l) (l2 +++ l) -> VPermutation l1 l2.
    Proof.
    induction l.
    intros n1 l1 n2 l2. do 2 (rewrite (Hrw (sym_Heq (vapp_nil_end _))); Hsimplc). auto.
    intros.
    apply IHl.
    apply VPermutation_app_inv with a; auto.
    Qed.

  End Permutation.

  Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}.

  Lemma vector_eq_dec :
    forall n (l:vec n) n' (l':vec n'), { {{Svec # l == l'}} } + {~ {{Svec # l == l'}} }.
  Proof.
    induction l as [| x n l IHl]; destruct l' as [| y n' l'].
    left; auto.
    right; apply vnil_cons.
    right; unfold not; intro HF; apply (vnil_cons (sym_eq HF)).
    destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl _ l') as [leql'|lneql'];
      try (right; unfold not; intro HF; injection HF; intros; contradiction); Hsubst.
    left; auto.
  Qed.

End VectorOps.

Section Map.
  Variables A B : Type.
  Variable f : A -> B.

  Fixpoint vmap n (l:vector A n) : vector B n :=
    match l with
      | vnil => vnil
      | vcons a _ t => vcons (f a) (vmap t)
    end.

  Lemma vin_map :
    forall n (l:vector A n) (x:A), VIn x l -> VIn (f x) (vmap l).
  Proof.
    induction l as [| a n l IHl]; simpl in |- *;
      [ auto
        | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
  Qed.

  Lemma vin_map_iff : forall n (l:vector A n) y, VIn y (vmap l) <-> exists x, f x = y /\ VIn x l.
  Proof.
    induction l; firstorder (subst; auto).
  Qed.

  Lemma vmap_nth : forall m (l:vector A m) d n,
    vnth n (vmap l) (f d) = f (vnth n l d).
  Proof.
    induction l as[| x m l d n]; simpl vmap; destruct n; firstorder.
  Qed.

  Lemma vmap_app : forall n (l:vector A n) n' (l':vector A n'),
    vmap (l+++l') = (vmap l)+++(vmap l').
  Proof.
    induction l; simpl; auto.
    intros; rewrite IHl; auto.
  Qed.

  Lemma vmap_rev : forall n (l:vector A n), vmap (vrev l) = vrev (vmap l).
  Proof.
    induction l; simpl; auto.
    Hsimplc. rewrite vmap_app.
    rewrite IHl; auto.
  Qed.

  Hint Constructors VPermutation.

  Lemma VPermutation_map :
    forall n (l:vector A n) n' (l':vector A n'), VPermutation l l' -> VPermutation (vmap l) (vmap l').
  Proof.
  induction 1; simpl; auto; eauto.
  Qed.

  Fixpoint vflat_map m (f:A -> vector B m) n (l:vector A n) {struct l} : vector B (n*m) :=
    match l with
      | vnil => vnil
      | vcons x _ t => (f x)+++(vflat_map f t)
    end.

  Lemma vin_flat_map : forall m (f:A->vector B m) n (l:vector A n) (y:B),
    VIn y (vflat_map f l) <-> exists x, VIn x l /\ VIn y (f x).
  Proof.
    induction l; simpl; split; intros.
    contradiction.
    destruct H as (x,(H,_)); contradiction.
    destruct (vin_app_or _ _ _ H).
    exists a; auto.
    destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)).
    exists x; auto.
    apply vin_or_app.
    destruct H as (x,(H0,H1)); destruct H0.
    subst; auto.
    right; destruct (IHl y) as (_,H2); apply H2.
    exists x; auto.
  Qed.

End Map.

Lemma vmap_map : forall (A B C:Type)(f:A->B)(g:B->C) n (l:vector A n),
  vmap g (vmap f l) = vmap (fun x => g (f x)) l.
Proof.
  induction l; simpl; auto.
  rewrite IHl; auto.
Qed.

Lemma vmap_ext :
  forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall n (l:vector A n), vmap f l = vmap g l.
Proof.
  induction l; simpl; auto.
  rewrite H; rewrite IHl; auto.
Qed.

Section Fold_Left_Recursor.
  Variables A B : Type.
  Variable f : A -> B -> A.

  Fixpoint vfold_left n (l:vector B n) (a0:A) {struct l} : A :=
    match l with
      | vnil => a0
      | vcons b _ t => vfold_left t (f a0 b)
    end.

  Lemma vfold_left_app : forall n (l:vector B n) n' (l':vector B n') (i:A),
    vfold_left (l+++l') i = vfold_left l' (vfold_left l i).
  Proof.
    induction l.
    simpl; auto.
    intros.
    simpl.
    auto.
  Qed.

End Fold_Left_Recursor.

Lemma vfold_left_length :
  forall (A:Type) n (l:vector A n), vfold_left (fun x _ => S x) l 0 = n.
Proof.
  intro A.
  cut (forall m (l:vector A m) n, vfold_left (fun x _ => S x) l n = n + m).
  intros.
  exact (H _ l 0).
  induction l; simpl; auto.
  intros; rewrite IHl.
  apply plus_Snm_nSm.
Qed.

Section Fold_Right_Recursor.
  Variables A B : Type.
  Variable f : B -> A -> A.
  Variable a0 : A.

  Fixpoint vfold_right n (l:vector B n) : A :=
    match l with
      | vnil => a0
      | vcons b _ t => f b (vfold_right t)
    end.

End Fold_Right_Recursor.

  Lemma vfold_right_app : forall (A B:Type) (f:A->B->B) n (l:vector A n) n' (l':vector A n') i,
    vfold_right f i (l+++l') = vfold_right f (vfold_right f i l') l.
  Proof.
    induction l.
    simpl; auto.
    simpl; intros.
    f_equal; auto.
  Qed.

  Lemma vfold_left_rev_right : forall (A B:Type)(f:A->B->B) n (l:vector A n) i,
    vfold_right f i (vrev l) = vfold_left (fun x y => f y x) l i.
  Proof.
    induction l.
    simpl; auto.
    intros.
    simpl.
    Hsimplc. rewrite vfold_right_app; simpl; auto.
  Qed.

  Theorem vfold_symmetric :
    forall (A:Type) (f:A -> A -> A),
      (forall x y z:A, f x (f y z) = f (f x y) z) ->
      (forall x y:A, f x y = f y x) ->
      forall (a0:A) n (l:vector A n), vfold_left f l a0 = vfold_right f a0 l.
  Proof.
    destruct l as [| a n l].
    reflexivity.
    simpl in |- *.
    rewrite <- H0.
    generalize a0 a.
    induction l as [| a3 n l IHl]; simpl in |- *.
    trivial.
    intros.
    rewrite H.
    rewrite (H0 a2).
    rewrite <- (H a1).
    rewrite (H0 a1).
    rewrite IHl.
    reflexivity.
  Qed.

  Fixpoint power m n :=
    match n with
      | 0 => 1
      | S n' => power m n' * m
    end.

  Fixpoint vector_power (A B:Type) n (l:vector A n) n' (l':vector B n') {struct l} :
    vector (vector (A * B) n) (power n' n) :=
    match l in vector _ n return vector (vector (A * B) n) (power n' n) with
      | vnil => vcons vnil vnil
      | vcons x _ t =>
        vflat_map (fun f:vector (A * B) _ => vmap (fun y:B => vcons (x, y) f) l')
        (vector_power t l')
    end.

  Section Bool.
    Variable A : Type.
    Variable f : A -> bool.

    Notation vec := (vector A).

    Fixpoint vexistsb n (l:vec n) {struct l}: bool :=
      match l with
        | vnil => false
        | vcons a _ l => f a || vexistsb l
      end.

    Lemma vexistsb_exists :
      forall n (l:vec n), vexistsb l = true <-> exists x, VIn x l /\ f x = true.
    Proof.
      induction l; simpl; intuition.
      inversion H.
      firstorder.
      destruct (orb_prop _ _ H1); firstorder.
      firstorder.
      subst.
      rewrite H2; auto.
    Qed.

    Lemma vexistsb_nth : forall m (l:vec m) n d, n < m ->
      vexistsb l = false -> f (vnth n l d) = false.
    Proof.
      induction l.
      inversion 1.
      simpl; intros.
      destruct (orb_false_elim _ _ H0); clear H0; auto.
      destruct n0 ; auto.
      rewrite IHl; auto with arith.
    Qed.

    Fixpoint vforallb n (l:vec n) {struct l} : bool :=
      match l with
        | vnil => true
        | vcons a _ l => f a && vforallb l
      end.

    Lemma vforallb_forall :
      forall n (l:vec n), vforallb l = true <-> (forall x, VIn x l -> f x = true).
    Proof.
      induction l; simpl; intuition.
      destruct (andb_prop _ _ H1).
      congruence.
      destruct (andb_prop _ _ H1); auto.
      assert (vforallb l = true).
      apply H0; intuition.
      rewrite H1; auto.
    Qed.

    Fixpoint vfilter n (l:vec n) : { n : nat & Svec n } :=
      match l with
        | vnil => {{Svec # _, vnil}}
        | vcons x _ l => if f x then {{Svec # _, x:::projT2 (vfilter l)}} else vfilter l
      end.

    Lemma vfilter_In : forall x n (l:vec n), VIn x (projT2 (vfilter l)) <-> VIn x l /\ f x = true.
    Proof.
      induction l; simpl.
      intuition.
      case_eq (f a); intros; simpl; intuition congruence.
    Qed.

    Fixpoint vfind n (l:vec n) : option A :=
      match l with
        | vnil => None
        | vcons x _ tl => if f x then Some x else vfind tl
      end.

    Fixpoint vpartition n (l:vec n) {struct l} : {n:nat & Svec n} * {n:nat & Svec n} :=
      match l with
        | vnil => ({{Svec # _,vnil}}, {{Svec # _,vnil}})
        | vcons x _ tl => let (g,d) := vpartition tl in
          if f x then ({{Svec # _,x:::projT2 g}},d) else (g,{{Svec # _,x:::projT2 d}})
      end.

  End Bool.

  Section VectorPairs.
    Variables A B : Type.

    Fixpoint vsplit n (l:vector (A*B) n) { struct l }: vector A n * vector B n :=
      match l with
        | vnil => (vnil, vnil)
        | vcons (x,y) _ tl => let (g,d) := vsplit tl in (x:::g, y:::d)
      end.

    Lemma vin_split_l : forall n (l:vector (A*B) n) (p:A*B),
      VIn p l -> VIn (fst p) (fst (vsplit l)).
    Proof.
      induction l; simpl; intros; auto.
      destruct p; destruct a; destruct (vsplit l); simpl in *.
      destruct H.
      injection H; auto.
      right; apply (IHl (a0,b) H).
    Qed.

    Lemma vin_split_r : forall n (l:vector (A*B) n) (p:A*B),
      VIn p l -> VIn (snd p) (snd (vsplit l)).
    Proof.
      induction l; simpl; intros; auto.
      destruct p; destruct a; destruct (vsplit l); simpl in *.
      destruct H.
      injection H; auto.
      right; apply (IHl (a0,b) H).
    Qed.

    Lemma vsplit_nth : forall m (l:vector (A*B) m) (n:nat) (d:A*B),
      vnth n l d = (vnth n (fst (vsplit l)) (fst d), vnth n (snd (vsplit l)) (snd d)).
    Proof.
      induction l.
      destruct n; destruct d; simpl; auto.
      destruct n0; destruct d; simpl; auto.
      destruct a; destruct (vsplit l); simpl; auto.
      destruct a; destruct (vsplit l); simpl in *; auto.
      apply IHl.
    Qed.

    Fixpoint vcombine n (l : vector A n) (l' : vector B n) {struct l} : vector (A*B) n :=
      match l in vector _ n return vector _ n -> vector _ n with
        | vnil => fun _ => vnil
        | vcons x _ tl => fun l' => match l' in vector _ n' return (vector _ (pred n') -> vector _ (pred n')) -> vector _ n' with
                                     | vnil => fun _ => vnil
                                     | vcons y _ tl' => fun combinetl => (x,y):::(combinetl tl')
                                   end (vcombine tl)
      end l'.

    Lemma vsplit_combine : forall n (l: vector (A*B) n),
      let (l1,l2) := vsplit l in vcombine l1 l2 = l.
    Proof.
      induction l.
      simpl; auto.
      destruct a; simpl.
      destruct (vsplit l); simpl in *.
      f_equal; auto.
    Qed.

    Lemma vcombine_split : forall n (l:vector A n) (l':vector B n),
      vsplit (vcombine l l') = (l,l').
    Proof.
      induction l; intros; dependent destruction l'; auto.
      simpl. rewrite IHl. auto.
    Qed.

    Lemma vin_combine_l : forall n (l:vector A n) (l':vector B n) (x:A) (y:B),
      VIn (x,y) (vcombine l l') -> VIn x l.
    Proof.
      induction l; intros.
      simpl; auto.
      rewrite (vhdtail l') in *. simpl vcombine in H.
      destruct H.
        inversion H. intuition.
        right; apply IHl with (vtail l') y; auto.
    Qed.

    Lemma vin_combine_r : forall n (l:vector A n) (l':vector B n) (x:A) (y:B),
      VIn (x,y) (vcombine l l') -> VIn y l'.
    Proof.
      induction l; intros.
      inversion H.
      rewrite (vhdtail l') in *. simpl vcombine in H.
      destruct H.
        inversion H. intuition.
        right; apply IHl with x; auto.
    Qed.

    Lemma vcombine_nth : forall m (l:vector A m) (l':vector B m) (n:nat) (x:A) (y:B),
      vnth n (vcombine l l') (x,y) = (vnth n l x, vnth n l' y).
    Proof.
      induction l; intros.
        dependent destruction l'. destruct n; auto.
        rewrite (vhdtail l'). simpl vcombine.
        destruct n0; simpl; auto.
    Qed.

    Fixpoint vector_prod n (l:vector A n) n' (l':vector B n') {struct l} :
      vector (A * B) (n * n') :=
      match l with
        | vnil => vnil
        | vcons x _ t => (vmap (fun y:B => (x, y)) l')+++(vector_prod t l')
      end.

    Lemma vin_prod_aux :
      forall (x:A) (y:B) n (l:vector B n),
        VIn y l -> VIn (x, y) (vmap (fun y0:B => (x, y0)) l).
    Proof.
      induction l;
        [ simpl in |- *; auto
          | simpl in |- *; destruct 1 as [H1| ];
            [ left; rewrite H1; trivial | right; auto ] ].
    Qed.

    Lemma vin_prod :
      forall n (l:vector A n) n' (l':vector B n') (x:A) (y:B),
        VIn x l -> VIn y l' -> VIn (x, y) (vector_prod l l').
    Proof.
      induction l;
        [ simpl in |- *; tauto
          | simpl in |- *; intros; apply vin_or_app; destruct H;
            [ left; rewrite H; apply vin_prod_aux; assumption | right; auto ] ].
    Qed.

    Lemma vin_prod_iff :
      forall n (l:vector A n) n' (l':vector B n') (x:A) (y:B),
        VIn (x,y) (vector_prod l l') <-> VIn x l /\ VIn y l'.
    Proof.
      split; [ | intros; apply vin_prod; intuition ].
      induction l; simpl; intros.
      intuition.
      destruct (vin_app_or _ _ _ H); clear H.
      destruct (vin_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_).
      destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
      injection H2; clear H2; intros; subst; intuition.
      intuition.
    Qed.

  End VectorPairs.

Section SetIncl.

  Variable A : Type.

  Notation vec := (vector A).

  Definition vincl n (l:vec n) n' (l': vec n') := forall a:A, VIn a l -> VIn a l'.
  Hint Unfold vincl.

  Lemma vincl_refl : forall n (l:vec n), vincl l l.
  Proof.
    auto.
  Qed.
  Hint Resolve vincl_refl.

  Lemma vincl_tl : forall (a:A) n (l:vec n) n' (l':vec n'), vincl l l' -> vincl l (a ::: l').
  Proof.
    auto with datatypes.
  Qed.
  Hint Immediate vincl_tl.

  Lemma vincl_tran : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), vincl l l' -> vincl l' l'' -> vincl l l''.
  Proof.
    auto.
  Qed.

  Lemma vincl_appl : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), vincl l l'' -> vincl l (l'' +++ l').
  Proof.
    auto with datatypes.
  Qed.
  Hint Immediate vincl_appl.

  Lemma vincl_appr : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), vincl l l'' -> vincl l (l' +++ l'').
  Proof.
    auto with datatypes.
  Qed.
  Hint Immediate vincl_appr.

  Lemma vincl_cons :
    forall (a:A) n (l:vec n) n' (l':vec n'), VIn a l' -> vincl l l' -> vincl (a ::: l) l'.
  Proof.
    unfold vincl in |- *; simpl in |- *; intros a n l n' l' H H0 a0 H1.
    elim H1.
    elim H1; auto; intro H2.
    elim H2; auto.     auto.
  Qed.
  Hint Resolve vincl_cons.

  Lemma vincl_app : forall n (l:vec n) n' (l':vec n') n'' (l'':vec n''), vincl l l'' -> vincl l' l'' -> vincl (l +++ l') l''.
  Proof.
    unfold vincl in |- *; simpl in |- *; intros n l n' l' n'' l'' H H0 a H1.
    elim (vin_app_or _ _ _ H1); auto.
  Qed.
  Hint Resolve vincl_app.

End SetIncl.

Hint Resolve vincl_refl vincl_tl vincl_tran vincl_appl vincl_appr vincl_cons
  vincl_app: datatypes v62.

Lemma minus_n_O : forall n, n = n - 0.
Proof.
  induction n; simpl in |- *; auto with arith.
Defined.

Section Cutting.

  Variable A : Type.

  Notation vec := (vector A).

  Fixpoint vfirstn (n:nat) m (l: vec m) {struct n} : vec (min n m) :=
    match n with
      | 0 => vnil
      | S n => match l with
                 | vnil => vnil
                 | vcons a _ l => a:::(vfirstn n l)
               end
    end.

  Fixpoint vskipn (n:nat) m (l: vec m) { struct n } : vec (m-n) :=
    match n return vec (m-n) with
      | 0 => << Svec # minus_n_O _ >> l
      | S n => match l with
                 | vnil => vnil
                 | vcons a _ l => vskipn n l
               end
    end.

  Lemma vfirstn_skipn : forall n m (l:vec m), {{ Svec # vfirstn n l +++ vskipn n l == l }}.
  Proof.
    induction n; intros.
      simpl. Hsimplc. auto.
      destruct l; simpl; auto.
      Hrewritec (IHn _ l). auto.
  Qed.

   Lemma vremovelast_firstn : forall n m (l:vec m), n < m ->
     {{ Svec # vremovelast (vfirstn (S n) l) == vfirstn n l }}.
   Proof.
     induction n; destruct l.
     simpl; auto.
     simpl; auto.
     simpl; auto.
     intros.
     apply lt_S_n in H.
     change (vfirstn (S (S n)) (a:::l)) with ((a:::vnil)+++vfirstn (S n) l).
     change (vfirstn (S n) (a:::l)) with (a:::vfirstn n l).
     eapply trans_Heq. apply (@vremovelast_app _ _ (a:::vnil) _ (vfirstn (S n) l)).
       red; intros. destruct l; try discriminate. inversion H.
       simpl. Hrewritec (IHn _ l H). auto.
   Qed.

   Lemma vfirstn_removelast : forall n m (l:vec m), n < m ->
     {{ Svec # vfirstn n (vremovelast l) == vfirstn n l }}.
   Proof.
     induction n; destruct l.
     simpl; auto.
     simpl; auto.
     simpl; auto.
     intros.
     apply lt_S_n in H.
     change (vremovelast (a ::: l)) with (vremovelast ((a:::vnil)+++l)).
     assert (~ {{ Svec # l == vnil }} ).
       red; intros. inversion H0; Hsubst. inversion H.
     simpl. Hrewritec (vremovelast_app (a:::vnil) H0).
     Hrewritec (IHn _ l H). auto.
   Qed.

End Cutting.

Section ReDun.

  Variable A : Type.

  Notation vec := (vector A).

  Inductive VNoDup : forall n, vec n -> Prop :=
    | NoDup_nil : VNoDup vnil
    | NoDup_cons : forall x n (l:vec n), ~ VIn x l -> VNoDup l -> VNoDup (x:::l).

  Lemma VNoDup_remove_1 : forall n (l:vec n) n' (l':vec n') a, VNoDup (l+++a:::l') -> VNoDup (l+++l').
  Proof.
  induction l; simpl; intros; inversion H; Hsubst; auto.
  constructor.
  red; intro; apply H3.
  apply vin_or_app; destruct (vin_app_or _ _ _ H0); simpl; tauto.
  apply IHl with a0; auto.
  Qed.

  Lemma VNoDup_remove_2 : forall n (l:vec n) n' (l':vec n') a, VNoDup (l+++a:::l') -> ~VIn a (l+++l').
  Proof.
  induction l; simpl; intros; inversion H; Hsubst; auto.
  red; intro; apply H3.
  destruct H0.
  subst a0.
  apply vin_or_app; right; red; auto.
  destruct (IHl _ _ _ H4); auto.
  Qed.

  Lemma VNoDup_Permutation : forall n (l:vec n) n' (l':vec n'),
    VNoDup l -> VNoDup l' -> (forall x, VIn x l <-> VIn x l') -> VPermutation l l'.
  Proof.
  induction l.
  destruct l'; simpl; intros.
  apply perm_nil.
  destruct (H1 a) as (_,H2); destruct H2; auto.
  intros.
  destruct (VIn_split a l') as (n'1,(l'1,(n'2,(l'2,H2)))).
  destruct (H1 a) as (H2,H3); simpl in *; auto.
  Hsubst.
  apply VPermutation_cons_app.
  inversion H; Hsubst.
  apply IHl; auto.
  apply VNoDup_remove_1 with a; auto.
  intro x; split; intros.
  assert (VIn x (l'1+++a:::l'2)).
   destruct (H1 x); simpl in *; auto.
  apply vin_or_app; destruct (vin_app_or _ _ _ H3); auto.
  destruct H4; auto.
  inversion H; Hsubst; intuition.
  assert (VIn x (l'1+++a:::l'2)).
    apply vin_or_app; destruct (vin_app_or _ _ _ H2); simpl; auto.
  destruct (H1 x) as (_,H4); destruct H4; auto.
  subst x.
  destruct (VNoDup_remove_2 _ _ _ H0 H2).
  Qed.

End ReDun.