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

Reviewed-by: Zimmi48
Reviewed-by: herbelin

3 files changed, 57 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 3e0bf1d8ae..6984a7c2b6 100644
--- a/theories/Init/Datatypes.v
+++ b/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).
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 20a8581d46..cba4780bd4 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..b27566458e 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/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.