diff options
Diffstat (limited to 'theories/Vectors/VectorSpec.v')
| -rw-r--r-- | theories/Vectors/VectorSpec.v | 45 |
1 files changed, 25 insertions, 20 deletions
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 7f4228dd..c5278b91 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -22,6 +22,11 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} with | eq_refl => conj eq_refl eq_refl end. +Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v. +Proof. +intros; apply caseS with (v:=v); intros; reflexivity. +Defined. + (** 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] *) @@ -29,12 +34,12 @@ 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). +- 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. +- intros; now f_equal. Qed. Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n), @@ -47,8 +52,8 @@ 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. +- 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. @@ -60,8 +65,8 @@ 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 _ _ _); lazy beta; [ intros n v | intros n p H v ]. - revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. - revert p H. +- 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' -> 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]) -> @@ -84,8 +89,8 @@ 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. +- 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): @@ -93,8 +98,8 @@ Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n): 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 _ _ _); +- exact (Fin.case0 _). +- intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _); now simpl. Qed. @@ -103,17 +108,17 @@ Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} {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, assoc. now f_equal. - induction v. - reflexivity. - simpl. intros; now rewrite<- (IHv). +- induction v0. + + now simpl. + + intros; simpl. rewrite<- IHv0, assoc. 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. +- reflexivity. +- unfold to_list; simpl. now f_equal. Qed. |