Library DIPop
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.
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.
Pop from list
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.
Type equivalence
{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) _ _ _.
We simply lifting the domain