added nil_spec, removed pattern

Author: mrhaandi

theories/Vectors/Fin.v

@@ -161,10 +161,8 @@ Qed.
 
 Lemma L_inj {m} n (p q : t m) : L n p = L n q -> p = q.
 Proof.
-induction p as [m|m p IH]; pattern q.
-- now apply caseS'.
-- apply caseS'; [discriminate|].
-  intros ??. f_equal. now apply IH, FS_inj.
+induction p as [m|m p IH]; apply (caseS' q); [easy..|].
+intros ??. f_equal. now apply IH, FS_inj.
 Qed.
 
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of

theories/Vectors/VectorSpec.v

@@ -24,9 +24,14 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
    with | eq_refl => conj eq_refl eq_refl
    end.
 
+Lemma nil_spec {A} (v : t A 0) : v = [].
+Proof.
+apply (fun P E => case0 P E v). reflexivity.
+Defined.
+
 Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v.
 Proof.
-intros; apply (fun P IS => caseS P IS (n := n) v); intros; reflexivity.
+apply (fun P IS => caseS P IS (n := n) v); intros; reflexivity.
 Defined.
 
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
@@ -103,17 +108,18 @@ Qed.
 Lemma nth_replace_eq A: forall n p (v : t A n) a,
   nth (replace v p a) p = a.
 Proof.
-intros n p v a. induction v; pattern p.
-- apply Fin.case0.
-- now apply Fin.caseS'.
+intros n p v a. induction v.
+- now apply Fin.case0.
+- now apply (Fin.caseS' p).
 Qed.
 
 Lemma nth_replace_neq A: forall n p q, p <> q -> forall (v : t A n) a,
   nth (replace v q a) p = nth v p.
 Proof.
-intros n p q Hpq v a. induction v as [|b n v IH]; revert Hpq; pattern p.
-- apply Fin.case0.
-- apply Fin.caseS'; pattern q; apply Fin.caseS'; [easy..|].
+intros n p q Hpq v a.
+induction v as [|b n v IH]; revert Hpq.
+- now apply Fin.case0.
+- apply (Fin.caseS' p); apply (Fin.caseS' q); [easy..|].
   intros ???. apply IH. intros ?. now subst.
 Qed.
 
@@ -171,7 +177,7 @@ Lemma replace_append_L A: forall n m (v : t A n) (w : t A m) p a,
   replace (v ++ w) (Fin.L m p) a = (replace v p a) ++ w.
 Proof.
 intros n m v w p a. induction v as [|b n v IH].
-- pattern p. apply Fin.case0.
+- now apply Fin.case0.
 - apply (Fin.caseS' p).
   + reflexivity.
   + intros p'. cbn. apply f_equal, IH.
@@ -256,9 +262,10 @@ Qed.
 Lemma map2_ext A B C: forall (f g:A->B->C), (forall a b, f a b = g a b) ->
   forall n (v : t A n) (w : t B n), map2 f v w = map2 g v w.
 Proof.
-intros f g Hfg n v w. pattern n, v, w. apply rect2.
+intros f g Hfg n v w.
+apply (fun P H1 H2 => rect2 P H1 H2 v w).
 - reflexivity.
-- cbn. congruence.
+- cbn. intros ??? IH ??. now rewrite IH, Hfg.
 Qed.
 
 (** ** Properties of [fold_left] *)
@@ -448,7 +455,7 @@ intros P n v1 v2. split.
 - intros H. induction H.
   + apply Fin.case0.
   + intros p. now apply (Fin.caseS' p).
-- pattern n, v1, v2. apply rect2.
+- apply (fun P H1 H2 => rect2 P H1 H2 v1 v2).
   + constructor.
   + intros ??? IH ?? H. constructor.
     * apply (H Fin.F1).