From 703e5b595a4a96dc9ff3df7ad10f90a238a061b6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 8 Sep 2015 17:46:21 +0200 Subject: Emphasizing that eta for vectors is an instance of caseS, as pointed out to me by Pierre B. Also extending use of bullets in Vectors where relevant. --- theories/Vectors/Fin.v | 32 ++++++++++++++--------------- theories/Vectors/VectorSpec.v | 47 +++++++++++++++++++------------------------ 2 files changed, 37 insertions(+), 42 deletions(-) (limited to 'theories/Vectors') diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index b9bf6c7f7..2955184f6 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -152,18 +152,18 @@ Fixpoint L {m} n (p : t m) : t (m + n) := 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). +- 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). Proof. induction n. - exact p. - exact ((fix LS k (p: t k) := +- exact p. +- exact ((fix LS k (p: t k) := match p with |@F1 k' => @F1 (S k') |FS p' => FS (LS _ p') @@ -178,8 +178,8 @@ Fixpoint R {m} n (p : t m) : t (n + m) := 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). +- 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) := @@ -192,9 +192,9 @@ 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)). Proof. induction o ; simpl. - rewrite L_sanity. now rewrite Mult.mult_0_r. +- rewrite L_sanity. now rewrite Mult.mult_0_r. - rewrite R_sanity. rewrite IHo. +- 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. @@ -210,10 +210,10 @@ 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. +- 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. @@ -231,9 +231,9 @@ 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. +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. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 46b537737..c5278b918 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -24,12 +24,7 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v. Proof. - change - (match S n with - | 0 => fun v : t A 0 => v = v - | S n => fun v => v = hd v :: tl v - end v). - destruct v; reflexivity. +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 @@ -39,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), @@ -57,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. @@ -70,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]) -> @@ -94,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): @@ -103,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. @@ -113,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. -- cgit v1.2.3