diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-07 17:10:39 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-07 17:10:39 +0000 |
commit | 4c094673fb024310a2854f7c0d6339bdab5aa2b6 (patch) | |
tree | bd3102a8e7442b002de9e929487e6864a931326d /theories/Vectors/Fin.v | |
parent | efe6c61793d2e4c1419c0bb4bb52a8d6a4903aff (diff) |
Vectors use a bit more the pattern matching compiler
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Vectors/Fin.v')
-rw-r--r-- | theories/Vectors/Fin.v | 28 |
1 files changed, 10 insertions, 18 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index d6ffef6c4..28e355fb6 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -55,23 +55,16 @@ Definition rect2 (P: forall {n} (a b: t n), Type) 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 - return t n0 -> Type with - |0 => fun _ => @ID - |S n0 => fun b0 => P F1 b0 - end b' with + return match n',b' with + |0,_ => @ID + |S n0,b0 => P F1 b0 + end with |F1 m' => H0 m' |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 - return t n0 -> Type with - |0 => fun _ => @ID - |S n0 => fun b0 => - forall (a0: t n0), P (FS a0) b0 - end b' with - |F1 m' => fun aa => H2 aa - |FS m' b' => fun aa => HS aa b' (rect2_fix aa b') + |FS m a' => fun (b: t (S m)) => match b with + |F1 m' => fun aa: t m' => H2 aa + |FS m' b' => fun aa: t m' => HS aa b' (rect2_fix aa b') end a' end. End SCHEMES. @@ -123,8 +116,7 @@ Fixpoint weak {m}{n} p (f : t m -> t n) : t (p + m) -> t (p + n) := match p as p' return t (p' + m) -> t (p' + n) with |0 => f - |S p' => fun x => match x in t n0 return - match n0 with |0 => @ID |S n0' => n0' = p' + m -> t (S p' + n) end with + |S p' => fun x => match x with |F1 n' => fun eq : n' = p' + m => F1 |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq)) end (eq_refl _) @@ -149,8 +141,8 @@ Definition L_R {m} n (p : t m) : t (n + m). induction n. exact p. exact ((fix LS k (p: t k) := - match p in t n0 return t (S n0) with - |F1 _ => F1 + match p with + |F1 k' => @F1 (S k') |FS _ p' => FS (LS _ p') end) _ IHn). Defined. |