Vector: missing injection lemmas and better impossible branches

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

3 files changed, 27 insertions, 12 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 28e355fb6..a5e37f34b 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -14,7 +14,7 @@ Require Arith_base.
 the n-uplet and [FS] set (n-1)-uplet of all the element but the first.
 
    Author: Pierre Boutillier
-   Institution: PPS, INRIA 12/2010
+   Institution: PPS, INRIA 12/2010-01/2012
 *)
 
 Inductive t : nat -> Set :=
@@ -69,6 +69,13 @@ match a with
 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
+  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
@@ -167,6 +174,7 @@ end.
 
 Lemma depair_sanity {m n} (o : t m) (p : t n) :
   proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
+Proof.
 induction o ; simpl.
   rewrite L_sanity. now rewrite Mult.mult_0_r.
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 0fee50ffb..30c0d4c0e 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,17 +40,17 @@ 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 => @id
+ |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 _,_ => ID
+         |S _,_ => _
          end
      with
      |nil => bas a
-     |_ :: _ => @id
+     |_ :: _ => fun devil => False_rect (@ID) devil
      end
  |cons a (S nn') v => rect a v (rectS_fix v)
  end.
@@ -66,11 +66,11 @@ match v1 as v1' in t _ n1
   |[] => fun v2 =>
      match v2 with
        |[] => bas
-       |_ :: _ => @id
+       |_ :: _ => fun devil => False_rect (@ID) devil
      end
   |h1 :: t1 => fun v2 =>
     match v2 with
-      |[] => @id
+      |[] => fun devil => False_rect (@ID) devil
       |h2 :: t2 => fun t1' =>
         rect (rect2_fix t1' t2) h1 h2
     end t1
@@ -83,10 +83,10 @@ match v with
 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 : P n v :=
-match v with
-  |[] => @id (* Why needed ? *)
+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 !!! *)
   |h :: t => H h t
 end.
 End SCHEMES.
@@ -111,11 +111,12 @@ Fixpoint const {A} (a:A) (n:nat) :=
 
 Computational behavior of this function should be the same as
 ocaml function. *)
-Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : A :=
+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)
-   (fun h n t p0 => nth t p0) v) p'
+   (fun h n t p0 => nth_fix t p0) v) p'
 end v'.
 
 (** An equivalent definition of [nth]. *)
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index a576315e6..2f4086e5c 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -16,6 +16,12 @@ Require Fin.
 Require Import VectorDef.
 Import VectorNotations.
 
+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
+   end.
+
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
 is true for the one that use [lt] *)