summaryrefslogtreecommitdiff
path: root/theories/Vectors
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Vectors
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Vectors')
-rw-r--r--theories/Vectors/Fin.v174
-rw-r--r--theories/Vectors/Vector.v2
-rw-r--r--theories/Vectors/VectorDef.v136
-rw-r--r--theories/Vectors/VectorEq.v80
-rw-r--r--theories/Vectors/VectorSpec.v12
-rw-r--r--theories/Vectors/vo.itarget1
6 files changed, 271 insertions, 134 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index a5e37f34..b9bf6c7f 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -8,13 +8,14 @@
Require Arith_base.
-(** [fin n] is a convinient way to represent \[1 .. n\]
+(** [fin n] is a convenient way to represent \[1 .. n\]
-[fin n] can be seen as a n-uplet of unit where [F1] is the first element of
-the n-uplet and [FS] set (n-1)-uplet of all the element but the first.
+[fin n] can be seen as a n-uplet of unit. [F1] is the first element of
+the n-uplet. If [f] is the k-th element of the (n-1)-uplet, [FS f] is the
+(k+1)-th element of the n-uplet.
Author: Pierre Boutillier
- Institution: PPS, INRIA 12/2010-01/2012
+ Institution: PPS, INRIA 12/2010-01/2012-07/2012
*)
Inductive t : nat -> Set :=
@@ -23,76 +24,68 @@ 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 (@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))
- {n} (p: t (S n)): P p :=
+Definition caseS' {n : nat} (p : t (S n)) : forall (P : t (S n) -> Type)
+ (P1 : P F1) (PS : forall (p : t n), P (FS p)), P p :=
match p with
- |F1 k => P1 k
- |FS k pp => PS pp
+ | @F1 k => fun P P1 PS => P1
+ | FS pp => fun P P1 PS => PS pp
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))
+ {n} (p: t (S n)) : P p := caseS' p P (P1 n) PS.
+
Definition rectS (P: forall {n}, t (S n) -> Type)
(P1: forall n, @P n F1) (PS : forall {n} (p: t (S n)), P p -> P (FS p)):
forall {n} (p: t (S n)), P p :=
fix rectS_fix {n} (p: t (S n)): P p:=
match p with
- |F1 k => P1 k
- |FS 0 pp => case0 (fun f => P (FS f)) pp
- |FS (S k) pp => PS pp (rectS_fix pp)
+ | @F1 k => P1 k
+ | @FS 0 pp => case0 (fun f => P (FS f)) pp
+ | @FS (S k) pp => PS pp (rectS_fix pp)
end.
-Definition rect2 (P: forall {n} (a b: t n), Type)
- (H0: forall n, @P (S n) F1 F1)
- (H1: forall {n} (f: t n), P F1 (FS f))
- (H2: forall {n} (f: t n), P (FS f) F1)
- (HS: forall {n} (f g : t n), P f g -> P (FS f) (FS g)):
- 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' => H0 m'
- |FS m' b' => H1 b'
- end
- |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.
+Definition rect2 (P : forall {n} (a b : t n), Type)
+ (H0 : forall n, @P (S n) F1 F1)
+ (H1 : forall {n} (f : t n), P F1 (FS f))
+ (H2 : forall {n} (f : t n), P (FS f) F1)
+ (HS : forall {n} (f g : t n), P f g -> P (FS f) (FS g)) :
+ forall {n} (a b : t n), P a b :=
+ fix rect2_fix {n} (a : t n) {struct a} : forall (b : t n), P a b :=
+ match a with
+ | @F1 m => fun (b : t (S m)) => caseS' b (P F1) (H0 _) H1
+ | @FS m a' => fun (b : t (S m)) =>
+ caseS' b (fun b => P (@FS m a') b) (H2 a') (fun b' => HS _ _ (rect2_fix a' b'))
+ end.
+
End SCHEMES.
Definition FS_inj {n} (x y: t n) (eq: FS x = FS y): x = y :=
match eq in _ = a return
match a as a' in t m return match m with |0 => Prop |S n' => t n' -> Prop end
- with @F1 _ => fun _ => True |@FS _ y => fun x' => x' = y end x with
+ with F1 => fun _ => True |FS y => fun x' => x' = y end x with
eq_refl => eq_refl
end.
(** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
- match n in t k return {i | i< k} with
- |F1 j => exist (fun i => i< S j) 0 (Lt.lt_0_Sn j)
- |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
+ match n with
+ |@F1 j => exist _ 0 (Lt.lt_0_Sn j)
+ |FS p => match to_nat p with |exist _ i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
end.
(** [of_nat p n] answers the p{^ th} element of [fin n] if p < n or a proof of
p >= n else *)
Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
match n with
- |0 => inright _ (ex_intro (fun x => p = 0 + x) p (@eq_refl _ p))
+ |0 => inright _ (ex_intro _ p eq_refl)
|S n' => match p with
|0 => inleft _ (F1)
|S p' => match of_nat p' n' with
|inleft f => inleft _ (FS f)
- |inright arg => inright _ (match arg with |ex_intro m e =>
+ |inright arg => inright _ (match arg with |ex_intro _ m e =>
ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end)
end
end
@@ -109,13 +102,35 @@ Fixpoint of_nat_lt {p n : nat} : p < n -> t n :=
end
end.
+Lemma of_nat_ext {p}{n} (h h' : p < n) : of_nat_lt h = of_nat_lt h'.
+Proof.
+ now rewrite (Peano_dec.le_unique _ _ h h').
+Qed.
+
Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p.
Proof.
-induction p.
- reflexivity.
- simpl; destruct (to_nat p). simpl. subst p; repeat f_equal. apply Peano_dec.le_unique.
+induction p; simpl.
+- reflexivity.
+- destruct (to_nat p); simpl in *. f_equal. subst p. apply of_nat_ext.
+Qed.
+
+Lemma to_nat_of_nat {p}{n} (h : p < n) : to_nat (of_nat_lt h) = exist _ p h.
+Proof.
+ revert n h.
+ induction p; (destruct n ; intros h; [ destruct (Lt.lt_n_O _ h) | cbn]);
+ [ | rewrite (IHp _ (Lt.lt_S_n p n h))]; f_equal; apply Peano_dec.le_unique.
+Qed.
+
+Lemma to_nat_inj {n} (p q : t n) :
+ proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q.
+Proof.
+ intro H.
+ rewrite <- (of_nat_to_nat_inv p), <- (of_nat_to_nat_inv q).
+ destruct (to_nat p) as (np,hp), (to_nat q) as (nq,hq); simpl in *.
+ revert hp hq. rewrite H. apply of_nat_ext.
Qed.
+
(** [weak p f] answers a function witch is the identity for the p{^ th} first
element of [fin (p + m)] and [FS (FS .. (FS (f k)))] for [FS (FS .. (FS k))]
with p FSs *)
@@ -124,15 +139,15 @@ Fixpoint weak {m}{n} p (f : t m -> t n) :
match p as p' return t (p' + m) -> t (p' + n) with
|0 => f
|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))
+ |@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 _)
end.
(** The p{^ th} element of [fin m] viewed as the p{^ th} element of
[fin (m + n)] *)
Fixpoint L {m} n (p : t m) : t (m + n) :=
- match p with |F1 _ => F1 |FS _ p' => FS (L n p') end.
+ match p with |F1 => F1 |FS p' => FS (L n p') end.
Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
Proof.
@@ -145,12 +160,13 @@ Qed.
[fin (n + m)]
Really really ineficient !!! *)
Definition L_R {m} n (p : t m) : t (n + m).
+Proof.
induction n.
exact p.
exact ((fix LS k (p: t k) :=
match p with
- |F1 k' => @F1 (S k')
- |FS _ p' => FS (LS _ p')
+ |@F1 k' => @F1 (S k')
+ |FS p' => FS (LS _ p')
end) _ IHn).
Defined.
@@ -168,8 +184,8 @@ Qed.
Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
match o with
- |F1 m' => L (m' * n) p
- |FS m' o' => R n (depair o' p)
+ |@F1 m' => L (m' * n) p
+ |FS o' => R n (depair o' p)
end.
Lemma depair_sanity {m n} (o : t m) (p : t n) :
@@ -182,3 +198,55 @@ induction o ; simpl.
rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.
now rewrite (Plus.plus_comm n).
Qed.
+
+Fixpoint eqb {m n} (p : t m) (q : t n) :=
+match p, q with
+| @F1 m', @F1 n' => EqNat.beq_nat m' n'
+| FS _, F1 => false
+| F1, FS _ => false
+| FS p', FS q' => eqb p' q'
+end.
+
+Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
+Proof.
+intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal.
++ now apply EqNat.beq_nat_true.
++ easy.
++ easy.
++ eapply IHp. eassumption.
+Qed.
+
+Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q.
+Proof.
+apply rect2; simpl; intros.
+- split; intros ; [ reflexivity | now apply EqNat.beq_nat_true_iff ].
+- now split.
+- now split.
+- eapply iff_trans.
+ + eassumption.
+ + split.
+ * intros; now f_equal.
+ * apply FS_inj.
+Qed.
+
+Lemma eq_dec {n} (x y : t n): {x = y} + {x <> y}.
+Proof.
+ case_eq (eqb x y); intros.
+ + left; now apply eqb_eq.
+ + right. intros Heq. apply <- eqb_eq in Heq. congruence.
+Defined.
+
+Definition cast: forall {m} (v: t m) {n}, m = n -> t n.
+Proof.
+refine (fix cast {m} (v: t m) {struct v} :=
+ match v in t m' return forall n, m' = n -> t n with
+ |F1 => fun n => match n with
+ | 0 => fun H => False_rect _ _
+ | S n' => fun H => F1
+ end
+ |FS f => fun n => match n with
+ | 0 => fun H => False_rect _ _
+ | S n' => fun H => FS (cast f n' (f_equal pred H))
+ end
+end); discriminate.
+Defined.
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
index f3e5e338..672858fa 100644
--- a/theories/Vectors/Vector.v
+++ b/theories/Vectors/Vector.v
@@ -18,5 +18,7 @@ Based on contents from Util/VecUtil of the CoLoR contribution *)
Require Fin.
Require VectorDef.
Require VectorSpec.
+Require VectorEq.
Include VectorDef.
Include VectorSpec.
+Include VectorEq. \ No newline at end of file
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.
diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v
new file mode 100644
index 00000000..04c57073
--- /dev/null
+++ b/theories/Vectors/VectorEq.v
@@ -0,0 +1,80 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Equalities and Vector relations
+
+ Author: Pierre Boutillier
+ Institution: PPS, INRIA 07/2012
+*)
+
+Require Import VectorDef.
+Require Import VectorSpec.
+Import VectorNotations.
+
+Section BEQ.
+
+ Variables (A: Type) (A_beq: A -> A -> bool).
+ Hypothesis A_eqb_eq: forall x y, A_beq x y = true <-> x = y.
+
+ Definition eqb:
+ forall {m n} (v1: t A m) (v2: t A n), bool :=
+ fix fix_beq {m n} v1 v2 :=
+ match v1, v2 with
+ |[], [] => true
+ |_ :: _, [] |[], _ :: _ => false
+ |h1 :: t1, h2 :: t2 => A_beq h1 h2 && fix_beq t1 t2
+ end%bool.
+
+ Lemma eqb_nat_eq: forall m n (v1: t A m) (v2: t A n)
+ (Hbeq: eqb v1 v2 = true), m = n.
+ Proof.
+ intros m n v1; revert n.
+ induction v1; destruct v2;
+ [now constructor | discriminate | discriminate | simpl].
+ intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq.
+ f_equal; eauto.
+ Qed.
+
+ Lemma eqb_eq: forall n (v1: t A n) (v2: t A n),
+ eqb v1 v2 = true <-> v1 = v2.
+ Proof.
+ refine (@rect2 _ _ _ _ _); [now constructor | simpl].
+ intros ? ? ? Hrec h1 h2; destruct Hrec; destruct (A_eqb_eq h1 h2); split.
+ + intros Hbeq. apply andb_prop in Hbeq; destruct Hbeq.
+ f_equal; now auto.
+ + intros Heq. destruct (cons_inj Heq). apply andb_true_intro.
+ split; now auto.
+ Qed.
+
+ Definition eq_dec n (v1 v2: t A n): {v1 = v2} + {v1 <> v2}.
+ Proof.
+ case_eq (eqb v1 v2); intros.
+ + left; now apply eqb_eq.
+ + right. intros Heq. apply <- eqb_eq in Heq. congruence.
+ Defined.
+
+End BEQ.
+
+Section CAST.
+
+ Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n.
+ Proof.
+ refine (fix cast {A m} (v: t A m) {struct v} :=
+ match v in t _ m' return forall n, m' = n -> t A n with
+ |[] => fun n => match n with
+ | 0 => fun _ => []
+ | S _ => fun H => False_rect _ _
+ end
+ |h :: w => fun n => match n with
+ | 0 => fun H => False_rect _ _
+ | S n' => fun H => h :: (cast w n' (f_equal pred H))
+ end
+ end); discriminate.
+ Defined.
+
+End CAST.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 2f4086e5..7f4228dd 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -16,7 +16,7 @@ Require Fin.
Require Import VectorDef.
Import VectorNotations.
-Definition cons_inj A a1 a2 n (v1 v2 : t A n)
+Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
(eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 :=
match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1
with | eq_refl => conj eq_refl eq_refl
@@ -59,15 +59,15 @@ Qed.
Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
Proof.
-refine (@Fin.rectS _ _ _); intros.
+refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
revert p H.
- refine (match v as v' in t _ m return match m as m' return t A m' -> Type with
+ refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
|S (S n) => fun v => forall p : Fin.t (S n),
(forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
(shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
- |_ => fun _ => @ID end v' with
- |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl.
+ |_ => fun _ => True end v' with
+ |[] => I |h :: t => _ end). destruct n0. exact I. now simpl.
Qed.
Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last 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).
diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget
index 7f00d016..779b1821 100644
--- a/theories/Vectors/vo.itarget
+++ b/theories/Vectors/vo.itarget
@@ -1,4 +1,5 @@
Fin.vo
VectorDef.vo
VectorSpec.vo
+VectorEq.vo
Vector.vo