From Tealeaves Require Export
  Classes.Categorical.Applicative
  Classes.Kleisli.TraversableFunctor
  Classes.Kleisli.Theory.TraversableFunctor (* mapReduce *)
  Functors.List.

From Coq Require Import
  Logic.ProofIrrelevance.

#[local] Generalizable Variables ϕ T G A B C D M F n m p v.
Import Monoid.Notations.
Import Applicative.Notations.

Definition Vector (n: nat) (A: Type) : Type :=
  {l : list A | length l = n}.

Definition coerce_Vector_length:
  ∀ {A: Type} `(Heq: n = m),
    Vector n A → Vector m A.
Proof.
  introv heq [v pf].
  ∃ v. now subst.
Defined.

#[global] Notation "'coerce' Hlen 'in' V" :=
  (coerce_Vector_length Hlen V)
    (at level 10, V at level 10).

#[global] Notation "'precoerce' Hlen 'in' F" :=
  (F ○ coerce_Vector_length Hlen)
    (at level 10, F at level 20).

Lemma coerce_Vector_contents:
  ∀ {A: Type} `(Heq: n = m) (v: Vector n A),
    proj1_sig v = proj1_sig (coerce_Vector_length Heq v).
Proof.
  intros ? n m Heq [v pf].
  reflexivity.
Qed.

Lemma coerce_Vector_eq_refl:
  ∀ {A: Type} {n} (v: Vector n A),
    coerce eq_refl in v = v.
Proof.
  intros.
  destruct v.
  destruct e.
  reflexivity.
Qed.

Lemma coerce_Vector_eq_refl_pf:
  ∀ {A: Type} {n},
    coerce_Vector_length eq_refl = @id (Vector n A).
Proof.
  intros. ext v.
  apply coerce_Vector_eq_refl.
Qed.

Lemma coerce_Vector_compose
        {n m p: nat} `{v: Vector n A}
        (Heq1: n = m)
        (Heq2: m = p):
  coerce_Vector_length Heq2 (coerce_Vector_length Heq1 v) =
    coerce_Vector_length (eq_trans Heq1 Heq2) v.
Proof.
  destruct Heq1.
  destruct Heq2.
  destruct v as [vlist vlen].
  destruct vlen.
  reflexivity.
Qed.

Lemma coerce_Vector_eq_sym:
  ∀ {A: Type} {n m} (v: Vector n A)
    (Heq: n = m),
    v = coerce (eq_sym Heq) in coerce Heq in v.
Proof.
  intros.
  rewrite coerce_Vector_compose.
  rewrite eq_trans_sym_inv_r.
  rewrite coerce_Vector_eq_refl.
  reflexivity.
Qed.

From Coq Require Import RelationClasses.

Definition Vector_sim {n m A}:
  Vector n A → Vector m A → Prop :=
  fun v1 v2 ⇒ proj1_sig v1 = proj1_sig v2.

#[local] Infix "~~" := (Vector_sim) (at level 30).

(* Without <<n = m>>, functions with <<n <> m>> are related which is
awkward and blocks transitivity. >> *)
Definition Vector_fun_sim {n m A B}:
  (Vector n A → B) → (Vector m A → B) → Prop :=
  fun f1 f2 ⇒ n = m ∧ ∀ v1 v2, v1 ~~ v2 →
                     f1 v1 = f2 v2.

#[local] Infix "~!~" := (Vector_fun_sim) (at level 30).

Definition Vector_fun_indep {n A B} (f: Vector n A → B)
  : Prop := f ~!~ f.

Lemma Vector_fun_sim_eq
        {n m A B} {v1: Vector n A} {v2: Vector m A}
        {f: Vector n A → B} {g: Vector m A → B}:
  f ~!~ g →
  v1 ~~ v2 →
  f v1 = g v2.
Proof.
  introv Hfsim Hsim.
  destruct Hfsim as [Heq Hfsim].
  auto.
Qed.

Lemma Vector_fun_indep_eq
        {n A B} {v1: Vector n A} {v2: Vector n A}
        {f: Vector n A → B} (Hind: f ~!~f):
  v1 ~~ v2 →
  f v1 = f v2.
Proof.
  now apply Vector_fun_sim_eq.
Qed.

Lemma Vector_sim_length:
  ∀ {A: Type} {n m: nat}
    (v1: Vector n A)
    (v2: Vector m A),
    v1 ~~ v2 → n = m.
Proof.
  intros.
  destruct v1.
  destruct v2.
  unfold Vector_sim in H.
  cbn in H.
  subst.
  reflexivity.
Qed.

Lemma Vector_fun_sim_length:
  ∀ {A B: Type} {n m: nat}
    {f: Vector n A → B}
    {g: Vector m A → B},
    f ~!~ g → n = m.
Proof.
  intros.
  unfold Vector_fun_sim in H.
  tauto.
Qed.

Lemma Vector_eq_list_eq:
  ∀ (A: Type) (n: nat) (l1 l2 : list A)
    (p1 : length l1 = n)
    (p2 : length l2 = n),
    (l1 = l2) =
      (exist (fun l ⇒ length l = n) l1 p1 =
         exist (fun l ⇒ length l = n) l2 p2).
Proof.
  intros.
  propext.
  + intros. subst.
    fequal.
    apply proof_irrelevance.
  + intros.
    inversion H.
    reflexivity.
Qed.

Lemma Vector_eq:
  ∀ (A: Type) (n: nat)
    (v1 v2: Vector n A),
    proj1_sig v1 = proj1_sig v2 →
    v1 = v2.
Proof.
  intros.
  destruct v1.
  destruct v2.
  cbn in H.
  erewrite Vector_eq_list_eq in H.
  eassumption.
Defined.

Lemma Vector_sim_eq {n A} (v1 v2: Vector n A):
  v1 ~~ v2 → v1 = v2.
Proof.
  apply Vector_eq.
Qed.

#[export] Instance Reflexive_Vector_sim {n A}:
  Reflexive (@Vector_sim n n A).
Proof.
  unfold Reflexive. reflexivity.
Qed.

(* You need proof irrelevance to prove reflexivity *)
#[export] Instance Reflexive_Vector_fun_sim {n A B}:
  Reflexive (@Vector_fun_sim n n A B).
Proof.
  unfold Reflexive. intro f.
  unfold Vector_fun_sim.
  split; auto.
  intros.
  apply Vector_sim_eq in H.
  now subst.
Qed.

(* We cannot instantiate <<Symmetric>> because ~~ is parameterized by
n and m. *)
Lemma symmetric_Vector_sim
        `{v1: Vector n A}
        `{v2: Vector m A}:
  v1 ~~ v2 ↔
    v2 ~~ v1.
Proof.
  split; symmetry; assumption.
Qed.

Ltac vec_symmetry :=
  rewrite symmetric_Vector_sim.

Lemma symmetric_Vector_fun_sim
        `{f1: Vector n A → B}
        `{f2: Vector m A → B}:
  f1 ~!~ f2 ↔
    f2 ~!~ f1.
Proof.
  unfold Vector_fun_sim.
  (*
  split; intros.
  - symmetry. apply H. now vec_symmetry.
  - symmetry. apply H. now vec_symmetry.
  *)
  split; intros [H1 H2]; split; try congruence; subst.
  - symmetry. apply H2; auto. now vec_symmetry.
  - symmetry. apply H2; auto. now vec_symmetry.
Qed.

Ltac vec_fun_symmetry :=
  rewrite symmetric_Vector_fun_sim.

(* We cannot instantiate <<Transitive>> because ~~ is parameterized by
n and m. *)
Lemma transitive_Vector_sim
        `{v1: Vector n A}
        `{v2: Vector m A}
        `{v3: Vector p A}:
  v1 ~~ v2 → v2 ~~ v3 → v1 ~~ v3.
Proof.
  congruence.
Qed.

Lemma transitive_Vector_fun_sim
        `{f1: Vector n A → B}
        `{f2: Vector m A → B}
        `{f3: Vector p A → B}:
  f1 ~!~ f2 →
  f2 ~!~ f3 →
  f1 ~!~ f3.
Proof.
  intros.
  unfold Vector_fun_sim in ×.
  intuition.
  destruct H1.
  transitivity (f2 v1).
  - apply H2. reflexivity.
  - apply H3. assumption.
Qed.

Lemma Vector_coerce_sim_l {n m} `{v: Vector n A} (Heq: n = m):
    coerce Heq in v ~~ v.
Proof.
  unfold Vector_sim.
  rewrite (coerce_Vector_contents Heq).
  reflexivity.
Qed.

Lemma Vector_coerce_sim_r {n m} `{v: Vector n A} (Heq: n = m):
  v ~~ coerce Heq in v.
Proof.
  vec_symmetry.
  apply Vector_coerce_sim_l.
Qed.

(* Tactics *)
Lemma Vector_coerce_sim_l'
        {n m p} `{w: Vector p A} `{v: Vector n A} (Heq: n = m):
  v ~~ w →
  coerce Heq in v ~~ w.
Proof.
  apply transitive_Vector_sim.
  apply Vector_coerce_sim_l.
Qed.

Lemma Vector_coerce_sim_r'
        {n m p} `{w: Vector p A} `{v: Vector n A} (Heq: n = m):
  w ~~ v →
  w ~~ coerce Heq in v.
Proof.
  intro.
  vec_symmetry.
  eapply transitive_Vector_sim.
  apply Vector_coerce_sim_l.
  now vec_symmetry.
Qed.

Lemma Vector_coerce_fun_sim_l
        {n m A B} {f: Vector n A → B}:
  ∀ (Heq: m = n),
    (f ○ coerce_Vector_length Heq) ~!~ f.
Proof.
  intros Heq. destruct Heq.
  rewrite coerce_Vector_eq_refl_pf.
  reflexivity.
Qed.

Lemma Vector_coerce_fun_sim_r
        {n m A B} {f: Vector n A → B}:
  ∀ (Heq: m = n),
    f ~!~ (f ○ coerce_Vector_length Heq).
Proof.
  intros.
  vec_fun_symmetry.
  apply Vector_coerce_fun_sim_l.
Qed.

Lemma Vector_coerce_fun_sim_l'
        {n m p A B}
        {f: Vector n A → B} {g: Vector m A → B}:
  ∀ (Heq: p = n),
    f ~!~ g →
    (f ○ coerce_Vector_length Heq) ~!~ g.
Proof.
  unfold Vector_fun_sim.
  intros Heq1 [Heq2 Hfsim].
  split.
  - congruence.
  - intros v1 v2 Hsim.
    apply Hfsim.
    destruct Heq1.
    now rewrite coerce_Vector_eq_refl.
Qed.

Lemma Vector_coerce_fun_sim_r'
        {n m p A B}
        {f: Vector n A → B} {g: Vector m A → B}:
  ∀ (Heq: p = n),
    g ~!~ f →
    g ~!~ (f ○ coerce_Vector_length Heq).
Proof.
  intros.
  vec_fun_symmetry.
  apply Vector_coerce_fun_sim_l'.
  now vec_fun_symmetry.
Qed.

Lemma Vector_coerce_fun_coerce
        {n m A B} {f: Vector n A → B} {g: Vector m A → B}:
  ∀ (Heq: n = m),
    f ~!~ g →
    f = (g ○ coerce_Vector_length Heq).
Proof.
  intros.
  ext v.
  apply Vector_coerce_fun_sim_r'.
  assumption.
  reflexivity.
Qed.

Definition vnil {A}: Vector 0 A :=
  exist (fun l ⇒ length l = 0) nil eq_refl.

Definition vcons (n:nat) {A}:
  A →
  Vector n A →
  Vector (S n) A.
Proof.
  introv a v.
  destruct v as [vlist vlen].
  apply (exist (fun l ⇒ length l = S n) (cons a vlist)).
  cbn. fequal. assumption.
Defined.

Lemma vcons_eq_inv_both: ∀ (n: nat) (A: Type) (a1 a2: A) (v1 v2: Vector n A),
    vcons n a1 v1 = vcons n a2 v2 →
    a1 = a2 ∧ v1 = v2.
Proof.
  intros.
  destruct v1 as [l1 len1].
  destruct v2 as [l2 len2].
  cbn in H.
  inversion H.
  split; auto.
  apply Vector_sim_eq.
  unfold Vector_sim.
  assumption.
Qed.

Lemma vcons_eq_inv_hd: ∀ (n: nat) (A: Type) (a1 a2: A) (v1 v2: Vector n A),
    vcons n a1 v1 = vcons n a2 v2 →
    a1 = a2.
Proof.
  intros.
  apply vcons_eq_inv_both in H; tauto.
Qed.

Lemma vcons_eq_inv_tl: ∀ (n: nat) (A: Type) (a1 a2: A) (v1 v2: Vector n A),
    vcons n a1 v1 = vcons n a2 v2 →
    v1 = v2.
Proof.
  intros.
  apply vcons_eq_inv_both in H; tauto.
Qed.

Lemma proj_vnil: ∀ `(v: Vector 0 A),
    proj1_sig v = nil.
Proof.
  intros.
  destruct v as [v vlen].
  cbn.
  now apply List.length_zero_iff_nil.
Qed.

Lemma proj_vcons: ∀ (n: nat) `(a: A) (v: Vector n A),
    proj1_sig (vcons n a v) = cons a (proj1_sig v).
Proof.
  intros.
  destruct v as [vlist vlen].
  destruct vlen.
  reflexivity.
Qed.

Lemma vcons_sim
        {n m:nat} `{a:A}
        `{v1: Vector n A}
        `{v2: Vector m A}:
        v1 ~~ v2 →
      vcons n a v1 ~~ vcons m a v2.
Proof.
  intros.
  unfold Vector_sim in ×.
  do 2 rewrite proj_vcons.
  now rewrite H.
Qed.

(*
Instance vcons_resp:
  forall a n m, n = m ->
           vcons n a ~!~ vcons m a.
*)

(* This is better for rewriting *)
Lemma vcons_sim'
        {n:nat} `{a:A}
        `{v1: Vector n A}
        `{v2: Vector n A}:
        v1 ~~ v2 →
      vcons n a v1 = vcons n a v2.
Proof.
  intros.
  fequal.
  now apply Vector_eq.
Qed.

Definition vcons_resp:
  ∀ `(a:A) n,
    Vector_fun_indep (vcons n a).
Proof.
  intros.
  unfold Vector_fun_indep; split.
  - reflexivity.
  - intros. auto using vcons_sim'.
Qed.

Definition Vector_rev {n: nat} {A: Type}:
  Vector n A → Vector n A :=
  fun v ⇒ match v with
        | exist _ vlist vlen ⇒
            exist _ (List.rev vlist) (eq_trans (List.rev_length vlist) vlen)
        end.

Lemma Vector_rev_inv
        {n: nat} {A: Type}
        (v: Vector n A):
  Vector_rev (Vector_rev v) ~~ v.
Proof.
  destruct v as [vlist vlen].
  unfold Vector_sim.
  apply (List.rev_involutive vlist).
Qed.

Lemma Vector_rev_vnil: ∀ {A: Type},
    Vector_rev (@vnil A) = vnil.
Proof.
  unfold vnil.
  cbn.
  intros. fequal.
  apply proof_irrelevance.
Qed.

Lemma Vector_rev_vcons: ∀ {A: Type} {a: A} `{rest: Vector n A},
    Vector_rev (vcons n a rest) =
      Vector_rev (vcons n a rest).
Proof.
  intros.
  unfold Vector_rev.
  destruct (vcons n a rest).
Abort.

Section inversion.

  Section heads_tails.

    Context {A: Type} {n: nat}.

    Implicit Type (v: Vector (S n) A).

    (* Un-nil-ing *)
    Lemma Vector_nil_eq:
      ∀ `(v: Vector 0 A),
        v = vnil.
    Proof.
      intros.
      destruct v as [vlist vlen].
      assert (vlist = @nil A) by
        now rewrite (List.length_zero_iff_nil vlist) in vlen.
      subst.
      apply Vector_eq.
      reflexivity.
    Qed.

    Lemma Vector_uncons_exists:
      ∀ v, ∃ (a: A) (v': Vector n A),
        v = vcons n a v'.
    Proof.
      intros.
      destruct v as [vlist vlen].
      specialize (list_uncons_exists _ _ _ vlen).
      intros [vhd [vtl v_eq]].
      subst.
      ∃ vhd.
      ∃ (exist (fun l ⇒ length l = n) vtl (S_uncons vlen)).
      cbn.
      fequal.
      cbn in ×.
      apply proof_irrelevance.
    Qed.

    Lemma Vector_uncons_inform:
      ∀ v, {p: A × Vector n A | v = vcons n (fst p) (snd p)}.
    Proof.
      intros.
      destruct v as [vlist vlen].
      destruct (list_uncons_sigma2 vlist vlen) as [[vhd vtl] veq].
      subst.
      cbn in vlen.
      ∃ (vhd, (exist (fun l ⇒ length l = n)) vtl (S_uncons vlen)).
      cbn.
      fequal.
      apply proof_irrelevance.
    Defined.

    Definition Vector_uncons {n A} (v: Vector (S n) A):
      A × Vector n A :=
      let (vlist, vlen) := v in
      match vlist return (length vlist = S n → A × Vector n A) with
      | nil ⇒ zero_not_S
      | cons a rest ⇒ fun vlen ⇒ (a, exist _ rest (S_uncons vlen))
      end vlen.

    Lemma Vector_uncons_inform1 (v: Vector (S n) A):
      Vector_uncons v = proj1_sig (Vector_uncons_inform v).
    Proof.
      destruct v as [vlist vlen].
      destruct vlist.
      - inversion vlen.
      - cbn. reflexivity.
    Qed.

    Definition Vector_hd:
      Vector (S n) A → A :=
      fst ∘ Vector_uncons.

    Definition Vector_tl:
      Vector (S n) A → Vector n A :=
      snd ∘ Vector_uncons.

    Lemma Vector_list_hd (v: Vector (S n) A):
      Vector_hd v = list_hd (proj1_sig v) (proj2_sig v).
    Proof.
      intros.
      destruct v as [vlist vlen].
      destruct vlist.
      - inversion vlen.
      - reflexivity.
    Qed.

    Lemma proj_Vector_tl: ∀ `(v: Vector (S n) A),
        proj1_sig (Vector_tl v) = list_tl (proj1_sig v) (proj2_sig v).
    Proof.
      intros.
      destruct v as [vlist vlen].
      destruct vlist.
      - inversion vlen.
      - reflexivity.
    Qed.

    Lemma Vector_list_tl: ∀ `(v: Vector (S n) A),
        Vector_tl v = exist (fun l : list A ⇒ length l = n)
                            (list_tl (proj1_sig v) (proj2_sig v))
                            (list_tl_length (proj1_sig v) (proj2_sig v)).
    Proof.
      intros.
      destruct v as [vlist vlen].
      apply Vector_eq.
      rewrite proj_Vector_tl.
      reflexivity.
    Qed.

    Lemma Vector_surjective_pairing `{v: Vector (S n) A}:
      Vector_uncons v = (Vector_hd v , Vector_tl v).
    Proof.
      destruct v as [vlist vlen].
      unfold Vector_hd, Vector_tl.
      unfold compose.
      rewrite <- surjective_pairing.
      reflexivity.
    Qed.

    Lemma Vector_surjective_pairing2 `{v: Vector (S n) A}:
      v = vcons n (Vector_hd v) (Vector_tl v).
    Proof.
      destruct v as [vlist vlen].
      apply Vector_eq.
      rewrite proj_vcons.
      cbn.
      rewrite Vector_list_hd.
      rewrite Vector_list_tl.
      cbn.
      apply list_surjective_pairing2.
    Qed.

    Lemma Vector_hd_vcons {a} {v: Vector n A}:
      Vector_hd (vcons n a v) = a.
    Proof.
      destruct v.
      reflexivity.
    Qed.

    Lemma Vector_tl_vcons {a} {v: Vector n A}:
      Vector_tl (vcons n a v) = v.
    Proof.
      destruct v.
      cbn.
      fequal.
      apply proof_irrelevance.
    Qed.

  End heads_tails.

  Definition vunone {A}: Vector 1 A → A :=
    @Vector_hd A 0.

  Lemma Vector_hd_sim {n m A}
                      {v1: Vector (S n) A}
                      {v2: Vector (S m) A}:
    v1 ~~ v2 →
    Vector_hd v1 = Vector_hd v2.
  Proof.
    intro Hsim.
    rewrite Vector_list_hd.
    rewrite Vector_list_hd.
    unfold Vector_sim in Hsim.
    rewrite (list_hd_rw Hsim).
    apply list_hd_proof_irrelevance.
  Qed.

  Lemma Vector_tl_sim {n m A}
                      {v1: Vector (S n) A}
                      {v2: Vector (S m) A}:
    v1 ~~ v2 →
    Vector_tl v1 ~~ Vector_tl v2.
  Proof.
    intro Hsim.
    unfold Vector_sim in ×.
    rewrite proj_Vector_tl.
    rewrite proj_Vector_tl.
    rewrite (list_tl_rw Hsim).
    apply list_tl_proof_irrelevance.
  Qed.

  Corollary Vector_hd_coerce_eq
              {n m A}
              {v: Vector (S n) A}
              {Heq: S n = S m}:
    Vector_hd v = Vector_hd (coerce_Vector_length Heq v).
  Proof.
    apply Vector_hd_sim.
    apply Vector_coerce_sim_r.
  Qed.

  Corollary Vector_tl_coerce_sim
              {n m A}
              {v: Vector (S n) A}
              {Heq: S n = S m}:
    Vector_tl v ~~ Vector_tl (coerce_Vector_length Heq v).
  Proof.
    apply Vector_tl_sim.
    apply Vector_coerce_sim_r.
  Qed.

End inversion.

Ltac vector_sim :=
  repeat (match goal with
          | |- ?v ~~ coerce ?Heq in ?v ⇒
              apply Vector_coerce_sim_r
          | |- coerce ?Heq in ?v ~~ ?v ⇒
              apply Vector_coerce_sim_l
          | |- ?v ~~ coerce ?Heq in ?w ⇒
              apply Vector_coerce_sim_r'
          | |- coerce ?Heq in ?w ~~ ?v ⇒
              apply Vector_coerce_sim_l'
          | |- Vector_tl ?v ~~ Vector_tl ?w ⇒
              apply Vector_tl_sim
          | |- ?v ~!~ precoerce ?Heq in ?v ⇒
              apply Vector_coerce_fun_sim_r
          | |- precoerce ?Heq in ?v ~~ ?v ⇒
              apply Vector_coerce_fun_sim_l
          | |- ?v ~~ precoerce ?Heq in ?w ⇒
              apply Vector_coerce_fun_sim_r'
          | |- precoerce ?Heq in ?w ~~ ?v ⇒
              apply Vector_coerce_fun_sim_l'
          | |- _ ⇒ reflexivity
          | |- _ ⇒ assumption
          end).

Lemma Vector_induction_core:
  ∀ (A: Type)
    (P: ∀ m, Vector m A → Prop)
    (IHnil: P 0 vnil)
    (IHcons:
      ∀ a m (v: Vector m A), P m v → P (S m) (vcons m a v)),
  ∀ m (v: Vector m A), P m v.
Proof.
  intros.
  induction m.
  + rewrite Vector_nil_eq. assumption.
  + destruct (Vector_uncons_inform v) as [[vhd vtl] veq].
    subst. auto.
Qed.

Lemma Vector_induction:
  ∀ (m: nat) (A: Type) (P: ∀ m, Vector m A → Prop)
    (IHnil: P 0 vnil)
    (IHcons:
      ∀ a m (v: Vector m A), P m v → P (S m) (vcons m a v)),
  ∀ (v: Vector m A), P m v.
Proof.
  intros; apply Vector_induction_core; auto.
Qed.

Lemma Vector_induction2_core:
  ∀ (A: Type)
    (P: ∀ m, Vector m A → Vector m A → Prop)
    (IHnil: P 0 vnil vnil)
    (IHcons:
      ∀ m (a1 a2: A) (v1 v2: Vector m A),
        P m v1 v2 →
        P (S m) (vcons m a1 v1) (vcons m a2 v2)),
  ∀ (m : nat) (v1 v2: Vector m A), P m v1 v2.
Proof.
  intros.
  induction m.
  + rewrite Vector_nil_eq.
    rewrite (Vector_nil_eq v1).
    assumption.
  + destruct (Vector_uncons_inform v1) as
      [[v1hd v1tl] v1eq].
    destruct (Vector_uncons_inform v2) as
      [[v2hd v2tl] v2eq].
    subst; cbn; auto.
Qed.

Lemma Vector_induction2:
  ∀ (A: Type) (m n : nat)
    (P: ∀ m n, Vector m A → Vector n A → Prop)
    (IHnil: P 0 0 vnil vnil)
    (IHcons:
      ∀ m n (a1 a2: A) (v1: Vector m A) (v2: Vector n A),
        P m n v1 v2 →
        P (S m) (S n) (vcons m a1 v1) (vcons n a2 v2)),
  ∀ (v1: Vector m A) (v2: Vector n A),
    n = m → P m n v1 v2.
Proof.
  intros.
  subst.
  apply (Vector_induction2_core A (fun m ⇒ P m m)).
  assumption.
  auto.
Qed.

Fixpoint Vector_repeat
           (n: nat) {A: Type} (a : A): Vector n A :=
  match n with
  | 0 ⇒ vnil
  | S m ⇒ vcons m a (Vector_repeat m a)
  end.

Definition Vector_tt (n: nat): Vector n unit :=
  Vector_repeat n tt.

Section sec.

  Context (A: Type).

  Definition Vector_to_list {n:nat}: Vector n A → list A :=
    @proj1_sig (list A) _.

  Lemma Vector_to_list_vnil:
    Vector_to_list vnil = @nil A.
  Proof.
    reflexivity.
  Qed.

  Lemma Vector_to_list_vcons {a} {n} {v: Vector n A}:
    Vector_to_list (vcons _ a v) = a :: Vector_to_list v.
  Proof.
    destruct v.
    unfold vcons.
    reflexivity.
  Qed.

  Definition artificial_surjection {n:nat} (x: Vector n A):
    list A → Vector n A :=
    fun l ⇒
      match (decide_length n l) with
      | left Heq ⇒ (exist _ l Heq)
      | right _ ⇒ x
      end.

  Lemma artificial_surjection_inv n (x:Vector n A) (l:list A) (Heq: length l = n):
    proj1_sig (artificial_surjection x l) = l.
  Proof.
    unfold artificial_surjection.
    assert (decide_length n l = left Heq).
    { destruct (decide_length n l).
      + fequal. apply proof_irrelevance.
      + contradiction.
    }
    rewrite H.
    reflexivity.
  Qed.

  Lemma Vector_to_list_length: ∀ (n:nat) (x: Vector n A),
      length (Vector_to_list x) = n.
  Proof.
    intros.
    destruct x.
    assumption.
  Qed.

  Lemma artificial_iso {n:nat}(x: Vector n A):
    artificial_surjection x ∘ Vector_to_list = id.
  Proof.
    intros.
    ext v.
    unfold compose.
    destruct v.
    apply Vector_eq.
    rewrite artificial_surjection_inv.
    - reflexivity.
    - rewrite Vector_to_list_length.
      reflexivity.
  Qed.

  Lemma functors_preserve_inj `{Functor F}:
    ∀ {A B: Type} (f: A → B) (g: B → A)
      (Hinv: g ∘ f = id) (a1 a2: F A),
      map f a1 = map f a2 → a1 = a2.
  Proof.
    introv Hinv Heq.
    change (id a1 = id a2).
    rewrite <- (fun_map_id (F := F)).
    rewrite <- Hinv.
    rewrite <- (fun_map_map (F := F)).
    unfold compose.
    rewrite Heq.
    reflexivity.
  Qed.

  Lemma functors_preserve_inj2 `{Functor F}:
    ∀ {A B: Type} (f: A → B) (a1 a2: F A),
    (∃ g: B → A, g ∘ f = id) →
      map f a1 = map f a2 → a1 = a2.
  Proof.
    introv Hinv. destruct Hinv.
    eapply functors_preserve_inj.
    eassumption.
  Qed.

  Lemma functors_preserve_inj4 `{Applicative F}:
    ∀ {A1 A2 B: Type} (f: A1 → A2 → B) (a1 a2: F A1) (a1' a2': F A2),
    (∃ g: B → A1 × A2, (∀ x y, (compose g ∘ f) x y = (x, y))) →
    pure f <⋆> a1 <⋆> a1'
    = pure f <⋆> a2 <⋆> a2'
    → a1 = a2 ∧ a1' = a2'.
  Proof.
    introv Hinv Heq.
    enough (cut: (a1, a1') = (a2, a2')).
    { inversion cut. now subst. }
    change (id (a1, a1') = (a2, a2')).
    assert (a1 ⊗ a1' = a2 ⊗ a2' → (a1, a1') = (a2, a2')).
    { intro eq_mult.
      assert (map fst (a1 ⊗ a1') =
                map fst (a2 ⊗ a2'))
               by now rewrite eq_mult.
      assert (map snd (a1 ⊗ a1') =
                map snd (a2 ⊗ a2'))
        by now rewrite eq_mult.
      assert (map (F := F) (fun x ⇒ (fst x, snd x)) (a1 ⊗ a1') =
                map (fun x ⇒ (fst x, snd x)) (a2 ⊗ a2')).
      { rewrite eq_mult. reflexivity. }
  Abort.

  Lemma functors_preserve_inj3 `{Applicative F}:
    ∀ {A B: Type} (f: A → B) (a1 a2: F A),
    (∃ g: B → A, g ∘ f = id) →
    pure f <⋆> a1 = pure f <⋆> a2 → a1 = a2.
  Proof.
    introv Hinv.
    rewrite <- map_to_ap.
    rewrite <- map_to_ap.
    apply functors_preserve_inj2.
    assumption.
  Qed.

  Lemma Vector_pres_inj {n:nat} (v: Vector n A) `{Functor F}:
    ∀ (x y: F (Vector n A)),
      map Vector_to_list x = map Vector_to_list y →
      x = y.
  Proof.
    introv Heq.
    assert (map (artificial_surjection v) (map Vector_to_list x)
            = map (artificial_surjection v) (map Vector_to_list y)).
    { now rewrite Heq. }
    generalize H0.
    compose near x.
    compose near y.
    rewrite (fun_map_map).
    rewrite artificial_iso.
    rewrite fun_map_id.
    unfold id.
    auto.
  Qed.

End sec.

Definition map_Vector
             (n : nat) {A B : Type} (f : A → B)
             (v : Vector n A): Vector n B :=
  match v with
  | exist _ l p ⇒
      exist _ (map (F := list) f l)
            (eq_trans (map_preserve_length A B f l) p)
  end.

#[export] Instance Map_Vector (n: nat) : Map (Vector n) := @map_Vector n.

Lemma fun_map_id_Vector : ∀ (n : nat) (A : Type),
    map (F := Vector n) id = @id (Vector n A).
Proof.
  intros.
  ext [l Heq].
  apply Vector_eq.
  cbn.
  now rewrite fun_map_id.
Qed.

Lemma fun_map_map_Vector : ∀ (n : nat) (A B C : Type) (f : A → B) (g : B → C),
    map (F := Vector n) g ∘ map (F := Vector n) f = map (F := Vector n) (g ∘ f).
Proof.
  intros.
  ext [l Heq].
  apply Vector_eq.
  cbn. compose near l on left.
  now rewrite fun_map_map.
Qed.

#[export] Instance Functor_Vector (n : nat) : Functor (Vector n) :=
  {| fun_map_id := fun_map_id_Vector n;
    fun_map_map := fun_map_map_Vector n;
  |}.

Lemma map_coerce_Vector:
  ∀ (A B: Type) (f: A → B) (n m: nat) (Heq: n = m) (v: Vector n A),
    map f v ~~ map f (coerce Heq in v).
Proof.
  intros. unfold Vector_sim.
  destruct v as [l Hlen].
  reflexivity.
Qed.

Lemma map_coerce_Vector2:
  ∀ (A B: Type) (f: A → B) (n m: nat) (Heq: n = m) (v: Vector n A),
    map f (coerce Heq in v) = coerce Heq in (map f v).
Proof.
  intros.
  unfold Vector_sim.
  subst.
  rewrite coerce_Vector_eq_refl.
  rewrite coerce_Vector_eq_refl.
  reflexivity.
Qed.

Lemma Vector_coerce_map_l'
  {n m p} `{f: A → B}
  `{w: Vector p A} `{v: Vector n B}
  (Heq: p = m):
    coerce Heq in (map f w) ~~ v →
    map f (coerce Heq in w) ~~ v.
Proof.
  intros.
  rewrite (map_coerce_Vector2).
  assumption.
Qed.

Lemma Vector_coerce_map_r'
  {n m p} `{f: A → B}
  `{w: Vector p A} `{v: Vector n B}
  (Heq: p = m):
  (v ~~ coerce Heq in (map f w)) →
  v ~~ map f (coerce Heq in w).
Proof.
  intros.
  rewrite (map_coerce_Vector2).
  assumption.
Qed.

Ltac vector_sim ::=
  repeat (match goal with
          | |- _ ⇒ reflexivity
          | |- _ ⇒ assumption
          | |- ?v ~~ coerce ?Heq in ?v ⇒
              apply Vector_coerce_sim_r
          | |- coerce ?Heq in ?v ~~ ?v ⇒
              apply Vector_coerce_sim_l
          | |- ?v ~~ coerce ?Heq in ?w ⇒
              apply Vector_coerce_sim_r'
          | |- coerce ?Heq in ?w ~~ ?v ⇒
              apply Vector_coerce_sim_l'
          | |- Vector_tl ?v ~~ Vector_tl ?w ⇒
              apply Vector_tl_sim
          | |- ?v ~!~ precoerce ?Heq in ?v ⇒
              apply Vector_coerce_fun_sim_r
          | |- precoerce ?Heq in ?v ~~ ?v ⇒
              apply Vector_coerce_fun_sim_l
          | |- ?v ~~ precoerce ?Heq in ?w ⇒
              apply Vector_coerce_fun_sim_r'
          | |- precoerce ?Heq in ?w ~~ ?v ⇒
              apply Vector_coerce_fun_sim_l'
          | |- map ?f (coerce ?Heq in ?w) ~~ ?v ⇒
              apply Vector_coerce_map_l'
          | |- ?v ~~ map ?f (coerce ?Heq in ?w) ⇒
              apply Vector_coerce_map_r'
          end).

Lemma map_sim_function `{Functor F} (A B: Type) (n m: nat):
  ∀ (f: Vector n A → B) (g: Vector m A → B)
    (Heq: n = m),
    f ~!~ g →
    map (F := F) f = map (precoerce Heq in g).
Proof.
  introv Hsim.
  rewrite (Vector_coerce_fun_coerce Heq Hsim).
  reflexivity.
Qed.

Lemma map_Vector_vnil:
  ∀ {A B : Type} (f : A → B),
    map f vnil = vnil.
Proof.
  intros.
  apply Vector_eq.
  reflexivity.
Qed.

Lemma map_Vector_rw2:
  ∀ {A B : Type} (f : A → B)
    (a : A) (l: list A)
    (n : nat)
    (p : length (a :: l) = S n),
    map f (exist _ (a :: l) p) =
      vcons n (f a) (map f (exist (fun l ⇒ length l = n) l (S_uncons p))).
Proof.
  intros.
  apply Vector_eq.
  reflexivity.
Qed.

Lemma map_Vector_vcons:
  ∀ {A B : Type} (f : A → B)
     (n : nat) (v : Vector n A) (a : A),
    map f (vcons n a v) =
      vcons n (f a) (map f v).
Proof.
  intros.
  destruct v.
  unfold vcons.
  rewrite map_Vector_rw2.
  cbn. fequal.
  apply proof_irrelevance.
Qed.

Definition traverse_Vector_core
             {G} `{Map G} `{Pure G} `{Mult G}
             {A B : Type} (f : A → G B)
             (vlist : list A) `(vlen : length vlist = n) : G (Vector n B) :=
      (fix go (vl : list A) n : length vl = n → G (Vector n B) :=
         match vl
               return length vl = n → G (Vector n B)
         with
         | nil ⇒
             fun vlen ⇒
               pure (F := G) (exist _ nil vlen)
         | cons a rest ⇒
             fun vlen ⇒
               match n return
                     length (a :: rest) = n → G (Vector n B)
               with
               | O ⇒ fun vlen' ⇒ zero_not_S (eq_sym vlen')
               | S m ⇒
                   fun vlen' ⇒
                     pure (@vcons m B) <⋆> f a <⋆> go rest m (S_uncons vlen')
               end vlen
         end) vlist n vlen.

Definition traverse_Vector
             (n : nat) (G : Type → Type) `{Map G} `{Pure G} `{Mult G}
             {A B : Type} (f : A → G B)
             (v : Vector n A) : G (Vector n B) :=
  match v with
  | exist _ vlist vlen ⇒
      traverse_Vector_core f vlist vlen
  end.

#[export] Instance Traverse_Vector {n}: Traverse (Vector n)
  := traverse_Vector n.

#[export] Instance ToBatch_Vector {n: nat}:
  Coalgebraic.TraversableFunctor.ToBatch (Vector n) :=
  KleisliToCoalgebraic.TraversableFunctor.DerivedOperations.ToBatch_Traverse.

Lemma traverse_Vector_vnil:
  ∀ (G : Type → Type) `{Map G} `{Pure G} `{Mult G}
    {A B : Type} (f : A → G B),
    traverse f vnil = pure vnil.
Proof.
  intros.
  reflexivity.
Qed.

Lemma traverse_Vector_rw_lemma:
  ∀ (n : nat) (G : Type → Type) `{Map G} `{Pure G} `{Mult G}
    {A B : Type} (f : A → G B)
    (a : A) (l: list A)
    (p : length (a :: l) = S n),
    traverse f (exist _ (a :: l) p) =
      pure (vcons n) <⋆> f a <⋆>
        traverse f (exist (fun l ⇒ length l = n) l (S_uncons p)).
Proof.
  intros.
  reflexivity.
Qed.

Lemma traverse_Vector_vcons:
  ∀ (n : nat) (G : Type → Type) `{Map G} `{Pure G} `{Mult G}
    {A B : Type} (f : A → G B)
    (v : Vector n A) (a : A),
    traverse f (vcons n a v) =
      pure (vcons n) <⋆> f a <⋆> traverse f v.
Proof.
  intros.
  destruct v.
  unfold vcons.
  rewrite traverse_Vector_rw_lemma.
  fequal.
  fequal.
  fequal.
  apply proof_irrelevance.
Qed.