vector.v 4.36 KB
Newer Older
1
2
3
From iris.prelude Require Export vector.
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
60
61
  Qed.

  Global Instance vec_to_list_ne n m :
    Proper (dist n ==> dist n) (@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
102
103
104
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
  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).
Instance vecC_map_ne {A A'} m n :
  Proper (dist n ==> dist n) (@vecC_map A A' m).
Proof. intros f g ? v. by apply vec_map_ext_ne. Qed.

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.