HyPre.util.VectorExtra

(* CLN B *)
From Coq Require Vectors.Vector.
From Coq Require Export Lists.List.
From Coq Require Import Equality.
Import ListNotations.

From HyPre Require Export
     Tac
     ListExtra.

Definition t_combine {A B : Type} {n : nat}
  := Vector.map2 (n:=n) (@pair A B).

Lemma t_combine_fst {k} {X Y : Type} (a : Vector.t X k) (b : Vector.t Y k)
  : Vector.map fst (t_combine a b) = a.
Proof.
  dependent induction a;dependent destruction b;cbn.
  - reflexivity.
  - f_equal.
    eapply IHa.
Qed.

Lemma t_combine_snd {k} {X Y : Type} (a : Vector.t X k) (b : Vector.t Y k)
  : Vector.map snd (t_combine a b) = b.
Proof.
  dependent induction a;dependent destruction b;cbn.
  - reflexivity.
  - f_equal.
    eapply IHa.
Qed.

Lemma t_combine_self {k} {X Y : Type} (a : Vector.t (X * Y) k)
  : a = t_combine (Vector.map fst a) (Vector.map snd a).
Proof.
  dependent induction a;cbn.
  - reflexivity.
  - f_equal.
    + eapply surjective_pairing.
    + eapply IHa.
Qed.

Definition map3 {A B C D : Type}
           (f : A -> B -> C -> D) {n : nat}
  : Vector.t A n -> Vector.t B n -> Vector.t C n -> Vector.t D n
  := fun att bt => Vector.map2 (fun (ab : A*B) => let (a,b) := ab in f a b) (t_combine att bt).

Fixpoint map4 {A B C D E : Type}
         (f : A -> B -> C -> D -> E) {n : nat}
         (a : Vector.t A n) (b : Vector.t B n) (c : Vector.t C n) (d : Vector.t D n)
  : Vector.t E n.
Proof.
  dependent destruction a;
    dependent destruction b;
    dependent destruction c;
    dependent destruction d.
  - econstructor.
  - econstructor.
    + eapply f;eauto.
    + eapply map4;eauto.
Defined.

Lemma vec_map2_map2_map4 {A B C D X Y Z : Type}
      (f1 : A -> B -> X)
      (f2 : C -> D -> Y)
      (g : X -> Y -> Z)
      {n : nat}
      (a : Vector.t A n) (b : Vector.t B n) (c : Vector.t C n) (d : Vector.t D n)
  : Vector.map2 g (Vector.map2 f1 a b) (Vector.map2 f2 c d)
    = map4 (fun a' b' c' d' => g (f1 a' b') (f2 c' d')) a b c d.
Proof.
  dependent induction a;
    dependent destruction b;
    dependent destruction c;
    dependent destruction d;
    cbn.
  - reflexivity.
  - f_equal.
    eapply IHa.
Qed.

Lemma vec_map4_ext {A B C D E : Type}
      (f f' : A -> B -> C -> D -> E) {n : nat}
      (H : forall a' b' c' d', f a' b' c' d' = f' a' b' c' d')
         (a : Vector.t A n) (b : Vector.t B n) (c : Vector.t C n) (d : Vector.t D n)
  : map4 f a b c d = map4 f' a b c d.
Proof.
  dependent induction a;
    dependent destruction b;
    dependent destruction c;
    dependent destruction d;
    cbn.
  - reflexivity.
  - f_equal.
    + eapply H.
    + eapply IHa.
Qed.

Definition repl {X : Type} {k : nat} : Vector.t X k -> Vector.t X k -> Vector.t bool k -> Vector.t X k
  := map3 (fun x y (b : bool) => if b then y else x).

Fixpoint vb_zero (k:nat) : Vector.t bool k
  := match k with
     | O => Vector.nil _
     | S k' => Vector.cons _ false _ (vb_zero k')
     end.

Lemma Vector_Forall_dec {X : Type} {n : nat} (xt : Vector.t X n) (f : X -> bool)
  : {Vector.Forall (fun x => f x = true) xt} + {Vector.Exists (fun x => f x = false) xt}.
Proof.
  dependent induction xt;cbn.
  - left.
    eapply Vector.Forall_nil.
  - specialize (IHxt f).
    destruct IHxt.
    + destruct (f h) eqn:E.
      * left.
        econstructor;eauto.
      * right.
        econstructor;eauto.
    + right.
      eapply Vector.Exists_cons_tl.
      assumption.
Qed.

Lemma Vector_Exists_nth {X : Type} {n : nat} (P : X -> Prop) (xt : Vector.t X n)
  : Vector.Exists P xt -> exists (i : Fin.t n), P (Vector.nth xt i).
Proof.
  intros.
  dependent induction H.
  - exists (Fin.F1).
    cbn.
    assumption.
  - destruct IHExists.
    exists (Fin.FS x0).
    cbn.
    assumption.
Qed.

Lemma vec_nth_nth_order {X : Type} {k} (xt : Vector.t X k) (i : Fin.t k)
  : Vector.nth xt i = Vector.nth_order xt (proj2_sig (Fin.to_nat i)).
Proof.
  unfold Vector.nth_order.
  f_equal.
  eapply Fin.to_nat_inj.
  rewrite Fin.to_nat_of_nat.
  cbn.
  reflexivity.
Qed.

Lemma Vector_nth_replace {X : Type} {n : nat} (xt : Vector.t X n) (i : Fin.t n) (x : X)
  : Vector.nth (Vector.replace xt i x) i = x.
Proof.
  rewrite vec_nth_nth_order.
  setoid_rewrite <-Vector.nth_order_replace_eq
    with (a:=x) (v:=xt) (H1:=proj2_sig (Fin.to_nat i)) (H2:=proj2_sig (Fin.to_nat i)) at 2.
  f_equal.
  f_equal.
  eapply Fin.to_nat_inj.
  rewrite Fin.to_nat_of_nat.
  cbn.
  reflexivity.
Qed.

Notation "a [[ i ]]" := (Vector.nth a i) (at level 40).

Lemma Vec_Forall2_forall2 {k : nat} (X Y : Type) (P : X -> Y -> Prop) (xt : Vector.t _ k) yt
  : Vector.Forall2 P xt yt <-> forall i, P (Vector.nth xt i) (Vector.nth yt i).
Proof.
  split;intros.
  - dependent induction H.
    + inversion i.
    + dependent destruction i;cbn;eauto.
  - dependent induction xt;dependent destruction yt.
    + econstructor.
    + econstructor.
      * specialize (H Fin.F1).
        cbn in H.
        assumption.
      * eapply IHxt.
        intros.
        specialize (H (Fin.FS i)).
        cbn in H.
        assumption.
Qed.

Inductive Vec_Forall3 {A B C : Type} (P : A -> B -> C -> Prop)
  : forall {n : nat}, Vector.t A n -> Vector.t B n -> Vector.t C n -> Prop
  :=
  | Forall3_nil : Vec_Forall3 P (Vector.nil A) (Vector.nil B) (Vector.nil C)
  | Forall3_cons :
      forall (m : nat) (x1 : A) (x2 : B) (x3 : C) (v1 : Vector.t A m) (v2 : Vector.t B m) (v3 : Vector.t C m),
        P x1 x2 x3 -> Vec_Forall3 P v1 v2 v3
        -> Vec_Forall3 P (Vector.cons A x1 m v1) (Vector.cons B x2 m v2) (Vector.cons C x3 m v3).

Lemma vec_0_nil {X : Type} (v : Vector.t X 0)
  : v = Vector.nil X.
Proof.
  revert v.
  eapply Vector.case0.
  reflexivity.
Qed.

Lemma vec_nil_eq {X : Type} (v v' : Vector.t X 0)
  : v = v'.
Proof.
  rewrite vec_0_nil. rewrite vec_0_nil at 1.
  reflexivity.
Qed.

From Coq Require Import Lia.

Lemma le_inv_S (n m : nat)
  : S n <= m -> S (m - S n) <= m.
Proof.
  lia.
Qed.

Fixpoint vec_mapi' {k} {A B : Type} {n : nat} (H : n <= k) (f : Fin.t k -> A -> B) (a : Vector.t A n) : Vector.t B n :=
  match a in (Vector.t _ n0) return (n0 <= k -> Vector.t B n0) with
  | Vector.nil _ => fun _ : 0 <= k => Vector.nil B
  | Vector.cons _ h n0 t =>
    (fun (h0 : A) (n1 : nat) (a0 : Vector.t A n1) (H0 : S n1 <= k) =>
       Vector.cons B (f (Fin.of_nat_lt (le_inv_S _ _ H0)) h0) n1 (vec_mapi' (Le.le_Sn_le_stt n1 k H0) f a0)) h n0 t
  end H.

Definition vec_mapi {k} :
  forall {A B : Type}, (Fin.t k -> A -> B) -> Vector.t A k -> Vector.t B k
  := (fun (A B : Type) (X : Fin.t k -> A -> B) (X0 : Vector.t A k) => vec_mapi' (le_n k) X X0).

Fixpoint vec_mapi2' {k} {A B C : Type} {n : nat} (H : n <= k)
         (f : Fin.t k -> A -> B -> C) (a : Vector.t A n) (b : Vector.t B n) : Vector.t C n.
Proof.
  remember n as n'.
  rewrite Heqn' in a.
  destruct a, b.
  2,3:congruence.
  - econstructor.
  - econstructor.
    + eapply f;eauto.
      eapply le_inv_S in H.
      eapply (Fin.of_nat_lt H).
    + eapply vec_mapi2'.
      2,4: eassumption.
      * eapply Le.le_Sn_le_stt.
        eassumption.
      * erewrite eq_add_S;eauto.
Defined.

Definition vec_mapi2 {k} :
  forall {A B C : Type}, (Fin.t k -> A -> B -> C) -> Vector.t A k -> Vector.t B k -> Vector.t C k
  := (fun (A B C : Type) (f : Fin.t k -> A -> B -> C) => vec_mapi2' (le_n k) f).

Lemma vec_fold_left_max_start {k} (a : Vector.t nat k)
  : forall x y, x <= y -> x <= Vector.fold_left Nat.max y a.
Proof.
  dependent induction a;cbn;intros.
  - assumption.
  - setoid_rewrite <-IHa;eauto.
    lia.
Qed.

Lemma Vec_fold_left_max {k}
  : forall (a : Vector.t nat k) i x, a [[i]] <= Vector.fold_left Nat.max x a.
Proof.
  intros.
  dependent induction a; dependent destruction i;cbn.
  - setoid_rewrite <-vec_fold_left_max_start.
    + reflexivity.
    + lia.
  - rewrite IHa.
    reflexivity.
Qed.

Local Arguments Fin.F1 : clear implicits.
Local Arguments Fin.of_nat_lt : clear implicits.

Lemma of_nat_lt_eq_eq (k x y : nat) (Qx : x < k) (Qy : y < k) (H : x = y)
  : Fin.of_nat_lt x k Qx = Fin.of_nat_lt y k Qy.
Proof.
  revert k y Qx Qy H.
  induction x;destruct y;intros;try congruence.
  - eapply Fin.of_nat_ext.
  - destruct k;cbn.
    + exfalso. lia.
    + match goal with |- _ = _ (_ _ _ ?Q) => rewrite IHx with (y:=y) (Qy:=Q) at 1 end.
      * reflexivity.
      * lia.
Qed.

Lemma vec_nth_mapi2' {A B C : Type} {k n} (Hle : n <= k)
      (f : Fin.t k -> A -> B -> C) (a b : Vector.t _ n) (i : Fin.t n) (i' : Fin.t k)
      (Heq : proj1_sig (Fin.to_nat i) + k - n = proj1_sig (Fin.to_nat i'))
  : vec_mapi2' Hle f a b [[i]] = f i' (a [[i]]) (b [[i]]).
Proof.
  dependent induction a; dependent destruction b;dependent destruction i;[cbn|].
  - f_equal.
    cbn in Heq.
    rewrite <-Fin.of_nat_to_nat_inv with (p:=i').
    eapply of_nat_lt_eq_eq;eauto.
  - cbn. setoid_rewrite <-IHa. reflexivity.
    cbn in Heq.
    destruct (Fin.to_nat i).
    cbn in Heq. cbn.
    assumption.
Qed.

Lemma Vec_nth_mapi2 {A B C : Type} {k} (f : Fin.t k -> A -> B -> C) (a b : Vector.t _ k) (i : Fin.t k)
  : vec_mapi2 f a b [[i]] = f i (a [[i]]) (b [[i]]).
Proof.
  eapply vec_nth_mapi2'.
  lia.
Qed.

Lemma vec_mapi_nth' {k} {X Y : Type} (f : Fin.t k -> X -> Y) n
      (Hle : n <= k)
      (x : Vector.t X n) (i : Fin.t n) (i' : Fin.t k)
      (Heq : proj1_sig (Fin.to_nat i) + k - n = proj1_sig (Fin.to_nat i'))
  : vec_mapi' Hle f x [[i]] = f i' (x [[i]]).
Proof.
  dependent induction x; dependent destruction i;cbn.
  - f_equal.
    cbn in Heq.
    rewrite <-Fin.of_nat_to_nat_inv with (p:=i').
    eapply of_nat_lt_eq_eq;eauto.
  - cbn. setoid_rewrite <-IHx. reflexivity.
    cbn in Heq.
    destruct (Fin.to_nat i).
    cbn in Heq. cbn.
    assumption.
Qed.

Lemma vec_mapi_nth {k} {X Y : Type} (f : Fin.t k -> X -> Y) (xt : Vector.t X k) (i : Fin.t k)
  : vec_mapi f xt [[i]] = f i (xt [[i]]).
Proof.
  eapply vec_mapi_nth'.
  lia.
Qed.

Lemma Vec_nth_map2 {k} {A B C : Type} (f : A -> B -> C) (a b : Vector.t _ k) (i : Fin.t k)
  : Vector.map2 f a b [[i]] = f (a [[i]]) (b [[i]]).
Proof.
  dependent induction a; dependent destruction b; dependent destruction i;cbn.
  - reflexivity.
  - eapply IHa.
Qed.

Lemma vec_map_const {k} {X Y : Type} (f : X -> Y) x
  : Vector.map f (Vector.const x k) = Vector.const (f x) k.
Proof.
  clear.
  induction k;cbn.
  - reflexivity.
  - rewrite IHk. reflexivity.
Qed.

Lemma vec_map_map2 {k} {W X Y Z : Type} (f : Z -> W) (g : X -> Y -> Z) (x y : Vector.t _ k)
  : Vector.map f (Vector.map2 g x y) = Vector.map2 (fun x y => f (g x y)) x y.
Proof.
  clear.
  dependent induction x; dependent destruction y.
  - cbn. reflexivity.
  - cbn. rewrite IHx. reflexivity.
Qed.

Lemma vec_map2_ext {k} {X Y Z : Type} (f g : X -> Y -> Z)
  : (forall x y, f x y = g x y) -> forall (xt yt : Vector.t _ k), Vector.map2 f xt yt = Vector.map2 g xt yt.
Proof.
  clear.
  intros.
  dependent induction k;cbn.
  - dependent destruction xt. dependent destruction yt.
    cbn. reflexivity.
  - dependent destruction xt. dependent destruction yt.
    cbn. setoid_rewrite IHk. 2,3: eauto. rewrite H. reflexivity.
Qed.

Lemma vec_map2_fun_app {k} {X X1 Y Y1 Z : Type}
      (fx : X -> X1) (fy : Y -> Y1) (g : X1 -> Y1 -> Z) (xt yt : Vector.t _ k)
  : Vector.map2 (fun x y => g (fx x) (fy y)) xt yt = Vector.map2 g (Vector.map fx xt) (Vector.map fy yt).
Proof.
  clear.
  dependent induction xt; dependent destruction yt;cbn.
  - reflexivity.
  - rewrite IHxt. reflexivity.
Qed.

Definition vl_zero {X : Type} {k : nat} := Vector.const (@nil X) k.

Fixpoint vec_descending (k : nat) {struct k} : Vector.t (Fin.t k) k
  := match k with
     | O => Vector.nil _
     | (S k') => Vector.cons _ (@Fin.F1 k') _ (Vector.map Fin.FS (vec_descending k'))
     end.

Lemma vec_descending_S (k : nat)
  : vec_descending (S k) = Vector.cons _ (@Fin.F1 k) _ (Vector.map Fin.FS (vec_descending k)).
Proof.
  reflexivity.
Qed.

Definition vec_ascending (k : nat) : Vector.t (Fin.t k) k
  := Vector.rev (vec_descending k).

Definition fin_pred_to_vec {X : Type} {k : nat} (f : Fin.t k -> X) : Vector.t X k
  := Vector.map f (vec_ascending k).

Require Import Lia.
From Coq Require Import NPeano.

Definition vec_k1_sk {X : Type} {k : nat} : Vector.t X (k + 1) -> Vector.t X (S k).
Proof.
  intro xv.
  remember (k+1).
  revert dependent k.
  induction xv.
  - intros. rewrite Nat.add_1_r in Heqn. congruence.
  - intros.
    econstructor.
    + assumption.
    + destruct k;intros.
      * cbn in Heqn.
        destruct n;[|congruence].
        assumption.
      * eapply IHxv. lia.
Defined.

Definition vec_rcons {X : Type} {k : nat} (xv : Vector.t X k) (x : X)
  : Vector.t X (S k)
  := vec_k1_sk (Vector.append xv (Vector.const x 1)).

Fixpoint vec_rev {k : nat} {X : Type} (xt : Vector.t X k)
  : Vector.t X k
  := match xt with
     | Vector.nil _ => Vector.nil X
     | Vector.cons _ x n yt => vec_rcons (vec_rev yt) x
     end.

Lemma list_eq_vec_eq {k : nat} {X : Type} (v v' : Vector.t X k)
  : Vector.to_list v = Vector.to_list v' -> v = v'.
Proof.
  match goal with |- ?g => enough (forall l, l = Vector.to_list v -> l = Vector.to_list v' -> g) as Q end.
  { intros;eapply Q;eauto. }
  intros.
  revert dependent l.
  clear H1.
  dependent induction v;dependent destruction v';intros.
  - reflexivity.
  - destruct l;[cbn in H,H0;congruence|].
    rewrite Vector.to_list_cons in H, H0.
    inversion H.
    inversion H0.
    f_equal.
    + subst h. subst h0.
      reflexivity.
    + eapply IHv;eauto.
Qed.

Lemma vec_rev_rev {X : Type} {k : nat} (xv : Vector.t X k)
  : Vector.rev (Vector.rev xv) = xv.
Proof.
  eapply list_eq_vec_eq.
  setoid_rewrite Vector.to_list_rev.
  setoid_rewrite Vector.to_list_rev.
  eapply rev_involutive.
Qed.

Lemma vec_rev_rev_eq {X : Type} {k : nat} (x y : Vector.t X k)
  : Vector.rev x = Vector.rev y -> x = y.
Proof.
  intros.
  rewrite <-vec_rev_rev.
  rewrite <-vec_rev_rev at 1.
  rewrite H. reflexivity.
Qed.

Lemma vec_eq_rev_rev {X : Type} {k : nat} (x y : Vector.t X k)
  : x = y -> Vector.rev x = Vector.rev y.
Proof.
  intros.
  subst. reflexivity.
Qed.

Lemma Vec_Forall3_eq {X Y : Type} {k : nat} (xt : Vector.t X k) (yt1 yt2 : Vector.t Y k)
  : Vec_Forall3 (fun x y1 y2 => y1 = y2) xt yt1 yt2 -> yt1 = yt2.
Proof.
  intros H.
  induction H.
  - reflexivity.
  - f_equal;eauto.
Qed.

Lemma vector_forall_nth {X : Type} (k : nat) (a : Vector.t X k) P
  : Vector.Forall P a -> forall i, P (a[[i]]).
Proof.
  intros H i.
  induction H.
  - inversion i.
  - dependent destruction i.
    + cbn.
      eauto.
    + cbn.
      eauto.
Qed.

Lemma vector_Forall2_cons_inv {X Y : Type} (x : X) (y : Y) (k : nat) a b P
  : Vector.Forall2 P (Vector.cons X x k a) (Vector.cons Y y k b)
    -> P x y /\ Vector.Forall2 P a b.
Proof.
  intros.
  dependent destruction H.
  split;eauto.
Qed.

Lemma vec_append_const {k k'} {X : Type} (x : X)
  : Vector.append (Vector.const x k) (Vector.const x k') = Vector.const x (k+k').
Proof.
  dependent induction k;cbn.
  - reflexivity.
  - f_equal.
    eapply IHk.
Qed.

Lemma vec_forall3_forall {k} {X Y Z : Type} (f : X -> Y -> Z -> Prop) (x y z : Vector.t _ k)
  : Vec_Forall3 f x y z <-> (forall i, f (x[[i]]) (y[[i]]) (z[[i]])).
Proof.
  split;intros.
  - dependent induction H.
    + inversion i.
    + dependent destruction i;cbn;eauto.
  - dependent induction x;dependent destruction y;dependent destruction z.
    + econstructor.
    + econstructor.
      * specialize (H (@Fin.F1 ( n))).
        cbn in H.
        assumption.
      * eapply IHx.
        intros.
        specialize (H (Fin.FS i)).
        cbn in H.
        assumption.
Qed.

Lemma vec_append_rev {k} {X : Type} (x : Vector.t X k) (y : Vector.t X k)
  : Vector.append (Vector.rev x) (Vector.rev y) = Vector.rev (Vector.append y x).
Proof.
  eapply list_eq_vec_eq.
  rewrite Vector.to_list_append.
  setoid_rewrite Vector.to_list_rev.
  rewrite <-rev_app_distr.
  rewrite Vector.to_list_append.
  reflexivity.
Qed.

Lemma vec_const_cons {k : nat} {X : Type} (x : X)
  : Vector.const x (S k) = Vector.cons _ x k (Vector.const x k).
Proof.
  cbn.
  reflexivity.
Qed.

Lemma vec_take_const {k k'} {X : Type} (x : X) (Hleq : k' <= k)
  : Vector.take _ Hleq (Vector.const x k) = Vector.const x k'.
Proof.
  revert dependent k.
  dependent induction k';intros;cbn.
  - reflexivity.
  - dependent destruction k.
    + lia.
    + rewrite vec_const_cons.
      f_equal.
      specialize (IHk' _ x _ (le_S_n k' k Hleq)).
      assumption.
Qed.

Lemma vec_rev_nil {X : Type}
  : Vector.rev (Vector.nil X) = Vector.nil X.
Proof.
  eapply list_eq_vec_eq.
  rewrite Vector.to_list_rev.
  cbn.
  reflexivity.
Qed.

Lemma vec_rev_const {k} {X : Type} (x : X)
  : Vector.rev (Vector.const x k) = Vector.const x k.
Proof.
  eapply list_eq_vec_eq.
  rewrite Vector.to_list_rev.
  rewrite Vector.to_list_const.
  eapply rev_repeat.
Qed.

Lemma vec_take_map2 {k n} {X Y Z : Type} (H : k <= n) (f : X -> Y -> Z) (x y : Vector.t _ n)
  : Vector.take _ H (Vector.map2 f x y) = Vector.map2 f (Vector.take _ H x) (Vector.take _ H y).
Proof.
  revert dependent k.
  revert dependent y.
  dependent induction x;dependent destruction y;intros;cbn.
  - dependent destruction H. cbn.
    reflexivity.
  - dependent destruction k;cbn.
    + reflexivity.
    + rewrite IHx.
      reflexivity.
Qed.

Lemma vec_to_list_map2 {k} {X Y Z : Type} (f : X -> Y -> Z) (x y : Vector.t _ k)
  : Vector.to_list (Vector.map2 f x y) = map2 f (Vector.to_list x) (Vector.to_list y).
Proof.
  dependent induction x; dependent destruction y.
  - cbn.
    reflexivity.
  - rewrite Vector.to_list_cons.
    match goal with |- _ ?x = _ => cbn_this x end.
    setoid_rewrite Vector.to_list_cons.
    cbn.
    rewrite IHx.
    reflexivity.
Qed.

Lemma vec_rev_map2 {k} {X Y Z : Type} (f : X -> Y -> Z) (x y : Vector.t _ k)
  : Vector.rev (Vector.map2 f x y) = Vector.map2 f (Vector.rev x) (Vector.rev y).
Proof.
  eapply list_eq_vec_eq.
  rewrite Vector.to_list_rev.
  setoid_rewrite vec_to_list_map2.
  setoid_rewrite Vector.to_list_rev.
  rewrite rev_map2.
  - reflexivity.
  - setoid_rewrite Vector.length_to_list.
    reflexivity.
Qed.

Lemma vec_to_list_nth {k} {X : Type} (x : X) (a : Vector.t X k) (i : Fin.t k)
  : a [[i]] = nth (proj1_sig (Fin.to_nat i)) (Vector.to_list a) x.
Proof.
  dependent induction a.
  - inversion i.
  - dependent destruction i;[cbn;eauto|].
    match goal with |- _ = nth ?x ?y ?z => cbn_this x end.
    destruct (Fin.to_nat i) eqn:E.
    match goal with |- _ = nth ?x ?y ?z => cbn_this x end.
    rewrite Vector.to_list_cons.
    cbn.
    rewrite IHa.
    rewrite E.
    match goal with |- nth ?x ?y ?z = _ => cbn_this x end.
    reflexivity.
Qed.

Lemma vec_rev_nth {k} {X : Type} (a : Vector.t X k) (i j : Fin.t k)
  : k = S (proj1_sig (Fin.to_nat i) + proj1_sig (Fin.to_nat j)) -> (Vector.rev a) [[i]] = a [[j]].
Proof.
  intros.
  assert (x : X).
  {
    destruct a.
    - inversion i.
    - exact h.
  }
  setoid_rewrite vec_to_list_nth with (x:=x).
  rewrite Vector.to_list_rev.
  eapply rev_nth_eq.
  rewrite Vector.length_to_list.
  assumption.
Qed.

Lemma vec_map_app {k1 k2 : nat} {X Y : Type}
      (f : X -> Y) (xt1 : Vector.t _ k1) (xt2 : Vector.t _ k2)
  : Vector.map f (Vector.append xt2 xt1)
    = Vector.append (Vector.map f xt2) (Vector.map f xt1).
Proof.
  dependent induction xt2;cbn.
  - reflexivity.
  - f_equal.
    eapply IHxt2.
Qed.

(*Lemma vec_map2_app_gen {k1 k2 : nat} {X Y : Type -> Type} {X1 X2 Y1 Y2 Z : Type}
      (f : forall {V W}, X V -> Y W -> Z)
      (xt1 : Vector.t (X X1) k1) (yt1 : Vector.t (Y Y1) k1)
      (xt2 : Vector.t (X X2) k2) (yt2 : Vector.t (Y Y2) k2)
  : Vector.map2 f (Vector.append xt2 xt1) (Vector.append yt2 yt1)
    = Vector.append (Vector.map2 f xt2 yt2) (Vector.map2 f xt1 yt1).
Proof.
*)
Lemma vec_map2_app {k1 k2 : nat} {X Y Z : Type}
      (f : X -> Y -> Z) (xt1 yt1 : Vector.t _ k1) (xt2 yt2 : Vector.t _ k2)
  : Vector.map2 f (Vector.append xt2 xt1) (Vector.append yt2 yt1)
    = Vector.append (Vector.map2 f xt2 yt2) (Vector.map2 f xt1 yt1).
Proof.
  dependent induction xt2; dependent destruction yt2;cbn.
  - reflexivity.
  - f_equal.
    eapply IHxt2.
Qed.

Lemma vec_map_cons {X Y : Type} {k : nat} (f : X -> Y) x (xv : Vector.t X k)
  : Vector.map f (Vector.cons _ x _ xv) = Vector.cons _ (f x) _ (Vector.map f xv).
Proof.
  reflexivity.
Qed.

Lemma vec_take_cons {k n} {X : Type} (H : S k <= S n) (xt : Vector.t X n) x
  : Vector.take (S k) H (Vector.cons _ x n xt) = Vector.cons _ x k (Vector.take k (le_S_n _ _ H) xt).
Proof.
  cbn.
  reflexivity.
Qed.

Lemma vec_to_list_take {k n} {X : Type} (H : k <= n) (x : Vector.t X n)
  : Vector.to_list (Vector.take k H x) = firstn k (Vector.to_list x).
Proof.
  revert dependent k.
  dependent induction x;intros.
  - cbn.
    inversion H.
    subst k.
    rewrite Vector.take_O.
    cbn.
    reflexivity.
  - dependent destruction k.
    + cbn.
      reflexivity.
    + rewrite vec_take_cons.
      setoid_rewrite Vector.to_list_cons.
      setoid_rewrite firstn_cons.
      f_equal.
      eapply IHx.
Qed.

Lemma vec_map2_map2_assoc {X Y Z : Type} {k} (f : X -> Y -> Y) (g : Y -> Z -> Y)
      (Hassoc : forall x y z, f x (g y z) = g (f x y) z)
  : forall (xt yt zt : Vector.t _ k), Vector.map2 f xt (Vector.map2 g yt zt) = Vector.map2 g (Vector.map2 f xt yt) zt.
Proof.
  intro xt.
  dependent induction xt;intros;
    dependent destruction yt;
    dependent destruction zt;
    cbn.
  - reflexivity.
  - f_equal;eauto.
Qed.

Lemma vec_map2_const1 {X Y Z : Type} {k} (f : X -> Y -> Z)
  : forall (yt : Vector.t _ k) x, Vector.map2 f (Vector.const x k) yt = Vector.map (f x) yt.
Proof.
  intros yt.
  dependent induction yt;
    intros;cbn.
  - reflexivity.
  - f_equal;eauto.
Qed.

Lemma vec_map2_const2 {X Y Z : Type} {k} (f : X -> Y -> Z)
  : forall (xt : Vector.t _ k) y, Vector.map2 f xt (Vector.const y k) = Vector.map (fun x => f x y) xt.
Proof.
  intros xt.
  dependent induction xt;
    intros;cbn.
  - reflexivity.
  - f_equal;eauto.
Qed.

Lemma vec_forall2_nth {X Y : Type} (k : nat) (a : Vector.t X k) (b : Vector.t Y k) (P : X -> Y -> Prop)
  : Vector.Forall2 P a b -> forall i : Fin.t k, P (a [[i]]) (b [[i]]).
Proof.
  dependent induction a;
    dependent destruction b;
    dependent destruction i;
    dependent destruction H;
    cbn.
  - assumption.
  - eapply IHa.
    eauto.
Qed.

Lemma vec_Forall_forall {k} {A : Type} (a : Vector.t A k) P
  : Vector.Forall P a <-> (forall i, P (a[[i]])).
Proof.
  split;[eapply vector_forall_nth|].
  intros.
  dependent induction a.
  - econstructor.
  - econstructor.
    + specialize (H (@Fin.F1 _)).
      cbn in H.
      assumption.
    + eapply IHa.
      intros i.
      specialize (H (Fin.FS i)).
      cbn in H.
      assumption.
Qed.

Lemma vec_forall2_map_eq {k} {X Y : Type} (f : X -> Y) (xl1 xl2 : Vector.t _ k)
  : Vector.Forall2 (fun x y => f x = f y) xl1 xl2 -> Vector.map f xl1 = Vector.map f xl2.
Proof.
  intros.
  dependent induction H;eauto.
  setoid_rewrite vec_map_cons.
  f_equal;eauto.
Qed.

Lemma vec_forall2_impl {k} {X Y : Type} (P Q : X -> Y -> Prop) (xt yt : Vector.t _ k)
  : (forall x y, P x y -> Q x y) -> Vector.Forall2 P xt yt -> Vector.Forall2 Q xt yt.
Proof.
  intros.
  induction H0;econstructor;eauto.
Qed.

Lemma vec_forall3_impl {k} {X Y Z : Type} (P Q : X -> Y -> Z -> Prop) (xt yt zt : Vector.t _ k)
  : (forall x y z, P x y z -> forall x', Q x' y z) -> Vec_Forall3 P xt yt zt -> Vec_Forall3 Q xt yt zt.
Proof.
  intros.
  induction H0;econstructor;eauto.
Qed.

Lemma vec_forall3_forall2_1 {k : nat} {X Y Z : Type} (g : Y -> Z -> Prop) (xt yt zt : Vector.t _ k)
  : Vec_Forall3 (fun (_ : X) y z => g y z) xt yt zt -> Vector.Forall2 g yt zt.
Proof.
  intros.
  dependent induction H;econstructor;eauto.
Qed.

Lemma vec_nth_eq {k : nat} {X : Type} (x y : Vector.t X k)
  : x = y -> forall i, x [[i]] = y [[i]].
Proof.
  clear.
  intros.
  subst x.
  reflexivity.
Qed.

Lemma vec_nth_eq2 {X : Type} a
  : a = Vector.cons _ (a [[@Fin.F1 _]]) _ (Vector.cons _ (a [[Fin.FS (@Fin.F1 _)]]) _ (Vector.nil X)).
Proof using.
  clear.
  dependent destruction a;cbn.
  dependent destruction a;cbn.
  dependent destruction a;cbn.
  reflexivity.
Qed.