edits per review

doc/changelog/10-standard-library/09379-splitAt.rst

@@ -1,4 +1,4 @@
-- Added ``splitAt`` function and lemmas about ``splitAt`` and ``uncons``
+- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
   (`#9379 <https://github.com/coq/coq/pull/9379>`_,
   by Yishuai Li, with help of Konstantinos Kallas,
   follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,

theories/Init/Datatypes.v

@@ -243,15 +243,17 @@ Proof.
   rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
-Lemma single_valued_projections :
+Lemma pair_equal_spec :
   forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
-    (a1, b1) = (a2, b2) -> a1 = a2 /\ b1 = b2.
+    (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
 Proof with auto.
   split; intros.
-  - replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
-    rewrite H...
-  - replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
-    rewrite H...
+  - split.
+    + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
+      rewrite H...
+    + replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
+      rewrite H...
+  - destruct H; subst...
 Qed.
 
 Definition prod_uncurry (A B C:Type) (f:A * B -> C)

theories/Vectors/VectorDef.v

@@ -190,12 +190,12 @@ Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) :=
 Infix "++" := append.
 
 (** Split a vector into two parts *)
-Fixpoint splitAt {A} (l : nat) {r : nat} :
+Fixpoint splitat {A} (l : nat) {r : nat} :
   t A (l + r) -> t A l * t A r :=
   match l with
   | 0 => fun v => ([], v)
   | S l' => fun v =>
-    let (v1, v2) := splitAt l' (tl v) in
+    let (v1, v2) := splitat l' (tl v) in
     (hd v::v1, v2)
   end.
 

theories/Vectors/VectorSpec.v

@@ -153,18 +153,6 @@ Proof.
   - destruct v. inversion le. simpl. apply f_equal. apply IHp. 
 Qed.
 
-Lemma single_valued_uncons {A} : forall {n : nat} (a1 a2 : A) (v1 v2 : t A n),
-    a1::v1 = a2::v2 -> a1 = a2 /\ v1 = v2.
-Proof with auto.
-  split; intros.
-  - replace a1 with (hd (a1::v1));
-    replace a2 with (hd (a2::v2))...
-    rewrite H...
-  - replace v1 with (tl (a1::v1));
-    replace v2 with (tl (a2::v2))...
-    rewrite H...
-Qed.
-
 Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n),
     uncons (a::v) = (a,v).
 Proof. reflexivity. Qed.
@@ -173,28 +161,28 @@ Lemma append_comm_cons {A} : forall {n m : nat} (v : t A n) (w : t A m) (a : A),
     a :: (v ++ w) = (a :: v) ++ w.
 Proof. reflexivity. Qed.
 
-Lemma splitAt_append {A} : forall {n m : nat} (v : t A n) (w : t A m),
-    splitAt n (v ++ w) = (v, w).
+Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m),
+    splitat n (v ++ w) = (v, w).
 Proof with simpl; auto.
   intros n m v.
   generalize dependent m.
   induction v; intros...
   rewrite IHv...
 Qed.
 
-Lemma append_splitAt {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A (n+m)),
-    splitAt n vw = (v, w) ->
+Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A (n+m)),
+    splitat n vw = (v, w) ->
     vw = v ++ w.
 Proof with auto.
   intros n m v.
   generalize dependent m.
   induction v; intros; inversion H...
-  destruct (splitAt n (tl vw)) as [v' w'] eqn:Heq.
-  apply single_valued_projections in H1.
+  destruct (splitat n (tl vw)) as [v' w'] eqn:Heq.
+  apply pair_equal_spec in H1.
   destruct H1; subst.
   rewrite <- append_comm_cons.
   rewrite (eta vw).
-  apply single_valued_uncons in H0.
+  apply cons_inj in H0.
   destruct H0; subst.
   f_equal...
   apply IHv...