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.

2 files changed, 37 insertions, 42 deletions

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.