Vector: take out some elements from a vector with two methods

Question

I would like to prove a lemma split_assoc.

Require Import Coq.Vectors.Vector.
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coq.Arith.Plus.
From mathcomp Require Import ssreflect. 
Require Import Coq.Lists.List.

Lemma to_list_injective A n (v1 v2 : Vector.t A n) :
  to_list v1 = to_list v2 -> v1 = v2.
Proof.
elim: n / v1 v2=> [|x1 n v1 IH] /= v2.
- by elim/@case0: v2.
- by elim/@caseS': v2=> x2 v2 [-> /IH ->].
Qed.

Lemma to_list_splitat1 A n m (v : Vector.t A (n + m)) :
  to_list (fst (splitat n v)) = firstn n (to_list v).
Proof.
elim: n v=> [|n IH] //=.
elim/@caseS'=> x v /=.
rewrite -IH.
by case: (splitat n v).
Qed.

Lemma split_assoc (A:Type)(a b c:nat)(v:t A ((a+b)+c)): 
      fst (splitat a (fst (splitat (a+b) v))) = fst (splitat a (Vcast v (plus_assoc_reverse a b c))).
Proof.
apply to_list_injective.
rewrite !to_list_splitat1.
induction a => //.
Abort.

I tried to change the vector to the list, but I don't know any more.

Help me, please.

Answer 1

I have proved on my own.

Require Import Coq.Vectors.Vector.
Require Import CoLoR.Util.Vector.VecUtil.
From mathcomp Require Import ssreflect. 
Require Import Coq.Lists.List.
Require Import Coq.Arith.Plus.

Lemma to_list_injective A n (v1 v2 : Vector.t A n) :
  to_list v1 = to_list v2 -> v1 = v2.
Proof.
elim: n / v1 v2=> [|x1 n v1 IH] /= v2.
- by elim/@case0: v2.
- by elim/@caseS': v2=> x2 v2 [-> /IH ->].
Qed.

Lemma to_list_splitat1 A n m (v : Vector.t A (n + m)) :
  to_list (fst (splitat n v)) = firstn n (to_list v).
Proof.
elim: n v=> [|n IH] //=.
elim/@caseS'=> x v /=.
rewrite -IH.
by case: (splitat n v).
Qed.

Lemma firstn_eq (A:Type)(l:list A): forall(a b:nat), firstn a (firstn (a+b) l) = firstn a l.
Proof.
induction l.
destruct a; trivial.
intros.
destruct a0; trivial.
rewrite plus_Sn_m.
rewrite !firstn_cons.
rewrite (IHl a0 b); trivial.
Qed.

Lemma to_list_cons_app (A:Type)(n:nat)(a:A)(v:t A n): to_list (Vcons a v) = a :: (to_list v).
Proof.
reflexivity.
Qed.

Lemma Vcast_eq (A:Type): forall (n:nat)(v:t A n)(m:nat)(p:n=m),
      to_list v = to_list (Vcast v p).
Proof.
induction v.
intros; destruct (Vcast Vnil p); trivial.
inversion p.
intros.
destruct m.
inversion p.
rewrite Vcast_cons.
remember (eq_add_S p).
rewrite !to_list_cons_app.
f_equal.
apply (IHv m e).
Qed.

Lemma split_assoc (A:Type)(a b c:nat)(v:t A ((a+b)+c)): 
      fst (splitat a (fst (splitat (a+b) v))) = fst (splitat a (Vcast v (plus_assoc_reverse a b c))).
Proof.
apply to_list_injective.
rewrite !to_list_splitat1.
rewrite firstn_eq.
rewrite (Vcast_eq A (a+b+c) v (a+(b+c)) (plus_assoc_reverse a b c)); trivial.
Qed.