diff options
author | George Stelle <stelleg@lanl.gov> | 2017-03-09 10:48:10 -0700 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-30 00:12:40 +0200 |
commit | dfc89e3c2fb5e3801307b5b8b5491a38aa1630bb (patch) | |
tree | ee6427927e2e56b19a50ca3820e332c19787796f /theories/Vectors | |
parent | cae09e5af6cf31d96662b1b66a63c6a236a8e741 (diff) |
Added take to VectorDef.
Added a function that takes the first [p] elements of a vector, and
a few lemmas proving some of its properties.
Diffstat (limited to 'theories/Vectors')
-rw-r--r-- | theories/Vectors/VectorDef.v | 10 | ||||
-rw-r--r-- | theories/Vectors/VectorSpec.v | 29 |
2 files changed, 39 insertions, 0 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 1f8b76cb6..c49451776 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -147,6 +147,16 @@ 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. +(** Take first [p] elements of a vector *) +Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := + match p as p return p <= n -> t A p with + | 0 => fun _ => [] + | S p' => match v in t _ n return S p' <= n -> t A (S p') with + | []=> fun le => False_rect _ (Nat.nle_succ_0 p' le) + | x::xs => fun le => x::take p' (le_S_n p' _ le) xs + end + end le. + (** Remove [p] last elements of a vector *) Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n -> t A (n - p). diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index c5278b918..869d0fb5a 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -122,3 +122,32 @@ induction l. - reflexivity. - unfold to_list; simpl. now f_equal. Qed. + +Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. +Proof. + reflexivity. +Qed. + +Lemma take_idem : forall {A} p n (v:t A n) le le', + take p le' (take p le v) = take p le v. +Proof. + induction p; intros n v le le'. + - auto. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Qed. + +Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v. +Proof. + induction v; intros m w le. + - reflexivity. + - simpl. apply f_equal. apply IHv. +Qed. + +(* Proof is irrelevant for [take] *) +Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v. +Proof. + induction p; intros n v le le'. + - reflexivity. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Qed. + |