Vectors: lemmas about uncons and splitAt

Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>

5 files changed, 73 insertions, 1 deletions

diff --git a/CREDITS b/CREDITS
index 989e449cc5..888824aa31 100644
--- a/CREDITS
+++ b/CREDITS
@@ -112,6 +112,7 @@ 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,
@@ -119,7 +120,7 @@ of the Coq Proof assistant during the indicated time:
   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,
diff --git a/doc/changelog/10-standard-library/09379-splitAt.rst b/doc/changelog/10-standard-library/09379-splitAt.rst
new file mode 100644
index 0000000000..af00213c9c
--- /dev/null
+++ b/doc/changelog/10-standard-library/09379-splitAt.rst
@@ -0,0 +1,4 @@
+- Added ``uncons`` and ``splitAt`` functions over vectors,
+  and proved some lemmas about them
+  (`#9379 <https://github.com/coq/coq/pull/9379>`_,
+  by Yishuai Li, with help of Konstantinos Kallas).
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1639115cbd..aff081df12 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -243,6 +243,17 @@ Proof.
   rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
+Lemma single_valued_projections :
+  forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
+    (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...
+Qed.
+
 Definition prod_uncurry (A B C:Type) (f:A * B -> C)
   (x:A) (y:B) : C := f (x,y).
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 20a8581d46..a25722f4b0 100644
--- a/theories/Vectors/VectorDef.v
+++ b/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 *)
 
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 55a55c0b2f..1626c4aee7 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -153,3 +153,49 @@ 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.
+
+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 single_valued_projections in H1.
+  destruct H1; subst.
+  rewrite <- append_comm_cons.
+  rewrite (eta vw).
+  apply single_valued_uncons in H0.
+  destruct H0; subst.
+  f_equal...
+  apply IHv...
+Qed.