Merge PR #9379: Vectors: lemmas about uncons and splitAt

Reviewed-by: Zimmi48
Reviewed-by: herbelin

CREDITS

@@ -112,14 +112,15 @@ of the Coq Proof assistant during the indicated time:
   Hugo Herbelin (INRIA, 1996-now)
   Sébastien Hinderer (INRIA, 2014)
   Gérard Huet (INRIA, 1985-1997)
+  Konstantinos Kallas (U. Penn, 2019)
   Matej Košík (INRIA, 2015-2017)
   Leonidas Lampropoulos (University of Pennsylvania, 2018)
   Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
                    INRIA-PPS then IRIF, 2009-now)
   Yao Li (ORCID: https://orcid.org/0000-0001-8720-883X,
           University of Pennsylvania, 2018)
   Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903
-              U. Penn, 2018)
+              U. Penn, 2018-2019)
   Patrick Loiseleur (Paris Sud, 1997-1999)
   Evgeny Makarov (INRIA, 2007)
   Gregory Malecha (Harvard University 2013-2015,

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

@@ -0,0 +1,5 @@
+- 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>`_,
+  which added ``uncons`` in 8.10+beta1).

theories/Init/Datatypes.v

@@ -243,6 +243,19 @@ Proof.
   rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
+Lemma pair_equal_spec :
+  forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
+    (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
+Proof with auto.
+  split; intros.
+  - 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)
   (x:A) (y:B) : C := f (x,y).
 

theories/Vectors/VectorDef.v

@@ -189,6 +189,16 @@ 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} :
+  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
+    (hd v::v1, v2)
+  end.
+
 (** Two definitions of the tail recursive function that appends two lists but
 reverses the first one *)
 

theories/Vectors/VectorSpec.v

@@ -153,3 +153,37 @@ Proof.
   - destruct v. inversion le. simpl. apply f_equal. apply IHp. 
 Qed.
 
+Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n),
+    uncons (a::v) = (a,v).
+Proof. reflexivity. Qed.
+
+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).
+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) ->
+    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 pair_equal_spec in H1.
+  destruct H1; subst.
+  rewrite <- append_comm_cons.
+  rewrite (eta vw).
+  apply cons_inj in H0.
+  destruct H0; subst.
+  f_equal...
+  apply IHv...
+Qed.