Simplified rect2, it turns out Arthur's trick was not required.

Standard library now compiles fully.

2 files changed, 26 insertions, 34 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index e5fa182ae..b9bf6c7f7 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -57,8 +57,7 @@ Definition rect2 (P : forall {n} (a b : t n), Type)
     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 => forall a' : t m, (forall b' : t m, P a' b') -> P (@FS m a') b)
-      (fun a' _ => H2 a') (fun b' a' F => HS _ _ (F b')) a' (rect2_fix a')
+      caseS' b (fun b => P (@FS m a') b) (H2 a') (fun b' => HS _ _ (rect2_fix a' b'))
     end.
 
 End SCHEMES.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 6d2146b8e..45c13e5ce 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -51,27 +51,6 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  |_ => 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_ind (@IDProp) devil (* subterm !!! *)
-     end
-  |h1 :: t1 => fun v2 =>
-    match v2 with
-      |h2 :: t2 => fun t1' =>
-        rect (rect2_fix t1' t2) h1 h2
-      |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
-    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
@@ -86,6 +65,25 @@ 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.
@@ -119,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 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] *)
@@ -245,14 +243,9 @@ Definition fold_right2 {A B C} (g:A -> B -> C -> C) (c: C) :=
 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 with
-    |[] => a
-    |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
-  end
-  |@cons _ vh vn vt => fun w => match w with
-    |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt
-    |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
-  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.