vector.v 4.32 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export vector.
2 3
From iris.algebra Require Export ofe.
From iris.algebra Require Import list.
4
Set Default Proof Using "Type".
5 6 7 8 9 10 11 12 13 14

Section ofe.
  Context {A : ofeT}.

  Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A).
  Instance vec_dist m : Dist (vec A m) := dist (A:=list A).

  Definition vec_ofe_mixin m : OfeMixin (vec A m).
  Proof.
    split.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
    - intros v w. apply (equiv_dist (A:=listC A)).
16 17
    - unfold dist, vec_dist. split.
        by intros ?. by intros ??. by intros ?????; etrans.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
    - intros n v w. by apply (dist_S (A:=listC A)).
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
  Qed.
  Canonical Structure vecC m : ofeT := OfeT (vec A m) (vec_ofe_mixin m).

  Global Instance vnil_timeless : Timeless (@vnil A).
  Proof. intros v _. by inv_vec v. Qed.
  Global Instance vcons_timeless n x (v : vec A n) :
    Timeless x  Timeless v  Timeless (x ::: v).
  Proof.
    intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
    constructor. by apply timeless. change (v  v'). by apply timeless.
  Qed.
  Global Instance vec_discrete_cofe m : Discrete A  Discrete (vecC m).
  Proof. intros ? v. induction v; apply _. Qed.
End ofe.

Arguments vecC : clear implicits.
Typeclasses Opaque vec_dist.

Section proper.
  Context {A : ofeT}.

  Global Instance vcons_ne n :
    Proper (dist n ==> forall_relation (λ _, dist n ==> dist n)) (@vcons A).
  Proof. by constructor. Qed.
  Global Instance vcons_proper :
    Proper (equiv ==> forall_relation (λ _, equiv ==> equiv)) (@vcons A).
  Proof. by constructor. Qed.

  Global Instance vlookup_ne n m :
    Proper (dist n ==> eq ==> dist n) (@Vector.nth A m).
  Proof.
    intros v. induction v as [|x m v IH]; intros v'; inv_vec v'.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
    - intros _ x. inv_fin x.
    - intros x' v' EQ i ? <-. inversion_clear EQ. inv_fin i=> // i. by apply IH.
53 54 55 56
  Qed.
  Global Instance vlookup_proper m :
    Proper (equiv ==> eq ==> equiv) (@Vector.nth A m).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    intros v v' ? x x' ->. apply equiv_dist=> n. f_equiv. by apply equiv_dist.
58 59
  Qed.

60 61
  Global Instance vec_to_list_ne m :
    NonExpansive (@vec_to_list A m).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Proof. by intros v v'. Qed.
63 64
  Global Instance vec_to_list_proper m :
    Proper (equiv ==> equiv) (@vec_to_list A m).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  Proof. by intros v v'. Qed.
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
End proper.

Section cofe.
  Context `{Cofe A}.

  Global Program Instance list_cofe m : Cofe (vecC A m) :=
    {| compl c :=
         eq_rect _ (vec A) (list_to_vec (compl (chain_map vec_to_list c))) _ _ |}.
  Next Obligation.
    intros. by rewrite (conv_compl 0) vec_to_list_length.
  Qed.
  Next Obligation.
    simpl. intros m n c. unfold dist, ofe_dist, vecC, vec_dist.
    destruct (list_cofe_obligation_1 m c).
    by rewrite /= vec_to_list_of_list conv_compl.
  Qed.
End cofe.

(** Functor *)
Definition vec_map {A B : ofeT} m (f : A  B) : vecC A m  vecC B m :=
  @vmap A B f m.
Lemma vec_map_ext_ne {A B : ofeT} m (f g : A  B) (v : vec A m) n :
  ( x, f x {n} g x)  vec_map m f v {n} vec_map m g v.
Proof.
  intros Hf. eapply (list_fmap_ext_ne f g v) in Hf.
  by rewrite -!vec_to_list_map in Hf.
Qed.
Instance vec_map_ne {A B : ofeT} m f n :
  Proper (dist n ==> dist n) f 
  Proper (dist n ==> dist n) (@vec_map A B m f).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  intros ? v v' H. eapply list_fmap_ne in H; last done.
98 99 100 101
  by rewrite -!vec_to_list_map in H.
Qed.
Definition vecC_map {A B : ofeT} m (f : A -n> B) : vecC A m -n> vecC B m :=
  CofeMor (vec_map m f).
102 103 104
Instance vecC_map_ne {A A'} m :
  NonExpansive (@vecC_map A A' m).
Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129

Program Definition vecCF (F : cFunctor) m : cFunctor := {|
  cFunctor_car A B := vecC (cFunctor_car F A B) m;
  cFunctor_map A1 A2 B1 B2 fg := vecC_map m (cFunctor_map F fg)
|}.
Next Obligation.
  intros F A1 A2 B1 B2 n m f g Hfg. by apply vecC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
  intros F m A B l.
  change (vec_to_list (vec_map m (cFunctor_map F (cid, cid)) l)  l).
  rewrite vec_to_list_map. apply listCF.
Qed.
Next Obligation.
  intros F m A1 A2 A3 B1 B2 B3 f g f' g' l.
  change (vec_to_list (vec_map m (cFunctor_map F (f  g, g'  f')) l)
     vec_map m (cFunctor_map F (g, g')) (vec_map m (cFunctor_map F (f, f')) l)).
  rewrite !vec_to_list_map. by apply (cFunctor_compose (listCF F)  f g f' g').
Qed.

Instance vecCF_contractive F m :
  cFunctorContractive F  cFunctorContractive (vecCF F m).
Proof.
  by intros ?? A1 A2 B1 B2 n ???; apply vecC_map_ne; first apply cFunctor_contractive.
Qed.