diff options
Diffstat (limited to 'theories/Vectors')
| -rw-r--r-- | theories/Vectors/Fin.v | 174 | ||||
| -rw-r--r-- | theories/Vectors/Vector.v | 2 | ||||
| -rw-r--r-- | theories/Vectors/VectorDef.v | 136 | ||||
| -rw-r--r-- | theories/Vectors/VectorEq.v | 80 | ||||
| -rw-r--r-- | theories/Vectors/VectorSpec.v | 12 | ||||
| -rw-r--r-- | theories/Vectors/vo.itarget | 1 |
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 |