Require Import String Showable Equiv DepEquiv Decidable HODepEquiv HoTT.
Require Import Vector List.
Local Open Scope string_scope.

Notation "{ x : A & P }" := (sigT (A:=A) (fun x ⇒ P)) : type_scope.
Notation "x .1" := (projT1 x) (at level 3).
Notation "x .2" := (projT2 x) (at level 3).
Notation " ( x ; p ) " := (existT _ x p).


Definition vector A := Vector.t A.
Definition vnil {A} := Vector.nil A.
Definition vcons {A n} (val:A) (v:vector A n) := Vector.cons A val _ v.

Definition pop' {A} (l: list A): list A :=
  match l with
    | nil ⇒ nil
    | x :: l' ⇒ l'
  end.

Definition bad_pop {A} (l: list A): list A :=
  match l with
    | nil ⇒ nil
    | x :: l' ⇒ l
  end.

 {n:nat & Vector.t A n} ~ {l : list A & length l = n}

Fixpoint vector_to_list A (n:nat):
  Vector.t A n → {l : list A & clift (length (A:=A)) l = Some n} :=
  match n return Vector.t A n → {l : list A & clift (info:=Cast_info) (length (A:=A)) l = Some n} with
  | O ⇒ fun _ ⇒ (nil; eq_refl)
  | S n ⇒ fun v ⇒ let IHn := vector_to_list A n (Vector.tl v) in
           ((Vector.hd v) :: IHn.1 ; ap _ (ap S (Some_inj (IHn.2)))) end.

Definition list_to_vector A (n:nat) : {l : list A & clift (info := Cast_info) (length (A:=A)) l = Some n} → Vector.t A n.
Defined.

Definition transport_vector A n a (s:vector A n) k (e : n = k):
  ap S e # vcons a s = vcons a (e # s).
Defined.

Definition S_length :
  ∀ (A : Type) (l : list A) (n: nat),
    length l = S n → length (tail l) = n.
Defined.


Instance DepEquiv_vector_list_simpl A `{Show A} `{DecidablePaths A} :
  (vector A) ≈ list A :=
  @DepEquiv_eq nat (vector A) (list A) _ _ _ (clift (length (A:=A)))
              (vector_to_list A) (list_to_vector A) _ _ _.

Definition map_list (f : nat → nat) : list nat ⇀ list nat :=
  lift (Vector.map f).

Definition pop : list nat ⇀ list nat := lift (Vector.tl).

Eval compute in (pop nil).