diff options
Diffstat (limited to 'theories/Vectors')
-rw-r--r-- | theories/Vectors/Fin.v | 2 | ||||
-rw-r--r-- | theories/Vectors/VectorDef.v | 18 | ||||
-rw-r--r-- | theories/Vectors/VectorSpec.v | 2 |
3 files changed, 12 insertions, 10 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index f57726bea..1c4c16cc1 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -24,7 +24,7 @@ Inductive t : nat -> Set := Section SCHEMES. Definition case0 P (p: t 0): P p := - match p with | F1 | FS _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end. + match p with | F1 | FS _ => fun devil => False_rect (@IDProp) 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)) diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 8f672deda..f12aa0b87 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -21,6 +21,8 @@ Require Vectors.Fin. Import EqNotations. Local Open Scope nat_scope. +Set Universe Polymorphism. + (** A vector is a list of size n whose elements belong to a set A. *) @@ -43,10 +45,10 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type) |@cons _ a 0 v => match v with |nil _ => bas a - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end |@cons _ a (S nn') v => rect a v (rectS_fix v) - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end. (** An induction scheme for 2 vectors of same length *) @@ -60,13 +62,13 @@ match v1 as v1' in t _ n1 |[] => fun v2 => match v2 with |[] => bas - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => 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_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end t1 end. @@ -74,7 +76,7 @@ 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 !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end. (** A vector of length [S _] is [cons] *) @@ -82,7 +84,7 @@ 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 with |h :: t => H h t - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end. End SCHEMES. @@ -245,11 +247,11 @@ 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_rect (@ID) devil (* subterm !!! *) + |_ => 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_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end vt end. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index ed2b56d1f..3e8c1175f 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -105,7 +105,7 @@ Proof. assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). induction v0. now simpl. - intros; simpl. rewrite<- IHv0. now f_equal. + intros; simpl. rewrite<- IHv0, assoc. now f_equal. induction v. reflexivity. simpl. intros; now rewrite<- (IHv). |