Require Export definitions. (* This lemma is taken from Bruno Barras , see coq-club msg # Fri, 17 May 2002 17:17:49 +0200 *) (* It does not require any axiom because equality over nat is decidable *) Require Export Eqdep. (* required for vcons *) Require Export Eqdep_dec. Require Export Peano_dec. Lemma uniq : forall (A : Set) (v : vect A 0), v = vnil A. intros A v. change (v = eq_rec _ (vect A) (vnil A) _ (refl_equal 0)) in |- *. generalize (refl_equal 0). change ((fun (n : nat) (v : vect A n) => forall e : 0 = n, v = eq_rec _ (vect A) (vnil A) _ e) 0 v) in |- *. case v; intros. apply K_dec_set with (p := e). exact eq_nat_dec. reflexivity. discriminate e. Qed. (* This following theorems are derived from the hardware contrib of Coq *) Definition eq_vect (A : Set) := eq_dep nat (vect A). Lemma decompose_dep : forall (A : Set) (n m : nat), m = S n -> forall v : vect A (S n), {v' : vect A n & {a : A | eq_vect A (S n) v (S n) (vcons A n v' a)}}. intros A n m H v. generalize H; clear H. dependent inversion_clear v with (fun (n' : nat) (vl : vect A n') => m = n' -> {v' : vect A n & {a : A | eq_vect A n' vl (S n) (vcons A n v' a)}}). unfold eq_vect in |- *. intros H; exists v0; exists a. apply eq_dep_intro. Qed. Lemma decompose : forall (A : Set) (n : nat) (v : vect A (S n)), {v' : vect A n & {x : A | v = vcons A n v' x}}. intros A n v. cut (sigS (fun t : vect A n => sig (fun a : A => eq_vect A (S n) v (S n) (vcons A n t a)))). intros H; elim H; clear H. intros v' H; elim H; clear H. intros a H. exists v'; exists a. apply eq_dep_eq with (U := nat) (P := vect A) (p := S n). unfold eq_vect in H; trivial. apply (decompose_dep A n (S n)); trivial. Qed. (* Local Variables: mode: coq coq-prog-name: "/usr/local/coq-7.2/bin/coqtop -emacs -q" compile-command: "make lemmas.vo" End: *)