diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /theories/Vectors | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'theories/Vectors')
-rw-r--r-- | theories/Vectors/Fin.v | 176 | ||||
-rw-r--r-- | theories/Vectors/Vector.v | 22 | ||||
-rw-r--r-- | theories/Vectors/VectorDef.v | 317 | ||||
-rw-r--r-- | theories/Vectors/VectorSpec.v | 113 | ||||
-rw-r--r-- | theories/Vectors/vo.itarget | 4 |
5 files changed, 632 insertions, 0 deletions
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v new file mode 100644 index 00000000..28e355fb --- /dev/null +++ b/theories/Vectors/Fin.v @@ -0,0 +1,176 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +Require Arith_base. + +(** [fin n] is a convinient 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. + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 +*) + +Inductive t : nat -> Set := +|F1 : forall {n}, t (S n) +|FS : forall {n}, t n -> t (S n). + +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. + +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 := + match p with + |F1 k => P1 k + |FS k pp => PS pp + end. + +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) + 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. +End SCHEMES. + +(** [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 + 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)) + |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 => + ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end) + end + end + end. + +(** [of_nat_lt p n H] answers the p{^ th} element of [fin n] +it behaves much better than [of_nat p n] on open term *) +Fixpoint of_nat_lt {p n : nat} : p < n -> t n := + match n with + |0 => fun H : p < 0 => False_rect _ (Lt.lt_n_O p H) + |S n' => match p with + |0 => fun _ => @F1 n' + |S p' => fun H => FS (of_nat_lt (Lt.lt_S_n _ _ H)) + end + end. + +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. +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 *) +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 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 _) +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. + +Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p). +Proof. +induction p. + reflexivity. + simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p). +Qed. + +(** The p{^ th} element of [fin m] viewed as the p{^ th} element of +[fin (n + m)] +Really really ineficient !!! *) +Definition L_R {m} n (p : t m) : t (n + m). +induction n. + exact p. + exact ((fix LS k (p: t k) := + match p with + |F1 k' => @F1 (S k') + |FS _ p' => FS (LS _ p') + end) _ IHn). +Defined. + +(** The p{^ th} element of [fin m] viewed as the (n + p){^ th} element of +[fin (n + m)] *) +Fixpoint R {m} n (p : t m) : t (n + m) := + match n with |0 => p |S n' => FS (R n' p) end. + +Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p). +Proof. +induction n. + reflexivity. + simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p). +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) +end. + +Lemma depair_sanity {m n} (o : t m) (p : t n) : + proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)). +induction o ; simpl. + rewrite L_sanity. now rewrite Mult.mult_0_r. + + rewrite R_sanity. rewrite IHo. + rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r. + now rewrite (Plus.plus_comm n). +Qed. diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v new file mode 100644 index 00000000..f3e5e338 --- /dev/null +++ b/theories/Vectors/Vector.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Vectors. + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 + +Originally from the contribution bit vector by Jean Duprat (ENS Lyon). + +Based on contents from Util/VecUtil of the CoLoR contribution *) + +Require Fin. +Require VectorDef. +Require VectorSpec. +Include VectorDef. +Include VectorSpec. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v new file mode 100644 index 00000000..0fee50ff --- /dev/null +++ b/theories/Vectors/VectorDef.v @@ -0,0 +1,317 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Definitions of Vectors and functions to use them + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 +*) + +(** +Names should be "caml name in list.ml" if exists and order of arguments +have to be the same. complain if you see mistakes ... *) + +Require Import Arith_base. +Require Vectors.Fin. +Import EqNotations. +Open Local Scope nat_scope. + +(** +A vector is a list of size n whose elements belong to a set A. *) + +Inductive t A : nat -> Type := + |nil : t A 0 + |cons : forall (h:A) (n:nat), t A n -> t A (S n). + +Local Notation "[]" := (nil _). +Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity). + +Section SCHEMES. + +(** An induction scheme for non-empty vectors *) + +Definition rectS {A} (P:forall {n}, t A (S n) -> Type) + (bas: forall a: A, P (a :: [])) + (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 => @id + |cons a 0 v => + match v as vnn in t _ nn + return + match nn,vnn with + |0,vm => P (a :: vm) + |S _,_ => ID + end + with + |nil => bas a + |_ :: _ => @id + end + |cons a (S nn') v => rect a v (rectS_fix v) + 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 + |_ :: _ => @id + end + |h1 :: t1 => fun v2 => + match v2 with + |[] => @id + |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 +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 : P n v := +match v with + |[] => @id (* Why needed ? *) + |h :: t => H h t +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). + +(** 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). + +(** 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. + +(** The [p]{^ th} element of a vector of length [m]. + +Computational behavior of this function should be the same as +ocaml function. *) +Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : 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) + (fun h n t p0 => nth t p0) v) p' +end v'. + +(** An equivalent definition of [nth]. *) +Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) := +(nth v (Fin.of_nat_lt H)). + +(** 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' + end v. + +(** Version of replace with [lt] *) +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). + +(** 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). + +(** Add an element at the end of a vector *) +Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) := +match v with + |[] => a :: [] + |h :: t => h :: (shiftin a t) +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). + +(** Remove [p] last elements of a vector *) +Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n + -> t A (n - p). +Proof. + induction p as [| p f]; intros H v. + rewrite <- minus_n_O. + exact v. + + apply shiftout. + + rewrite minus_Sn_m. + apply f. + auto with *. + exact v. + auto with *. +Defined. + +(** Concatenation of two vectors *) +Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) := + match v with + | [] => w + | a :: v' => a :: (append v' w) + end. + +Infix "++" := append. + +(** Two definitions of the tail recursive function that appends two lists but +reverses the first one *) + +(** This one has the exact expected computational behavior *) +Fixpoint rev_append_tail {A n p} (v : t A n) (w: t A p) + : t A (tail_plus n p) := + match v with + | [] => w + | a :: v' => rev_append_tail v' (a :: w) + end. + +Import EqdepFacts. + +(** This one has a better type *) +Definition rev_append {A n p} (v: t A n) (w: t A p) + :t A (n + p) := + rew <- (plus_tail_plus n p) in (rev_append_tail v w). + +(** rev [a₁ ; a₂ ; .. ; an] is [an ; a{n-1} ; .. ; a₁] + +Caution : There is a lot of rewrite garbage in this definition *) +Definition rev {A n} (v : t A n) : t A n := + rew <- (plus_n_O _) in (rev_append v []). + +End BASES. +Local Notation "v [@ p ]" := (nth v p) (at level 1). + +Section ITERATORS. +(** * Here are special non dependent useful instantiation of induction +schemes *) + +(** Uniform application on the arguments of the vector *) +Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n := + fix map_fix {n} (v : t A n) : t B n := match v with + | [] => [] + | a :: v' => (f a) :: (map_fix v') + 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. + +(** 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 := + fix fold_left_fix (b:B) {n} (v : t A n) : B := match v with + | [] => b + | a :: w => (fold_left_fix (f b a) w) + end. + +(** fold_right f [x1 .. xn] b = f x1 (f x2 .. (f xn b) .. ) *) +Definition fold_right {A B : Type} (f : A->B->B) := + fix fold_right_fix {n} (v : t A n) (b:B) + {struct v} : B := + match v with + | [] => 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_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 +end. + +End ITERATORS. + +Section SCANNING. +Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop := + |Forall_nil: Forall P [] + |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v). +Hint Constructors Forall. + +Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop := + |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v) + |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v). +Hint Constructors Exists. + +Inductive In {A} (a:A): forall {n}, t A n -> Prop := + |In_cons_hd {m} (v: t A m): In a (a::v) + |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v). +Hint Constructors In. + +Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := + |Forall2_nil: Forall2 P [] [] + |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 -> + Forall2 P (x1::v1) (x2::v2). +Hint Constructors Forall2. + +Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := + |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2) + |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2). +Hint Constructors Exists2. + +End SCANNING. + +Section VECTORLIST. +(** * vector <=> list functions *) + +Fixpoint of_list {A} (l : list A) : t A (length l) := +match l as l' return t A (length l') with + |Datatypes.nil => [] + |(h :: tail)%list => (h :: (of_list tail)) +end. + +Definition to_list {A}{n} (v : t A n) : list A := +Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.nil. +End VECTORLIST. + +Module VectorNotations. +Notation "[]" := [] : vector_scope. +Notation "h :: t" := (h :: t) (at level 60, right associativity) + : vector_scope. +Notation " [ x ] " := (x :: []) : vector_scope. +Notation " [ x ; .. ; y ] " := (cons _ x _ .. (cons _ y _ (nil _)) ..) : vector_scope +. +Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. +Open Scope vector_scope. +End VectorNotations. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v new file mode 100644 index 00000000..a576315e --- /dev/null +++ b/theories/Vectors/VectorSpec.v @@ -0,0 +1,113 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Proofs of specification for functions defined over Vector + + Author: Pierre Boutillier + Institution: PPS, INRIA 12/2010 +*) + +Require Fin. +Require Import VectorDef. +Import VectorNotations. + +(** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all +is true for the one that use [lt] *) + +Lemma eq_nth_iff A n (v1 v2: t A n): + (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2. +Proof. +split. + revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros. + reflexivity. + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl). + apply H. intros p1 p2 H1; + apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)). + intros; now f_equal. +Qed. + +Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n), + nth_order v H = last v. +Proof. +unfold nth_order; refine (@rectS _ _ _ _); now simpl. +Qed. + +Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): + nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2. +Proof. +subst k2; induction k1. + generalize dependent n. apply caseS ; intros. now simpl. + generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl. +Qed. + +Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a. +Proof. +induction v ;now simpl. +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. + 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 + |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. +Qed. + +Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v. +Proof. +refine (@rectS _ _ _ _); now simpl. +Qed. + +Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a. +Proof. +now induction p. +Qed. + +Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2): + (map f v) [@ p1] = f (v [@ p2]). +Proof. +subst p2; induction p1. + revert n v; refine (@caseS _ _ _); now simpl. + revert n v p1 IHp1; refine (@caseS _ _ _); now simpl. +Qed. + +Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n): + p1 = p2 -> p2 = p3 -> (map2 f v w) [@p1] = f (v[@p2]) (w[@p3]). +Proof. +intros; subst p2; subst p3; revert n v w p1. +refine (@rect2 _ _ _ _ _); simpl. + exact (Fin.case0 _). + intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _); + now simpl. +Qed. + +Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} + (assoc: forall a b c, f (f a b) c = f (f a c) b) + {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a. +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. + induction v. + reflexivity. + simpl. intros; now rewrite<- (IHv). +Qed. + +Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l. +Proof. +induction l. + reflexivity. + unfold to_list; simpl. now f_equal. +Qed. diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget new file mode 100644 index 00000000..7f00d016 --- /dev/null +++ b/theories/Vectors/vo.itarget @@ -0,0 +1,4 @@ +Fin.vo +VectorDef.vo +VectorSpec.vo +Vector.vo |