diff options
| -rw-r--r-- | theories/Vectors/Fin.v | 12 | ||||
| -rw-r--r-- | theories/Vectors/VectorDef.v | 37 |
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. |