summaryrefslogtreecommitdiff
path: root/theories/Vectors/VectorDef.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Vectors/VectorDef.v')
-rw-r--r--theories/Vectors/VectorDef.v136
1 files changed, 61 insertions, 75 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 32ffcb3d..45c13e5c 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. *)
@@ -40,72 +42,61 @@ 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
- |nil => bas a
- |_ :: _ => fun devil => False_rect (@ID) devil
- end
- |cons a (S nn') v => rect a v (rectS_fix v)
+ |@cons _ a 0 v =>
+ match v with
+ |nil _ => bas a
+ |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
+ end
+ |@cons _ a (S nn') v => rect a v (rectS_fix v)
+ |_ => 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_rect (@ID) devil
- 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
- 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
|[] => H
+ |_ => fun devil => False_ind (@IDProp) 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_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.
(** The first element of a non empty vector *)
-Definition hd {A} {n} (v:t A (S n)) := Eval cbv delta beta in
-(caseS (fun n v => A) (fun h n t => h) v).
+Definition hd {A} := @caseS _ (fun n v => A) (fun h n t => h).
+Global Arguments hd {A} {n} v.
(** The last element of an non empty vector *)
-Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in
-(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) v).
+Definition last {A} := @rectS _ (fun _ _ => A) (fun a => a) (fun _ _ _ H => H).
+Global Arguments last {A} {n} v.
(** Build a vector of n{^ th} [a] *)
-Fixpoint const {A} (a:A) (n:nat) :=
- match n return t A n with
- | O => nil A
- | S n => a :: (const a n)
- end.
+Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
(** The [p]{^ th} element of a vector of length [m].
@@ -114,8 +105,8 @@ ocaml function. *)
Definition nth {A} :=
fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
match p in Fin.t m' return t A m' -> A with
- |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v
- |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
+ |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
+ |Fin.FS p' => fun v => (caseS (fun n v' => Fin.t n -> A)
(fun h n t p0 => nth_fix t p0) v) p'
end v'.
@@ -126,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 k 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] *)
@@ -136,13 +127,13 @@ Definition replace_order {A n} (v: t A n) {p} (H: p < n) :=
replace v (Fin.of_nat_lt H).
(** Remove the first element of a non empty vector *)
-Definition tl {A} {n} (v:t A (S n)) := Eval cbv delta beta in
-(caseS (fun n v => t A n) (fun h n t => t) v).
+Definition tl {A} := @caseS _ (fun n v => t A n) (fun h n t => t).
+Global Arguments tl {A} {n} v.
(** Remove last element of a non-empty vector *)
-Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n :=
-Eval cbv delta beta in (rectS (fun n _ => t A n) (fun a => [])
- (fun h _ _ H => h :: H) v).
+Definition shiftout {A} := @rectS _ (fun n _ => t A n) (fun a => [])
+ (fun h _ _ H => h :: H).
+Global Arguments shiftout {A} {n} v.
(** Add an element at the end of a vector *)
Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) :=
@@ -152,9 +143,9 @@ match v with
end.
(** Copy last element of a vector *)
-Definition shiftrepeat {A} {n} (v:t A (S n)) : t A (S (S n)) :=
-Eval cbv delta beta in (rectS (fun n _ => t A (S (S n)))
- (fun h => h :: h :: []) (fun h _ _ H => h :: H) v).
+Definition shiftrepeat {A} := @rectS _ (fun n _ => t A (S (S n)))
+ (fun h => h :: h :: []) (fun h _ _ H => h :: H).
+Global Arguments shiftrepeat {A} {n} v.
(** Remove [p] last elements of a vector *)
Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
@@ -221,10 +212,10 @@ Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
end.
(** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *)
-Definition map2 {A B C} (g:A -> B -> C) {n} (v1:t A n) (v2:t B n)
- : t C n :=
-Eval cbv delta beta in rect2 (fun n _ _ => t C n) (nil C)
- (fun _ _ _ H a b => (g a b) :: H) v1 v2.
+Definition map2 {A B C} (g:A -> B -> C) :
+ forall (n : nat), t A n -> t B n -> t C n :=
+@rect2 _ _ (fun n _ _ => t C n) (nil C) (fun _ _ _ H a b => (g a b) :: H).
+Global Arguments map2 {A B C} g {n} v1 v2.
(** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *)
Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B :=
@@ -242,24 +233,19 @@ Definition fold_right {A B : Type} (f : A->B->B) :=
| a :: w => f a (fold_right_fix w b)
end.
-(** fold_right2 g [x1 .. xn] [y1 .. yn] c = g x1 y1 (g x2 y2 .. (g xn yn c) .. ) *)
-Definition fold_right2 {A B C} (g:A -> B -> C -> C) {n} (v:t A n)
- (w : t B n) (c:C) : C :=
-Eval cbv delta beta in rect2 (fun _ _ _ => C) c
- (fun _ _ _ H a b => g a b H) v w.
+(** fold_right2 g c [x1 .. xn] [y1 .. yn] = g x1 y1 (g x2 y2 .. (g xn yn c) .. )
+ c is before the vectors to be compliant with "refolding". *)
+Definition fold_right2 {A B C} (g:A -> B -> C -> C) (c: C) :=
+@rect2 _ _ (fun _ _ _ => C) c (fun _ _ _ H a b => g a b H).
+
(** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *)
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
- |[] => 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 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 06:59:09 +0000