HyPre.util.VectorPair

From Coq Require Import
     Lia
     Lists.List.
From Coq Require Import Program.Equality.

From HyPre Require Import Tac.

From HyPre Require Export
     ListExtra
     MonoidHomomorphism
     VectorExtra.
(* TODO Prove all the vectorpair lemmas *)

Lemma k_leq_2k {k} : k <= k+k.
Proof.
  clear. lia.
Qed.

Definition fst_vec {k} {X : Type} : Vector.t X (k+k) -> Vector.t X k
  := fun xt => Vector.rev (Vector.take k k_leq_2k (Vector.rev xt)).

Definition snd_vec {k} {X : Type} : Vector.t X (k+k) -> Vector.t X k
  := Vector.take k k_leq_2k.

Definition nth_pair {k} {X : Type} (i : Fin.t k) : Vector.t X (k+k) -> X * X
  := fun xt => (Vector.nth (fst_vec xt) i, Vector.nth (snd_vec xt) i).

Lemma x_minus_lt_k {k} : forall x, x < k+k -> x - k < k.
Proof.
  clear. lia.
Qed.

Definition depair_i {k} (i : Fin.t (k+k)) : bool * Fin.t k
  := let i_sig := Fin.to_nat i in
     let i1 := proj1_sig i_sig in
     let i2 := proj2_sig i_sig in
     match Compare_dec.lt_dec i1 k with
     | left H => (false, Fin.of_nat_lt H)
     | right _ => (true, Fin.of_nat_lt (x_minus_lt_k i1 i2))
     end.

Definition is_fst {k} (i : Fin.t (k+k)) : bool
  := let (r,_) := depair_i i in r.

Definition vec_k_comm {k k' : nat} {X : Type} (x : Vector.t X (k+k')) : Vector.t X (k'+k).
Proof.
  rewrite PeanoNat.Nat.add_comm.
  exact x.
Defined.

Lemma to_kk_snd_vec {k} {X : Type} (x y : Vector.t X k)
  : snd_vec (Vector.append y x) = y.
Proof.
  unfold snd_vec.
  rewrite Vector.take_app.
  reflexivity.
Qed.

Lemma to_kk_fst_vec {k} {X : Type} (x y : Vector.t X k)
  : fst_vec (Vector.append y x) = x.
Proof.
  setoid_rewrite <-vec_rev_rev with (xv:=x).
  setoid_rewrite <-vec_rev_rev with (xv:=y).
  unfold fst_vec.
  eapply vec_rev_rev_eq.
  rewrite vec_append_rev.
  rewrite vec_rev_rev.
  rewrite vec_rev_rev.
  specialize (to_kk_snd_vec (X:=X) (k:=k)) as Q.
  unfold snd_vec in Q.
  rewrite vec_rev_rev.
  eapply Q.
Qed.

Lemma snd_vec_const {k} {X : Type} (x : X)
  : snd_vec (Vector.const x (k+k)) = Vector.const x k.
Proof.
  unfold snd_vec.
  eapply vec_take_const.
Qed.

Lemma fst_vec_const {k} {X : Type} (x : X)
  : fst_vec (Vector.const x (k+k)) = Vector.const x k.
Proof.
  unfold fst_vec.
  rewrite vec_rev_const.
  rewrite vec_take_const.
  rewrite vec_rev_const.
  reflexivity.
Qed.

Lemma snd_vec_map2 {k} {X Y Z : Type} (f : X -> Y -> Z) (x y : Vector.t _ (k+k))
  : snd_vec (Vector.map2 f x y) = Vector.map2 f (snd_vec x) (snd_vec y).
Proof.
  unfold snd_vec.
  eapply vec_take_map2.
Qed.

Lemma fst_vec_map2 {k} {X Y Z : Type} (f : X -> Y -> Z) (x y : Vector.t _ (k+k))
  : fst_vec (Vector.map2 f x y) = Vector.map2 f (fst_vec x) (fst_vec y).
Proof.
  unfold fst_vec.
  rewrite <-vec_rev_map2.
  rewrite vec_rev_map2.
  eapply vec_eq_rev_rev.
  eapply vec_take_map2.
Qed.

Lemma depair_i_nlt {k} (i : Fin.t (k+k)) j
  : (true, j) = depair_i i -> not (proj1_sig (Fin.to_nat i) < k).
Proof.
  intros.
  unfold depair_i in H.
  destruct (Compare_dec.lt_dec (proj1_sig (Fin.to_nat i)) k).
  - congruence.
  - assumption.
Qed.

Lemma depair_i_lt {k} (i : Fin.t (k+k)) j
  : (false, j) = depair_i i -> (proj1_sig (Fin.to_nat i) < k).
Proof.
  intros.
  unfold depair_i in H.
  destruct (Compare_dec.lt_dec (proj1_sig (Fin.to_nat i)) k).
  - assumption.
  - congruence.
Qed.

Lemma vec_take_nth {k n} {X : Type} (H : k <= n) (a : Vector.t X n) (i : Fin.t n) (j : Fin.t k)
  : proj1_sig (Fin.to_nat j) = proj1_sig (Fin.to_nat i) -> Vector.take k H a [[j]] = a [[i]].
Proof.
  revert j.
  revert dependent n.
  dependent induction k;intros.
  - inversion j.
  - dependent destruction a.
    + inversion H.
    + dependent destruction i; dependent destruction j.
      * cbn.
        reflexivity.
      * exfalso.
        cbn in H0. destruct (Fin.to_nat j).
        cbn in H0.
        congruence.
      * cbn in H0.
        destruct (Fin.to_nat i) eqn:E.
        cbn in H0.
        congruence.
      * cbn. cbn in H0.
        destruct (Fin.to_nat i) eqn:Ei.
        destruct (Fin.to_nat j) eqn:Ej.
        cbn in H0.
        eapply IHk.
        rewrite Ei,Ej.
        cbn.
        lia.
Qed.

Lemma snd_vec_nth {k} {X : Type} (a : Vector.t X (k+k)) i j
  : (false, j) = depair_i i -> snd_vec a [[j]] = a[[i]].
Proof.
  dependent destruction k;intros.
  - inversion j.
  - unfold depair_i in H.
    match goal with [H: _ = match ?x with _=>_ end |- _] => destruct x end.
    + inversion H.
      unfold snd_vec.
      eapply vec_take_nth.
      cbn.
      rewrite Fin.to_nat_of_nat.
      cbn.
      reflexivity.
    + congruence.
Qed.

Lemma fst_vec_nth {k} {X : Type} (a : Vector.t X (k+k)) i j
  : (true, j) = depair_i i -> fst_vec a [[j]] = a[[i]].
Proof.
  dependent destruction k;intros.
  - inversion j.
  - unfold depair_i in H.
    match goal with [H: _ = match ?x with _=>_ end |- _] => destruct x end.
    + congruence.
    + inversion H.
      unfold fst_vec.
      progress cbn in n.
      assert (S k <= proj1_sig (Fin.to_nat i)) as Q by (cbn;lia).
      progress cbn in Q.
      progress cbn in H.
      match goal with [Q: _ <= proj1_sig ?x |-_] => destruct x as [i' ?] eqn:E end.
      cbn in Q.
      match goal with [|- Vector.rev _ [[ ?x ]] = _] => cbn_this x end.
      clear H n.
      assert (S (k + k) - i' < S k + S k) as Hlt by lia.
      setoid_rewrite <-vec_rev_nth with (i:=Fin.of_nat_lt Hlt) (a:=a);cycle 1.
      * rewrite Fin.to_nat_of_nat.
        cbn.
        rewrite E.
        cbn.
        destruct i';lia.
      * assert (S k + k - i' < S k) as Hlt'.
        {
          destruct i'. lia.
          lia.
        }
        setoid_rewrite vec_rev_nth with (j:=Fin.of_nat_lt Hlt');cycle 1.
        -- setoid_rewrite Fin.to_nat_of_nat.
           cbn.
           destruct i';[inversion Q|].
           lia.
        -- setoid_rewrite vec_take_nth.
           reflexivity.
           setoid_rewrite Fin.to_nat_of_nat.
           cbn.
           reflexivity.
Qed.

Section with_kMH.
  Context {k : nat}.
  Context `{MH : MonoidHomomorphism}.

  Global Instance MapVecMonHom
    : MonoidHomomorphism (Vector.map hom (n:=k)).
  Proof.
    econstructor.
    - intros.
      cbn.
      rewrite vec_map_map2.
      rewrite <-vec_map2_fun_app.
      eapply vec_map2_ext.
      setoid_rewrite homomorph.
      reflexivity.
    - cbn.
      rewrite vec_map_const.
      rewrite homomorph_unit.
      reflexivity.
  Qed.
End with_kMH.

Section with_kM.
  Context {k : nat}.

  Definition vpl_to_kk (v : Vector.t (nat * nat) k)
    := Vector.append (Vector.map snd v) (Vector.map fst v).

  Global Instance to_kk_hom
    : MonoidHomomorphism vpl_to_kk.
  Proof.
    econstructor.
    - intros.
      unfold vpl_to_kk.
      unfold monoid_plus at 3. unfold MonVecMon.
      setoid_rewrite vec_map2_app.
      f_equal.
      + setoid_rewrite vec_map_map2.
        setoid_rewrite <-vec_map2_fun_app.
        eapply vec_map2_ext.
        intros.
        destruct x, y. cbn.
        reflexivity.
      + setoid_rewrite vec_map_map2.
        setoid_rewrite <-vec_map2_fun_app.
        eapply vec_map2_ext.
        intros.
        destruct x, y. cbn.
        reflexivity.
    - cbn.
      setoid_rewrite vec_map_const.
      cbn.
      eapply vec_append_const.
  Qed.
End with_kM.
Arguments MapVecMonHom _ {_ _ _ _} _ {_}.

Section with_kXY.
  Context {X Y : Type}.
  Context {k : nat}.

  Definition pair_len (xy : list X * list Y) := let (x,y) := xy in (length x, length y).

  Global Instance pair_len_hom
    : MonoidHomomorphism pair_len.
  Proof.
    econstructor.
    - intros.
      destruct m1 as [m11 m12]. destruct m2 as [m21 m22].
      cbn.
      setoid_rewrite app_length.
      reflexivity.
    - cbn.
      reflexivity.
  Qed.

  Definition vpl_len (v : Vector.t (list X * list Y) k)
    := Vector.map pair_len v.

  Global Instance vpl_len_hom
    : MonoidHomomorphism vpl_len.
  Proof.
    econstructor.
    - intros.
      unfold vpl_len.
      specialize (MapVecMonHom k pair_len) as Q.
      eapply Q.
    - cbn.
      rewrite vec_map_const.
      cbn.
      reflexivity.
  Qed.

  Definition vpl_len_kk (v : Vector.t (list X * list Y) k)
    := vpl_to_kk (vpl_len v).

  Global Instance vpl_len_kk_hom
    : @MonoidHomomorphism _ _ (MonVecMon _) (MonVecMon _) vpl_len_kk.
  Proof.
    econstructor.
    - intros.
      unfold vpl_len_kk.
      setoid_rewrite homomorph.
      generalize (vpl_len m1) as v1.
      generalize (vpl_len m2) as v2.
      intros.
      eapply to_kk_hom.
    - cbn.
      setoid_rewrite Vector.map_map.
      setoid_rewrite vec_map_const.
      rewrite vec_append_const.
      cbn.
      reflexivity.
  Qed.
End with_kXY.

From HyPre Require Export VectorList.

Lemma vpl_len_kk_snd_vec {k} {X Y : Type} (a : Vector.t (list X * list Y) k)
  : snd_vec (vpl_len_kk a) = vl_len (Vector.map snd a).
Proof.
  unfold snd_vec, vpl_len_kk, vl_len, vpl_to_kk, vpl_len.
  setoid_rewrite Vector.take_app.
  dependent induction a.
  - cbn.
    reflexivity.
  - cbn.
    f_equal.
    + unfold pair_len.
      destruct h;cbn.
      reflexivity.
    + eapply IHa.
Qed.

Lemma vpl_len_kk_fst_vec {k} {X Y : Type} (x : Vector.t (list X * list Y) k)
  : fst_vec (vpl_len_kk x) = vl_len (Vector.map fst x).
Proof.
  unfold fst_vec, vpl_len_kk, vl_len, vpl_to_kk, vpl_len.
  rewrite <-vec_append_rev.
  rewrite Vector.take_app.
  rewrite vec_rev_rev.
  dependent induction x;cbn.
  - reflexivity.
  - f_equal.
    + unfold pair_len.
      destruct h;cbn.
      reflexivity.
    + eapply IHx.
Qed.

Import VectorListNotations.

(*Lemma vec_map2_map2 {k} {X Y Z W : Type} (f : X -> Y -> Z) (g : Z -> Z -> W) x1 x2 y1 y2
  : Vector.map2 g (Vector.map2 f x1 y1) (Vector.map2 f x2 y2) = Vector.map2 (fun x y => g (f x y)) x y.*)

Lemma vec_pair_fg {k} {T : Type -> Type} {X Y : Type}
      (x1 x2 : Vector.t (T X) k) (y1 y2 : Vector.t (T Y) k)
      (f : T X * T Y -> T X * T Y -> T X * T Y) (g : forall Z, T Z -> T Z -> T Z)
  : (forall a1 a2 b1 b2, f (a1,b1) (a2,b2) = (g X a1 a2, g Y b1 b2))
    -> Vector.map2 f (Vector.map2 pair x1 y1) (Vector.map2 pair x2 y2)
    = Vector.map2 pair (Vector.map2 (g X) x1 x2) (Vector.map2 (g Y) y1 y2).
Proof.
  intros H.
  dependent induction x1;
    dependent destruction x2;
    dependent destruction y1;
    dependent destruction y2;
    cbn.
  - reflexivity.
  - f_equal.
    + eapply H.
    + eapply IHx1;eauto.
Qed.

Lemma t_combine_monoid_plus {k} {X Y : Type} (x1 x2 : Vector.t (list X) k) (y1 y2 : Vector.t (list Y) k)
  : monoid_plus (t_combine x1 y1) (t_combine x2 y2) = t_combine (x1 +vl+ x2) (y1 +vl+ y2).
Proof.
  eapply vec_pair_fg.
  clear.
  intros.
  cbn.
  reflexivity.
Qed.

Lemma vec_map2_fst {k} {X Y : Type} (xt : Vector.t X k) (yt : Vector.t Y k)
  : Vector.map2 (fun x _ => x) xt yt = xt.
Proof.
  dependent induction xt;dependent destruction yt;cbn.
  - reflexivity.
  - f_equal.
    eapply IHxt.
Qed.

Lemma vec_map2_snd {k} {X Y : Type} (xt : Vector.t X k) (yt : Vector.t Y k)
  : Vector.map2 (fun _ y => y) xt yt = yt.
Proof.
  dependent induction xt;dependent destruction yt;cbn.
  - reflexivity.
  - f_equal.
    eapply IHxt.
Qed.

Lemma vpl_to_kk_t_combine {k} (a b : Vector.t nat k)
  : vpl_to_kk (t_combine a b) = Vector.append b a.
Proof.
  unfold vpl_to_kk, t_combine.
  setoid_rewrite vec_map_map2.
  cbn.
  rewrite vec_map2_fst.
  rewrite vec_map2_snd.
  reflexivity.
Qed.

Lemma vpl_len_t_combine {k} {X Y : Type} (x : Vector.t (list X) k) (y : Vector.t (list Y) k)
  : vpl_len (t_combine x y) = t_combine (vl_len x) (vl_len y).
Proof.
  unfold vpl_len,t_combine.
  rewrite vec_map_map2.
  unfold vl_len.
  rewrite <-vec_map2_fun_app.
  unfold pair_len.
  reflexivity.
Qed.

Lemma to_kk_self {k} {X : Type} (x : Vector.t X (k+k))
  : Vector.append (snd_vec x) (fst_vec x) = x.
Proof.
  unfold snd_vec, fst_vec.
  eapply list_eq_vec_eq.
  setoid_rewrite Vector.to_list_append.
  setoid_rewrite Vector.to_list_rev.
  setoid_rewrite vec_to_list_take.
  setoid_rewrite Vector.to_list_rev.
  setoid_rewrite firstn_rev.
  rewrite rev_involutive.
  rewrite Vector.length_to_list.
  replace (k + k - k) with k by lia.
  eapply firstn_skipn.
Qed.

Lemma vpl_len_kk_eq_inv {k} {X Y : Type} (a b : Vector.t (list X * list Y) k)
  : vpl_len_kk a = vpl_len_kk b
    -> vl_len (Vector.map fst a) = vl_len (Vector.map fst b) /\ vl_len (Vector.map snd a) = vl_len (Vector.map snd b).
Proof.
  intros.
  setoid_rewrite <-vpl_len_kk_fst_vec.
  setoid_rewrite <-vpl_len_kk_snd_vec.
  split;f_equal;assumption.
Qed.

Import MonoidHomomorphismNotations.

Lemma vec_map2_map2_inj {k} {X Y Z : Type} (f : X -> Y -> Z) (xt1 xt2 yt1 yt2 : Vector.t _ k)
      (Hinj : forall x1 x2 y1 y2, f x1 y1 = f x2 y2 -> x1 = x2 /\ y1 = y2)
      (Hmap : Vector.map2 f xt1 yt1 = Vector.map2 f xt2 yt2)
  : xt1 = xt2 /\ yt1 = yt2.
Abort.

Lemma vpl_len_kk_plus_eq1 {k} {X Y : Type} (a1 a2 b1 b2 : Vector.t (list X * list Y) k)
  : a2 +m+ a1 = b2 +m+ b1 -> vpl_len_kk a1 = vpl_len_kk b1 -> a1 = b1 /\ a2 = b2.
Proof.
  intros.
  cbn in H.
  eapply vpl_len_kk_eq_inv in H0.
  unfold vl_len in H0.
  setoid_rewrite Vector.map_map in H0.
  destruct H0 as [Q1 Q2].
  revert a2 b1 b2 H Q1 Q2.
  dependent induction a1;
    dependent destruction a2;
    dependent destruction b1;
    dependent destruction b2;
    cbn;intros.
  - split;reflexivity.
  - destruct h0,h1,h2,h.
    dependent destruction H.
    cbn in Q1,Q2.
    dependent destruction Q1;dependent destruction Q2.
    eapply length_app_eq in x1;eauto.
    eapply length_app_eq in x2;eauto.
    specialize (IHa1 a2 b1 b2).
    exploit IHa1.
    split;f_equal;firstorder.
    all:f_equal;firstorder.
Qed.

Lemma vec_map2_map_1 {k} {X X' Y Z : Type} (f : X' -> Y -> Z) (g : X -> X') (xt yt : Vector.t _ k)
  : Vector.map2 (fun x y => f (g x) y) xt yt = Vector.map2 (fun x y => f x y) (Vector.map g xt) yt.
Proof.
  dependent induction xt; dependent destruction yt;cbn.
  - reflexivity.
  - f_equal.
    eapply IHxt.
Qed.

Lemma vec_map2_map_2 {k} {X Y Y' Z : Type} (f : X -> Y' -> Z) (g : Y -> Y') (xt yt : Vector.t _ k)
  : Vector.map2 (fun x y => f x (g y)) xt yt = Vector.map2 (fun x y => f x y) xt (Vector.map g yt).
Proof.
  dependent induction xt; dependent destruction yt;cbn.
  - reflexivity.
  - f_equal.
    eapply IHxt.
Qed.

Lemma vl_len_le_v1 {k} {X : Type} (a : Vector.t (list X) k) v1 v2
  (Hvl : vl_len a = v1 +m+ v2)
  : Vector.Forall2 (fun x y => x <= length y) v1 a.
Proof.
  revert v1 v2 Hvl.
  dependent induction a;
    dependent destruction v1;
    dependent destruction v2;
    cbn;intros.
  - econstructor.
  - dependent destruction Hvl.
    econstructor.
    + lia.
    + eauto.
Qed.

Lemma vl_len_le_v2 {k} {X : Type} (a : Vector.t (list X) k) v1 v2
  (Hvl : vl_len a = v1 +m+ v2)
  : Vector.Forall2 (fun x y => x <= length y) v2 a.
Proof.
  revert v1 v2 Hvl.
  dependent induction a;
    dependent destruction v1;
    dependent destruction v2;
    cbn;intros.
  - econstructor.
  - dependent destruction Hvl.
    econstructor.
    + lia.
    + eauto.
Qed.

Global Instance fst_vec_MonHom (k : nat)
  : MonoidHomomorphism (fst_vec (k:=k)).
Proof.
  econstructor.
  - intros.
    unfold fst_vec.
    setoid_rewrite vec_rev_map2.
    setoid_rewrite vec_take_map2.
    setoid_rewrite vec_rev_map2.
    reflexivity.
  - unfold fst_vec.
    cbn.
    setoid_rewrite vec_rev_const.
    setoid_rewrite vec_take_const.
    eapply vec_rev_const.
Qed.

Global Instance snd_vec_MonHom (k : nat)
  : MonoidHomomorphism (snd_vec (k:=k)).
Proof.
  econstructor.
  - intros.
    unfold snd_vec.
    cbn.
    setoid_rewrite vec_take_map2.
    reflexivity.
  - unfold snd_vec.
    cbn.
    setoid_rewrite vec_take_const.
    reflexivity.
Qed.

Lemma vpl_len_kk_le_v1_fst {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
      (Hvpl : vpl_len_kk a = v1 +m+ v2)
  : Vector.Forall2 (fun x y => x <= length y) (fst_vec v1) (Vector.map fst a).
Proof.
  eapply f_equal with (f:=fst_vec) in Hvpl.
  rewrite vpl_len_kk_fst_vec in Hvpl.
  unfold vpl_len_kk, vpl_to_kk in Hvpl.
  rewrite homomorph in Hvpl.
  eapply vl_len_le_v1.
  eassumption.
Qed.

Lemma vpl_len_kk_le_v1_snd {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
      (Hvpl : vpl_len_kk a = v1 +m+ v2)
  : Vector.Forall2 (fun x y => x <= length y) (snd_vec v1) (Vector.map snd a).
Proof.
  eapply f_equal with (f:=snd_vec) in Hvpl.
  rewrite vpl_len_kk_snd_vec in Hvpl.
  unfold vpl_len_kk, vpl_to_kk in Hvpl.
  rewrite homomorph in Hvpl.
  eapply vl_len_le_v1.
  eassumption.
Qed.

Lemma vpl_len_kk_le_v2_fst {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
      (Hvpl : vpl_len_kk a = v1 +m+ v2)
  : Vector.Forall2 (fun x y => x <= length y) (fst_vec v2) (Vector.map fst a).
Proof.
  eapply f_equal with (f:=fst_vec) in Hvpl.
  rewrite vpl_len_kk_fst_vec in Hvpl.
  unfold vpl_len_kk, vpl_to_kk in Hvpl.
  rewrite homomorph in Hvpl.
  eapply vl_len_le_v2.
  eassumption.
Qed.

Lemma vpl_len_kk_le_v2_snd {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
      (Hvpl : vpl_len_kk a = v1 +m+ v2)
  : Vector.Forall2 (fun x y => x <= length y) (snd_vec v2) (Vector.map snd a).
Proof.
  eapply f_equal with (f:=snd_vec) in Hvpl.
  rewrite vpl_len_kk_snd_vec in Hvpl.
  unfold vpl_len_kk, vpl_to_kk in Hvpl.
  rewrite homomorph in Hvpl.
  eapply vl_len_le_v2.
  eassumption.
Qed.

Lemma len_nat_min_eq {k} {X : Type} (a : Vector.t X k) v f
  (Hfa : Vector.Forall2 (fun x y => x <= f y) v a)
  : Vector.map2 (fun x y => Nat.min x (f y)) v a = v.
Proof.
  dependent induction Hfa;cbn.
  - reflexivity.
  - f_equal.
    + lia.
    + eauto.
Qed.

Lemma vpl_len_kk_surj_v1 {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
  : vpl_len_kk a = v1 +m+ v2
    -> let a1 := Vector.map2 (fun (ij : nat * nat) x => let (i,j) := ij in
                                                (firstn i (fst x), firstn j (snd x))
                            )
                            (Vector.map2 pair (fst_vec v1) (snd_vec v1))
                            a in
      vpl_len_kk a1 = v1.
Proof.
  intros.
  subst a1.
  unfold vpl_len_kk,vpl_len,vpl_to_kk.
  unfold pair_len.
  setoid_rewrite vec_map_map2.
  setoid_rewrite vec_map_map2.
  match goal with |- Vector.append (Vector.map2 ?x _ _) _ = _
                  => rewrite vec_map2_ext with (g:=fun i y => length (firstn (snd i) (snd y))) end.
  match goal with |- Vector.append (Vector.map2 ?x _ _) _ = _
                  => setoid_rewrite vec_map2_ext with (g:=fun i y => length (firstn (fst i) (fst y))) at 2 end.
  2,3:intros;destruct x;cbn;reflexivity.
  set (v:=Vector.map2 pair (fst_vec v1) (snd_vec v1)).
  set (f:=fun (A:Type) i (y : list A) => length (firstn i y)).
  assert ((fun (i : nat * nat) (y : list X * list Y) => length (firstn (snd i) (snd y)))
          = (fun i y => f Y (snd i) (snd y))) as Fy by reflexivity.
  assert ((fun (i : nat * nat) (y : list X * list Y) => length (firstn (fst i) (fst y)))
          = (fun i y => f X (fst i) (fst y))) as Fx by reflexivity.
  rewrite Fy,Fx.
  rewrite vec_map2_map_1 with (f:=fun x y => f Y x (snd y)) (g:=snd).
  rewrite vec_map2_map_1 with (f:=fun x y => f X x (fst y)) (g:=fst).
  rewrite vec_map2_map_2 with (f:=fun x y => f Y x y) (g:=snd).
  rewrite vec_map2_map_2 with (f:=fun x y => f X x y) (g:=fst).
  subst v.
  setoid_rewrite vec_map_map2.
  cbn.
  rewrite vec_map2_fst.
  rewrite vec_map2_snd.
  setoid_rewrite vec_map2_ext with (g:=fun x y => Nat.min x (length y)).
  2,3: intros; eapply firstn_length.
  setoid_rewrite len_nat_min_eq.
  - eapply to_kk_self.
  - eapply vpl_len_kk_le_v1_snd;eauto.
  - eapply vpl_len_kk_le_v1_fst;eauto.
Qed.

Lemma vpl_len_kk_surj_v2 {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
  : vpl_len_kk a = v1 +m+ v2
    -> let a2 := Vector.map2 (fun (ij : nat * nat) x => let (i,j) := ij in
                                                (skipn i (fst x), skipn j (snd x))
                            )
                            (Vector.map2 pair (fst_vec v1) (snd_vec v1))
                            a in
      vpl_len_kk a2 = v2.
Proof.
  intros.
  subst a2.
  unfold vpl_len_kk,vpl_len,vpl_to_kk.
  unfold pair_len.
  setoid_rewrite vec_map_map2.
  setoid_rewrite vec_map_map2.
  match goal with |- Vector.append (Vector.map2 ?x _ _) _ = _
                  => rewrite vec_map2_ext with (g:=fun i y => length (skipn (snd i) (snd y))) end.
  match goal with |- Vector.append (Vector.map2 ?x _ _) _ = _
                  => setoid_rewrite vec_map2_ext with (g:=fun i y => length (skipn (fst i) (fst y))) at 2 end.
  2,3:intros;destruct x;cbn;reflexivity.
  set (v:=Vector.map2 pair (fst_vec v1) (snd_vec v1)).
  setoid_rewrite vec_map2_ext with (f:=fun i y => length (skipn (snd i) (snd y))) (g:=fun i y => length (snd y) - snd i).
  setoid_rewrite vec_map2_ext with (g:=fun i y => length (fst y) - fst i) at 2.
  2,3: intros; now eapply skipn_length.
  set (f:=fun (A : Type) i (y : list A) => length y - i).
  assert ((fun (i : nat * nat) (y : list X * list Y) => length (snd y) - snd i)
          = (fun i y => f Y (snd i) (snd y))) as Fy by reflexivity.
  assert ((fun (i : nat * nat) (y : list X * list Y) => length (fst y) - fst i)
          = (fun i y => f X (fst i) (fst y))) as Fx by reflexivity.
  rewrite Fy,Fx.
  rewrite vec_map2_map_1 with (f:=fun x y => f Y x (snd y)) (g:=snd).
  rewrite vec_map2_map_1 with (f:=fun x y => f X x (fst y)) (g:=fst).
  rewrite vec_map2_map_2 with (f:=fun x y => f Y x y) (g:=snd).
  rewrite vec_map2_map_2 with (f:=fun x y => f X x y) (g:=fst).
  subst f.
  setoid_rewrite vec_map2_map_2 with (f:=fun x y => y - x) (g:=@length _).
  setoid_rewrite <-vec_map2_app.
  enough (Vector.map2 (fun x y => y - x) v1 (vpl_len_kk a) = v2).
  {
    rewrite <-H0.
    f_equal.
    - subst v.
      setoid_rewrite vec_map_map2.
      cbn.
      rewrite vec_map2_fst.
      rewrite vec_map2_snd.
      eapply to_kk_self.
    - unfold vpl_len_kk, vpl_to_kk, vpl_len.
      setoid_rewrite Vector.map_map.
      unfold pair_len.
      f_equal.
      + eapply Vector.map_ext.
        intros.
        destruct a0;cbn.
        reflexivity.
      + eapply Vector.map_ext.
        intros.
        destruct a0;cbn.
        reflexivity.
  }
  rewrite H.
  clear.
  eapply list_eq_vec_eq.
  rewrite vec_to_list_map2.
  setoid_rewrite vec_to_list_map2.
  specialize (Vector.length_to_list _ _ v1) as Q1.
  specialize (Vector.length_to_list _ _ v2) as Q2.
  rewrite <-Q2 in Q1.
  clear Q2.
  revert Q1.
  generalize (Vector.to_list v1).
  generalize (Vector.to_list v2).
  intro l.
  induction l;intros;cbn.
  - destruct l;cbn in Q1;[|congruence].
    cbn.
    reflexivity.
  - destruct l0;cbn in Q1;[congruence|].
    cbn.
    f_equal.
    + lia.
    + eapply IHl.
      lia.
Qed.

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

Lemma vec_map4_eq13_eq24_map2 {A B E : Type}
      (f : A -> B -> A -> B -> E) {n : nat}
      (a : Vector.t A n) (b : Vector.t B n)
  : map4 f a b a b = Vector.map2 (fun a' b' => f a' b' a' b') a b.
Proof.
  dependent induction a;
    dependent destruction b;
    cbn.
  - reflexivity.
  - f_equal.
    eapply IHa.
Qed.

Lemma vpl_len_kk_surj_aeq {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
  : vpl_len_kk a = v1 +m+ v2
    -> let a1 := Vector.map2 (fun (ij : nat * nat) x => let (i,j) := ij in
                                                (firstn i (fst x), firstn j (snd x))
                            )
                            (Vector.map2 pair (fst_vec v1) (snd_vec v1))
                            a in
      let a2 := Vector.map2 (fun (ij : nat * nat) x => let (i,j) := ij in
                                                (skipn i (fst x), skipn j (snd x))
                            )
                            (Vector.map2 pair (fst_vec v1) (snd_vec v1))
                            a in
      a = a1 +m+ a2.
Proof.
  intros.
  subst a1 a2.
  setoid_rewrite vec_map2_map2_map4.
  rewrite vec_map4_eq13_eq24_map2.
  setoid_rewrite vec_map2_ext with (g:=fun _ x => x).
  - rewrite vec_map2_snd.
    reflexivity.
  - clear.
    intros.
    destruct x as [i j].
    cbn.
    setoid_rewrite firstn_skipn.
    symmetry.
    eapply surjective_pairing.
Qed.

Lemma vpl_len_kk_surj_eq' {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
  : vpl_len_kk a = v1 +m+ v2
    -> let a1 := Vector.map2 (fun (ij : nat * nat) x => let (i,j) := ij in
                                                (firstn i (fst x), firstn j (snd x))
                            )
                            (Vector.map2 pair (fst_vec v1) (snd_vec v1))
                            a in
      let a2 := Vector.map2 (fun (ij : nat * nat) x => let (i,j) := ij in
                                                (skipn i (fst x), skipn j (snd x))
                            )
                            (Vector.map2 pair (fst_vec v1) (snd_vec v1))
                            a in
      vpl_len_kk a1 = v1 /\ vpl_len_kk a2 = v2 /\ a = a1 +m+ a2.
Proof.
  intros.
  split_conj.
  - eapply vpl_len_kk_surj_v1;eauto.
  - eapply vpl_len_kk_surj_v2;eauto.
  - eapply vpl_len_kk_surj_aeq;eauto.
Qed.

Lemma vpl_len_kk_surj_eq {k} {X Y : Type} (a : Vector.t (list X * list Y) k) v1 v2
  : vpl_len_kk a = v1 +m+ v2 -> exists a1 a2, vpl_len_kk a1 = v1 /\ vpl_len_kk a2 = v2 /\ a = a1 +m+ a2.
Proof.
  intros.
  eexists;eexists.
  eapply vpl_len_kk_surj_eq'.
  assumption.
Qed.

Lemma vec_app_unit1 {k n} (a : Vector.t _ k) (b : Vector.t _ n)
  : Vector.append a b = monoid_unit -> a = monoid_unit.
Proof.
  revert b.
  dependent induction a;
    intros;
    cbn.
  - split;reflexivity.
  - cbn in H.
    dependent destruction H.
    f_equal.
    eapply IHa;eauto.
Qed.

Lemma vec_app_unit2 {k n} (a : Vector.t _ k) (b : Vector.t _ n)
  : Vector.append a b = monoid_unit -> b = monoid_unit.
Proof.
  revert b.
  dependent induction a;cbn;intros.
  - assumption.
  - eapply IHa.
    dependent destruction H.
    assumption.
Qed.

Lemma vpl_len_zero_zero {k} {X Y : Type} (a : Vector.t (list X * list Y) k)
  : vpl_len a = monoid_unit -> a = monoid_unit.
Proof.
  dependent induction a;intros;cbn.
  - reflexivity.
  - dependent destruction H.
    f_equal.
    + unfold pair_len in x.
      destruct h.
      inversion x.
      rewrite H0 in H1.
      f_equal; eapply length_zero_iff_nil;eauto.
    + eapply IHa;eauto.
Qed.

Lemma vec_map_unit_nat {k} (a : Vector.t (nat * nat) k)
  : Vector.map fst a = monoid_unit -> Vector.map snd a = monoid_unit -> a = monoid_unit.
Proof.
  intros.
  setoid_rewrite t_combine_self at 1.
  setoid_rewrite H.
  setoid_rewrite H0.
  unfold t_combine.
  clear.
  induction k;cbn.
  - reflexivity.
  - f_equal.
    eapply IHk.
Qed.

Lemma vpl_len_kk_zero_zero {k} {X Y : Type} (a : Vector.t (list X * list Y) k)
  : vpl_len_kk a = monoid_unit -> a = monoid_unit.
Proof.
  intros.
  unfold vpl_len_kk,vpl_to_kk in H.
  eapply vec_app_unit1 in H as Q1.
  eapply vec_app_unit2 in H as Q2.
  eapply vec_map_unit_nat in Q2;eauto.
  eapply vpl_len_zero_zero;eauto.
Qed.

Definition vec_unzip {k} {X Y : Type} (vp : Vector.t (X * Y) k) : Vector.t X k * Vector.t Y k.
Proof.
  dependent induction vp.
  - econstructor;econstructor.
  - destruct IHvp as [IHx IHy].
    destruct h as [x y].
    econstructor;econstructor.
    all:eauto.
Defined.

Definition vec_zip {k} {X Y : Type} (x : Vector.t X k) (y : Vector.t Y k) : Vector.t (X * Y) k.
Proof.
  dependent induction x;
    dependent destruction y.
  - econstructor.
  - econstructor.
    + econstructor;eauto.
    + eapply IHx;eauto.
Defined.

Lemma vec_unzip_cons {k} {X Y : Type} (vp : Vector.t (X * Y) k) x y
  : vec_unzip (Vector.cons _ (x,y) _ vp)
    = (Vector.cons _ x _ (fst (vec_unzip vp)) , Vector.cons _ y _ (snd (vec_unzip vp))).
Proof.
  revert x y.
  dependent induction vp;intros.
  - cbn.
    reflexivity.
  - destruct h.
    specialize (IHvp x0 y0).
    setoid_rewrite IHvp.
    match goal with |- _ = ?x => cbn_this x end.
    cbn.
    match goal with [|- (match match ?x with _=>_ end with _=>_ end) = _]
                    => rewrite surjective_pairing with (p:=x) end.
    f_equal.
Qed.

Lemma vec_zip_cons {k} {X Y : Type} (xt : Vector.t X k) (yt : Vector.t Y k) x y
  : vec_zip (Vector.cons _ x _ xt) (Vector.cons _ y _ yt) = Vector.cons _ (x,y) _ (vec_zip xt yt).
Proof.
  dependent induction xt;
    dependent destruction yt.
  - cbn.
    reflexivity.
  - cbn.
    f_equal.
Qed.

Lemma vec_zip_unzip {k} {X Y : Type} (vp : Vector.t (X * Y) k)
  : let (x,y) := vec_unzip vp in vec_zip x y = vp.
Proof.
  rewrite surjective_pairing with (p:=vec_unzip vp).
  dependent induction vp.
  - cbn.
    reflexivity.
  - destruct h.
    rewrite vec_unzip_cons.
    unfold fst at 1.
    unfold snd at 1.
    rewrite vec_zip_cons.
    f_equal.
    eapply IHvp.
Qed.

Lemma vec_unzip_eq_map {k} {X Y : Type} (xyt : Vector.t _ k)
  : vec_unzip xyt
    = (Vector.map fst xyt, Vector.map (@snd X Y) xyt).
Proof.
  dependent induction xyt.
  - econstructor.
  - destruct h.
    setoid_rewrite vec_unzip_cons.
    setoid_rewrite IHxyt.
    unfold fst at 1.
    unfold snd at 1.
    cbn.
    reflexivity.
Qed.

Lemma vec_unzip_map2 {k} {X Y Z1 Z2 : Type} (f : X -> Y -> Z1 * Z2) (xt yt : Vector.t _ k)
  : vec_unzip (Vector.map2 f xt yt)
    = (Vector.map2 (fun x y => fst (f x y)) xt yt, Vector.map2 (fun x y => snd (f x y)) xt yt).
Proof.
  setoid_rewrite <-vec_map_map2.
  setoid_rewrite vec_unzip_eq_map.
  reflexivity.
Qed.

Lemma vec_unzip_fst {k} {X Y : Type} (xt : Vector.t (X * Y) k)
  : fst (vec_unzip xt) = Vector.map fst xt.
Proof.
  rewrite vec_unzip_eq_map.
  unfold fst at 1.
  reflexivity.
Qed.

Lemma vec_unzip_snd {k} {X Y : Type} (xt : Vector.t (X * Y) k)
  : snd (vec_unzip xt) = Vector.map snd xt.
Proof.
  rewrite vec_unzip_eq_map.
  unfold snd at 1.
  reflexivity.
Qed.