Vectors fully use implicit arguments

and take disavantages for maximal insertion

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

3 files changed, 50 insertions, 50 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 19b4c3b2f..980a5f706 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -22,43 +22,43 @@ Inductive t : nat -> Set :=
 |FS : forall {n}, t n -> t (S n).
 
 Section SCHEMES.
-Definition case0 {P} (p: t 0): P p :=
+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.
 
-Definition caseS (P: forall n, t (S n) -> Type)
-  (P1: forall n, P n F1) (PS : forall n (p: t n), P n (FS p))
-  n (p: t (S n)): P n p :=
+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 :=
   match p as p0 in t n0
   return match n0 as nn return t nn -> Type with
-    |0 => fun _ => @ID |S n' => fun p' => P n' p'
+    |0 => fun _ => @ID |S n' => fun p' => P p'
   end p0 with
   |F1 k => P1 k
-  |FS k pp => PS k pp
+  |FS k pp => PS pp
   end.
 
-Definition rectS (P: forall n, t (S n) -> Type)
-  (P1: forall n, P n F1) (PS : forall n (p: t (S n)), P n p -> P (S n) (FS p)):
-  forall n (p: t (S n)), P n p :=
-fix rectS_fix n (p: t (S n)): P n p:=
+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 as p0 in t n0
   return match n0 as nn return t nn -> Type with
-    |0 => fun _ => @ID |S n' => fun p' => P n' p'
+    |0 => fun _ => @ID |S n' => fun p' => P p'
   end p0 with
   |F1 k => P1 k
-  |FS 0 pp => @case0 (fun f => P 0 (FS f)) pp
-  |FS (S k) pp => PS k pp (rectS_fix k pp)
+  |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 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 :=
+  (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' as n0
@@ -67,7 +67,7 @@ match a with
                             |S n0 => fun b0 => P F1 b0
                           end b' with
                      |F1 m' => H0 m'
-                     |FS m' b' => H1 m' b'
+                     |FS m' b' => H1 b'
                    end
   |FS m a' => fun (b: t (S m)) => match b as b' in t n'
                       return match n' as n0
@@ -76,8 +76,8 @@ match a with
                                |S n0 => fun b0 =>
                                  forall (a0: t n0), P (FS a0) b0
                              end b' with
-                         |F1 m' => fun aa => H2 m' aa
-                         |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b')
+                         |F1 m' => fun aa => H2 aa
+                         |FS m' b' => fun aa => HS aa b' (rect2_fix aa b')
                        end a'
 end.
 End SCHEMES.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index cff72c11b..1b3c3d3b6 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -54,17 +54,17 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  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 0 [] []) (rect : forall n v1 v2, P n v1 v2 ->
-    forall a b, P (S n) (a :: v1) (b :: v2)) :=
+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 n v1 v2 :=
+  forall v2 : t B n, P v1 v2 :=
 match v1 as v1' in t _ n1
-  return forall v2 : t B n1, P n1 v1' v2 with
+  return forall v2 : t B n1, P v1' v2 with
   |[] => fun v2 =>
      match v2 as v2' in t _ n2
        return match n2 as n2' return t B n2' -> Type with
-         |0 => fun v2 => P 0 [] v2 |S _ => fun _ => @ID end v2' with
+         |0 => fun v2 => P [] v2 |S _ => fun _ => @ID end v2' with
        |[] => bas
        |_ :: _ => @id
      end
@@ -74,11 +74,11 @@ match v1 as v1' in t _ n1
         return t B n2' -> Type with
         |0 => fun _ => @ID
         |S n' => fun v2 => forall t1' : t A n',
-          P (S n') (h1 :: t1') v2
+          P (h1 :: t1') v2
         end v2' with
       |[] => @id
       |h2 :: t2 => fun t1' =>
-        rect _ t1' t2 (rect2_fix t1' t2) h1 h2
+        rect (rect2_fix t1' t2) h1 h2
     end t1
 end.
 
@@ -90,17 +90,17 @@ 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 _ (h :: t)) n v : P n v :=
+  (H : forall h {n} t, @P n (h :: t)) {n} v : P n v :=
 match v with
   |[] => @id (* Why needed ? *)
-  |h :: t => H h _ t
+  |h :: t => H h t
 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) n v).
+(caseS (fun n v => A) (fun h n t => h) v).
 
 (** The last element of an non empty vector *)
 Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in
@@ -119,9 +119,9 @@ 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 :=
 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) q v
+ |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) q v) p'
+   (fun h n t p0 => nth t p0) v) p'
 end v'.
 
 (** An equivalent definition of [nth]. *)
@@ -131,9 +131,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 in Fin.t j return t A j -> t A j with
-  |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) _ v'
+  |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': t A (S k) =>
-    (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) _ v') p'
+    (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) v') p'
   end v.
 
 (** Version of replace with [lt] *)
@@ -142,7 +142,7 @@ 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) n v).
+(caseS (fun n v => t A n) (fun h n t => t) v).
 
 (** Remove last element of a non-empty vector *)
 Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n :=
@@ -226,7 +226,7 @@ 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}{n} (g:A -> B -> C) (v1:t A n) (v2:t B n)
+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.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 1fa70a60c..a576315e6 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -23,7 +23,7 @@ Lemma eq_nth_iff A n (v1 v2: t A n):
   (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
 Proof.
 split.
-  revert n v1 v2; refine (rect2 _ _ _); simpl; intros.
+  revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
     reflexivity.
     f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
     apply H. intros p1 p2 H1;
@@ -34,7 +34,7 @@ Qed.
 Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
  nth_order v H = last v.
 Proof.
-unfold nth_order; refine (rectS _ _ _); now simpl.
+unfold nth_order; refine (@rectS _ _ _ _); now simpl.
 Qed.
 
 Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
@@ -42,7 +42,7 @@ Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
 Proof.
 subst k2; induction k1.
   generalize dependent n. apply caseS ; intros. now simpl.
-  generalize dependent n. refine (caseS _ _) ; intros. now simpl.
+  generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
 Qed.
 
 Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a.
@@ -53,8 +53,8 @@ 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.
-  revert n v; refine (caseS _ _); simpl; intros. now destruct t.
+refine (@Fin.rectS _ _ _); intros.
+  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
     |S (S n) => fun v => forall p : Fin.t (S n),
@@ -66,7 +66,7 @@ Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
 Proof.
-refine (rectS _ _ _); now simpl.
+refine (@rectS _ _ _ _); now simpl.
 Qed.
 
 Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a.
@@ -78,17 +78,17 @@ Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2):
   (map f v) [@ p1] = f (v [@ p2]).
 Proof.
 subst p2; induction p1.
-  revert n v; refine (caseS _ _); now simpl.
-  revert n v p1 IHp1; refine (caseS _ _); now simpl.
+  revert n v; refine (@caseS _ _ _); now simpl.
+  revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
 Qed.
 
 Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
   p1 = p2 -> p2 = p3 -> (map2 f v w) [@p1] = f (v[@p2]) (w[@p3]).
 Proof.
 intros; subst p2; subst p3; revert n v w p1.
-refine (rect2 _ _ _); simpl.
-  exact (Fin.case0).
-  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (Fin.caseS _ _ _);
+refine (@rect2 _ _ _ _ _); simpl.
+  exact (Fin.case0 _).
+  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
     now simpl.
 Qed.