aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Vectors/Fin.v12
-rw-r--r--theories/Vectors/VectorDef.v37
2 files changed, 19 insertions, 30 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index b5736f22d..3c46ebb9a 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -23,10 +23,7 @@ Inductive t : nat -> Set :=
Section SCHEMES.
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.
+ match p with | F1 _ | FS _ _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
Definition caseS (P: forall {n}, t (S n) -> Type)
(P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
@@ -54,11 +51,8 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
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',b' with
- |0,_ => @ID
- |S n0,b0 => P F1 b0
- end with
+ |F1 m => fun (b: t (S m)) => match b as b' in t (S n')
+ return P F1 b' with
|F1 m' => H0 m'
|FS m' b' => H1 b'
end
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 30c0d4c0e..23427eb86 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,19 +40,13 @@ 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 => 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 _,_ => _
- end
- with
+ match v with
|nil => bas a
- |_ :: _ => fun devil => False_rect (@ID) devil
- end
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+ end
|cons a (S nn') v => rect a v (rectS_fix v)
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end.
(** An induction scheme for 2 vectors of same length *)
@@ -66,13 +60,13 @@ match v1 as v1' in t _ n1
|[] => fun v2 =>
match v2 with
|[] => bas
- |_ :: _ => fun devil => False_rect (@ID) devil
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end
|h1 :: t1 => fun v2 =>
match v2 with
- |[] => fun devil => False_rect (@ID) devil
|h2 :: t2 => fun t1' =>
rect (rect2_fix t1' t2) h1 h2
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end t1
end.
@@ -80,14 +74,15 @@ end.
Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
match v with
|[] => H
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
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: 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 !!! *)
+match v with
|h :: t => H h t
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end.
End SCHEMES.
@@ -252,14 +247,14 @@ Eval cbv delta beta in rect2 (fun _ _ _ => 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 in t _ n1
- return match n1 with |0 => A |S _ => @ID end with
+ |[] => fun w => match w with
|[] => a
- |_ :: _ => @id end
- |cons vh vn vt => fun w => match w in t _ n1
- return match n1 with |0 => @ID |S n => t B n -> A end with
- |[] => @id
- |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt end vt
+ |_ => fun devil => False_rect (@ID) 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_rect (@ID) devil (* subterm !!! *)
+ end vt
end.
End ITERATORS.