iprod.v 13 KB
Newer Older
1
From algebra Require Export cmra.
2
From algebra Require Import functor upred.
3

4
(** * Indexed product *)
5 6
(** Need to put this in a definition to make canonical structures to work. *)
Definition iprod {A} (B : A  cofeT) :=  x, B x.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Definition iprod_insert {A} {B : A  cofeT} `{ x x' : A, Decision (x = x')}
8 9
    (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
  match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
10 11 12 13
Global Instance iprod_empty {A} {B : A  cofeT}
  `{ x, Empty (B x)} : Empty (iprod B) := λ x, .
Definition iprod_singleton {A} {B : A  cofeT} 
    `{ x x' : A, Decision (x = x'),  x : A, Empty (B x)}
14
  (x : A) (y : B x) : iprod B := iprod_insert x y .
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16
Instance: Params (@iprod_insert) 4.
Instance: Params (@iprod_singleton) 5.
17 18 19 20 21

Section iprod_cofe.
  Context {A} {B : A  cofeT}.
  Implicit Types x : A.
  Implicit Types f g : iprod B.
22

23
  Instance iprod_equiv : Equiv (iprod B) := λ f g,  x, f x  g x.
24
  Instance iprod_dist : Dist (iprod B) := λ n f g,  x, f x {n} g x.
25 26 27 28 29 30 31 32
  Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) :=
    {| chain_car n := c n x |}.
  Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
  Program Instance iprod_compl : Compl (iprod B) := λ c x,
    compl (iprod_chain c x).
  Definition iprod_cofe_mixin : CofeMixin (iprod B).
  Proof.
    split.
33
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
34
      intros Hfg k; apply equiv_dist; intros n; apply Hfg.
35
    - intros n; split.
36 37
      + by intros f x.
      + by intros f g ? x.
38
      + by intros f g h ?? x; trans (g x).
39
    - intros n f g Hfg x; apply dist_S, Hfg.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
    - intros n c x.
      rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
42 43 44 45
      apply (chain_cauchy c); lia.
  Qed.
  Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.

46 47 48 49
  (** Properties of empty *)
  Section empty.
    Context `{ x, Empty (B x)}.
    Definition iprod_lookup_empty  x :  x =  := eq_refl.
50
    Global Instance iprod_empty_timeless :
51
      ( x : A, Timeless ( : B x))  Timeless ( : iprod B).
52
    Proof. intros ? f Hf x. by apply: timeless. Qed.
53 54
  End empty.

55
  (** Properties of iprod_insert. *)
56
  Context `{ x x' : A, Decision (x = x')}.
57

Robbert Krebbers's avatar
Robbert Krebbers committed
58
  Global Instance iprod_insert_ne n x :
59 60 61 62 63 64 65
    Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
  Proof.
    intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
    by destruct (decide _) as [[]|].
  Qed.
  Global Instance iprod_insert_proper x :
    Proper (() ==> () ==> ()) (iprod_insert x) := ne_proper_2 _.
66

67 68 69 70 71 72 73 74 75
  Lemma iprod_lookup_insert f x y : (iprod_insert x y f) x = y.
  Proof.
    rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done.
    by rewrite (proof_irrel Hx eq_refl).
  Qed.
  Lemma iprod_lookup_insert_ne f x x' y :
    x  x'  (iprod_insert x y f) x' = f x'.
  Proof. by rewrite /iprod_insert; destruct (decide _). Qed.

76
  Global Instance iprod_lookup_timeless f x : Timeless f  Timeless (f x).
77
  Proof.
78
    intros ? y ?.
79
    cut (f  iprod_insert x y f).
80
    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
81
    by apply: timeless=>x'; destruct (decide (x = x')) as [->|];
82
      rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
83 84 85 86
  Qed.
  Global Instance iprod_insert_timeless f x y :
    Timeless f  Timeless y  Timeless (iprod_insert x y f).
  Proof.
87
    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
88
    - rewrite iprod_lookup_insert.
89
      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert.
90
    - rewrite iprod_lookup_insert_ne //.
91
      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne.
92 93 94
  Qed.

  (** Properties of iprod_singletom. *)
95
  Context `{ x : A, Empty (B x)}.
96

Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Global Instance iprod_singleton_ne n x :
98 99 100 101
    Proper (dist n ==> dist n) (iprod_singleton x).
  Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed.
  Global Instance iprod_singleton_proper x :
    Proper (() ==> ()) (iprod_singleton x) := ne_proper _.
102

103 104
  Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y.
  Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
105
  Lemma iprod_lookup_singleton_ne x x' y: x  x'  (iprod_singleton x y) x' = .
106
  Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
107 108

  Global Instance iprod_singleton_timeless x (y : B x) :
109 110
    ( x : A, Timeless ( : B x))  Timeless y  Timeless (iprod_singleton x y).
  Proof. eauto using iprod_insert_timeless, iprod_empty_timeless. Qed.
111 112 113 114 115 116 117
End iprod_cofe.

Arguments iprodC {_} _.

Section iprod_cmra.
  Context {A} {B : A  cmraT}.
  Implicit Types f g : iprod B.
118

119 120
  Instance iprod_op : Op (iprod B) := λ f g x, f x  g x.
  Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
121
  Instance iprod_valid : Valid (iprod B) := λ f,  x,  f x.
122
  Instance iprod_validN : ValidN (iprod B) := λ n f,  x, {n} f x.
123
  Instance iprod_minus : Minus (iprod B) := λ f g x, f x  g x.
124 125 126

  Definition iprod_lookup_op f g x : (f  g) x = f x  g x := eq_refl.
  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
127
  Definition iprod_lookup_minus f g x : (f  g) x = f x  g x := eq_refl.
128

Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Lemma iprod_included_spec (f g : iprod B) : f  g   x, f x  g x.
130 131
  Proof.
    split.
132 133
    - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
    - intros Hh; exists (g  f)=> x; specialize (Hh x).
134 135
      by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137 138 139 140 141 142
  Lemma iprod_includedN_spec n (f g : iprod B) : f {n} g   x, f x {n} g x.
  Proof.
    split.
    - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
    - intros Hh; exists (g  f)=> x; specialize (Hh x).
      by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus'.
  Qed.
143

144 145 146
  Definition iprod_cmra_mixin : CMRAMixin (iprod B).
  Proof.
    split.
147 148 149 150
    - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
    - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
    - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
151 152 153
    - intros g; split.
      + intros Hg n i; apply cmra_valid_validN, Hg.
      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
154 155 156 157 158
    - intros n f Hf x; apply cmra_validN_S, Hf.
    - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
    - by intros f1 f2 x; rewrite iprod_lookup_op comm.
    - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
    - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
    - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
      by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf.
161
    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
    - intros f1 f2; rewrite iprod_included_spec=> Hf x.
163
      by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
164 165 166 167
    - intros n f f1 f2 Hf Hf12.
      set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
      exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
      split_and?; intros x; apply (proj2_sig (g x)).
168
  Qed.
169
  Canonical Structure iprodRA : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin.
170 171 172 173
  Global Instance iprod_cmra_identity `{ x, Empty (B x)} :
    ( x, CMRAIdentity (B x))  CMRAIdentity iprodRA.
  Proof.
    intros ?; split.
174
    - intros x; apply cmra_empty_valid.
175 176
    - by intros f x; rewrite iprod_lookup_op left_id.
    - by apply _.
177 178
  Qed.

179 180
  (** Internalized properties *)
  Lemma iprod_equivI {M} g1 g2 : (g1  g2)%I  ( i, g1 i  g2 i : uPred M)%I.
181
  Proof. by uPred.unseal. Qed.
182
  Lemma iprod_validI {M} g : ( g)%I  ( i,  g i : uPred M)%I.
183
  Proof. by uPred.unseal. Qed.
184

185
  (** Properties of iprod_insert. *)
186
  Context `{ x x' : A, Decision (x = x')}.
187

188 189 190 191
  Lemma iprod_insert_updateP x (P : B x  Prop) (Q : iprod B  Prop) g y1 :
    y1 ~~>: P  ( y2, P y2  Q (iprod_insert x y2 g)) 
    iprod_insert x y1 g ~~>: Q.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
    intros Hy1 HP n gf Hg. destruct (Hy1 n (gf x)) as (y2&?&?).
193 194 195 196 197 198 199 200 201 202 203 204 205 206
    { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
    exists (iprod_insert x y2 g); split; [auto|].
    intros x'; destruct (decide (x' = x)) as [->|];
      rewrite iprod_lookup_op ?iprod_lookup_insert //; [].
    move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne.
  Qed.

  Lemma iprod_insert_updateP' x (P : B x  Prop) g y1 :
    y1 ~~>: P 
    iprod_insert x y1 g ~~>: λ g',  y2, g' = iprod_insert x y2 g  P y2.
  Proof. eauto using iprod_insert_updateP. Qed.
  Lemma iprod_insert_update g x y1 y2 :
    y1 ~~> y2  iprod_insert x y1 g ~~> iprod_insert x y2 g.
  Proof.
207
    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
208 209
  Qed.

210
  (** Properties of iprod_singleton. *)
211
  Context `{ x, Empty (B x),  x, CMRAIdentity (B x)}.
212

213
  Lemma iprod_singleton_validN n x (y: B x) : {n} iprod_singleton x y  {n} y.
214
  Proof.
215 216 217
    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
    move=>Hx x'; destruct (decide (x = x')) as [->|];
      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
218
    by apply cmra_empty_validN.
219 220
  Qed.

221 222 223
  Lemma iprod_unit_singleton x (y : B x) :
    unit (iprod_singleton x y)  iprod_singleton x (unit y).
  Proof.
224 225 226
    by move=>x'; destruct (decide (x = x')) as [->|];
      rewrite iprod_lookup_unit ?iprod_lookup_singleton
      ?iprod_lookup_singleton_ne // cmra_unit_empty.
227 228
  Qed.

229 230 231 232
  Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
    iprod_singleton x y1  iprod_singleton x y2  iprod_singleton x (y1  y2).
  Proof.
    intros x'; destruct (decide (x' = x)) as [->|].
233 234
    - by rewrite iprod_lookup_op !iprod_lookup_singleton.
    - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
235 236 237 238 239 240 241 242
  Qed.

  Lemma iprod_singleton_updateP x (P : B x  Prop) (Q : iprod B  Prop) y1 :
    y1 ~~>: P  ( y2, P y2  Q (iprod_singleton x y2)) 
    iprod_singleton x y1 ~~>: Q.
  Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
  Lemma iprod_singleton_updateP' x (P : B x  Prop) y1 :
    y1 ~~>: P 
243
    iprod_singleton x y1 ~~>: λ g,  y2, g = iprod_singleton x y2  P y2.
244
  Proof. eauto using iprod_singleton_updateP. Qed.
245 246 247
  Lemma iprod_singleton_update x y1 y2 :
    y1 ~~> y2  iprod_singleton x y1 ~~> iprod_singleton x y2.
  Proof. eauto using iprod_insert_update. Qed.
248 249

  Lemma iprod_singleton_updateP_empty x (P : B x  Prop) (Q : iprod B  Prop) :
250
     ~~>: P  ( y2, P y2  Q (iprod_singleton x y2))   ~~>: Q.
251
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
    intros Hx HQ n gf Hg. destruct (Hx n (gf x)) as (y2&?&?); first apply Hg.
253 254
    exists (iprod_singleton x y2); split; [by apply HQ|].
    intros x'; destruct (decide (x' = x)) as [->|].
255 256
    - by rewrite iprod_lookup_op iprod_lookup_singleton.
    - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
257
  Qed.
258 259 260
  Lemma iprod_singleton_updateP_empty' x (P : B x  Prop) :
     ~~>: P   ~~>: λ g,  y2, g = iprod_singleton x y2  P y2.
  Proof. eauto using iprod_singleton_updateP_empty. Qed.
261 262 263 264
End iprod_cmra.

Arguments iprodRA {_} _.

265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
(** * Functor *)
Definition iprod_map {A} {B1 B2 : A  cofeT} (f :  x, B1 x  B2 x)
  (g : iprod B1) : iprod B2 := λ x, f _ (g x).

Lemma iprod_map_ext {A} {B1 B2 : A  cofeT} (f1 f2 :  x, B1 x  B2 x) g :
  ( x, f1 x (g x)  f2 x (g x))  iprod_map f1 g  iprod_map f2 g.
Proof. done. Qed.
Lemma iprod_map_id {A} {B: A  cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
Proof. done. Qed.
Lemma iprod_map_compose {A} {B1 B2 B3 : A  cofeT}
    (f1 :  x, B1 x  B2 x) (f2 :  x, B2 x  B3 x) (g : iprod B1) :
  iprod_map (λ x, f2 x  f1 x) g = iprod_map f2 (iprod_map f1 g).
Proof. done. Qed.

Instance iprod_map_ne {A} {B1 B2 : A  cofeT} (f :  x, B1 x  B2 x) n :
  ( x, Proper (dist n ==> dist n) (f x)) 
  Proper (dist n ==> dist n) (iprod_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
283 284 285 286
Instance iprod_map_cmra_monotone {A} {B1 B2: A  cmraT} (f :  x, B1 x  B2 x) :
  ( x, CMRAMonotone (f x))  CMRAMonotone (iprod_map f).
Proof.
  split.
287
  - intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x.
288
    rewrite /iprod_map; apply includedN_preserving, Hf.
289
  - intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
290 291
Qed.

292 293 294 295 296 297
Definition iprodC_map {A} {B1 B2 : A  cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
Instance iprodC_map_ne {A} {B1 B2 : A  cofeT} n :
  Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
Proof. intros f1 f2 Hf g x; apply Hf. Qed.

298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
Program Definition iprodF {A} (Σ : A  iFunctor) : iFunctor := {|
  ifunctor_car B := iprodRA (λ x, Σ x B);
  ifunctor_map B1 B2 f := iprodC_map (λ x, ifunctor_map (Σ x) f);
|}.
Next Obligation.
  by intros A Σ B1 B2 n f f' ? g; apply iprodC_map_ne=>x; apply ifunctor_map_ne.
Qed.
Next Obligation.
  intros A Σ B g. rewrite /= -{2}(iprod_map_id g).
  apply iprod_map_ext=> x; apply ifunctor_map_id.
Qed.
Next Obligation.
  intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose.
  apply iprod_map_ext=> y; apply ifunctor_map_compose.
Qed.