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 xP)) : 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

This example is taken from the "Dependent Interoperability" paper. The objective is to cast a simply-typed pop to a precise type on indexed vectors.

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

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

Type equivalence

We establish the following 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
  | Ofun _(nil; eq_refl)
  | S nfun vlet 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) _ _ _.


Monadic Liftings



We simply lifting the domain

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).