iprod.v 14 KB
Newer Older
1 2
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.prelude Require Import finite.
4
Set Default Proof Using "Type".
5

6
(** * Indexed product *)
7
(** Need to put this in a definition to make canonical structures to work. *)
8 9
Definition iprod `{Finite A} (B : A  ofeT) :=  x, B x.
Definition iprod_insert `{Finite A} {B : A  ofeT}
10 11
    (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.
12
Instance: Params (@iprod_insert) 5.
13 14

Section iprod_cofe.
15
  Context `{Finite A} {B : A  ofeT}.
16 17
  Implicit Types x : A.
  Implicit Types f g : iprod B.
18

19
  Instance iprod_equiv : Equiv (iprod B) := λ f g,  x, f x  g x.
20
  Instance iprod_dist : Dist (iprod B) := λ n f g,  x, f x {n} g x.
21
  Definition iprod_ofe_mixin : OfeMixin (iprod B).
22 23
  Proof.
    split.
24
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
25
      intros Hfg k; apply equiv_dist; intros n; apply Hfg.
26
    - intros n; split.
27 28
      + by intros f x.
      + by intros f g ? x.
29
      + by intros f g h ?? x; trans (g x).
30
    - intros n f g Hfg x; apply dist_S, Hfg.
31
  Qed.
32 33 34 35 36 37 38 39 40 41 42 43
  Canonical Structure iprodC : ofeT := OfeT (iprod B) iprod_ofe_mixin.

  Program Definition iprod_chain (c : chain iprodC) (x : A) : chain (B x) :=
    {| chain_car n := c n x |}.
  Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
  Global Program Instance iprod_cofe `{ a, Cofe (B a)} : Cofe iprodC :=
    {| compl c x := compl (iprod_chain c x) |}.
  Next Obligation.
    intros ? n c x.
    rewrite (conv_compl n (iprod_chain c x)).
    apply (chain_cauchy c); lia.
  Qed.
44

45
  (** Properties of iprod_insert. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  Global Instance iprod_insert_ne n x :
47 48 49 50 51 52 53
    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 _.
54

55 56 57 58 59 60 61 62 63
  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.

64
  Global Instance iprod_lookup_timeless f x : Timeless f  Timeless (f x).
65
  Proof.
66
    intros ? y ?.
67
    cut (f  iprod_insert x y f).
68
    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
69 70
    apply (timeless _)=> x'; destruct (decide (x = x')) as [->|];
      by rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
71 72 73 74
  Qed.
  Global Instance iprod_insert_timeless f x y :
    Timeless f  Timeless y  Timeless (iprod_insert x y f).
  Proof.
75
    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
76
    - rewrite iprod_lookup_insert.
77
      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert.
78
    - rewrite iprod_lookup_insert_ne //.
79
      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne.
80
  Qed.
81 82
End iprod_cofe.

83
Arguments iprodC {_ _ _} _.
84 85

Section iprod_cmra.
86
  Context `{Finite A} {B : A  ucmraT}.
87
  Implicit Types f g : iprod B.
88

89
  Instance iprod_op : Op (iprod B) := λ f g x, f x  g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)).
91
  Instance iprod_valid : Valid (iprod B) := λ f,  x,  f x.
92
  Instance iprod_validN : ValidN (iprod B) := λ n f,  x, {n} f x.
93 94

  Definition iprod_lookup_op f g x : (f  g) x = f x  g x := eq_refl.
Ralf Jung's avatar
Ralf Jung committed
95
  Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
96

Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Lemma iprod_included_spec (f g : iprod B) : f  g   x, f x  g x.
98
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100
    split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
    intros [h ?]%finite_choice. by exists h.
101
  Qed.
102

103
  Lemma iprod_cmra_mixin : CMRAMixin (iprod B).
104
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
    apply cmra_total_mixin.
    - eauto.
107
    - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
Ralf Jung's avatar
Ralf Jung committed
108
    - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
109
    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
110 111 112
    - intros g; split.
      + intros Hg n i; apply cmra_valid_validN, Hg.
      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
113 114 115
    - 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.
Ralf Jung's avatar
Ralf Jung committed
116 117
    - by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
    - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
    - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
119
      by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
120
    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
121
    - intros n f f1 f2 Hf Hf12.
122 123 124 125 126 127
      destruct (finite_choice (λ x (yy : B x * B x),
        f x  yy.1  yy.2  yy.1 {n} f1 x  yy.2 {n} f2 x)) as [gg Hgg].
      { intros x. specialize (Hf12 x).
        destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
        exists (y1,y2); eauto. }
      exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
128
  Qed.
129
  Canonical Structure iprodR :=
130
    CMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin.
131 132 133 134 135

  Instance iprod_empty : Empty (iprod B) := λ x, .
  Definition iprod_lookup_empty x :  x =  := eq_refl.

  Lemma iprod_ucmra_mixin : UCMRAMixin (iprod B).
136
  Proof.
137 138
    split.
    - intros x; apply ucmra_unit_valid.
139
    - by intros f x; rewrite iprod_lookup_op left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
    - constructor=> x. apply persistent_core, _.
141
  Qed.
142
  Canonical Structure iprodUR :=
143
    UCMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
144

145 146 147 148
  Global Instance iprod_empty_timeless :
    ( i, Timeless ( : B i))  Timeless ( : iprod B).
  Proof. intros ? f Hf x. by apply: timeless. Qed.

149
  (** Internalized properties *)
150
  Lemma iprod_equivI {M} g1 g2 : g1  g2 ⊣⊢ ( i, g1 i  g2 i : uPred M).
151
  Proof. by uPred.unseal. Qed.
152
  Lemma iprod_validI {M} g :  g ⊣⊢ ( i,  g i : uPred M).
153
  Proof. by uPred.unseal. Qed.
154

155
  (** Properties of iprod_insert. *)
156 157 158 159
  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
160 161
    intros Hy1 HP; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
162 163 164 165 166 167 168 169 170 171 172 173 174 175
    { 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.
176
    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
177
  Qed.
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
End iprod_cmra.

Arguments iprodR {_ _ _} _.
Arguments iprodUR {_ _ _} _.

Definition iprod_singleton `{Finite A} {B : A  ucmraT} 
  (x : A) (y : B x) : iprod B := iprod_insert x y .
Instance: Params (@iprod_singleton) 5.

Section iprod_singleton.
  Context `{Finite A} {B : A  ucmraT}.
  Implicit Types x : A.

  Global Instance iprod_singleton_ne n x :
    Proper (dist n ==> dist n) (iprod_singleton x : B x  _).
  Proof. intros y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
  Global Instance iprod_singleton_proper x :
    Proper (() ==> ()) (iprod_singleton x) := ne_proper _.
196

197 198 199 200 201
  Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y.
  Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
  Lemma iprod_lookup_singleton_ne x x' (y : B x) :
    x  x'  (iprod_singleton x y) x' = .
  Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
202

203
  Global Instance iprod_singleton_timeless x (y : B x) :
204 205
    ( i, Timeless ( : B i))   Timeless y  Timeless (iprod_singleton x y).
  Proof. apply _. Qed.
206 207

  Lemma iprod_singleton_validN n x (y : B x) : {n} iprod_singleton x y  {n} y.
208
  Proof.
209 210 211
    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
    move=>Hx x'; destruct (decide (x = x')) as [->|];
      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
212
    by apply ucmra_unit_validN.
213 214
  Qed.

Ralf Jung's avatar
Ralf Jung committed
215 216
  Lemma iprod_core_singleton x (y : B x) :
    core (iprod_singleton x y)  iprod_singleton x (core y).
217
  Proof.
218 219
    move=>x'; destruct (decide (x = x')) as [->|];
      by rewrite iprod_lookup_core ?iprod_lookup_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
220
      ?iprod_lookup_singleton_ne // (persistent_core ∅).
221 222
  Qed.

223 224
  Global Instance iprod_singleton_persistent x (y : B x) :
    Persistent y  Persistent (iprod_singleton x y).
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  Proof. by rewrite !persistent_total iprod_core_singleton=> ->. Qed.
226

227 228 229 230
  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 [->|].
231 232
    - by rewrite iprod_lookup_op !iprod_lookup_singleton.
    - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
233 234 235 236 237 238 239 240
  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 
241
    iprod_singleton x y1 ~~>: λ g,  y2, g = iprod_singleton x y2  P y2.
242
  Proof. eauto using iprod_singleton_updateP. Qed.
243
  Lemma iprod_singleton_update x (y1 y2 : B x) :
244 245
    y1 ~~> y2  iprod_singleton x y1 ~~> iprod_singleton x y2.
  Proof. eauto using iprod_insert_update. Qed.
246 247

  Lemma iprod_singleton_updateP_empty x (P : B x  Prop) (Q : iprod B  Prop) :
248
     ~~>: P  ( y2, P y2  Q (iprod_singleton x y2))   ~~>: Q.
249
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
    intros Hx HQ; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
252 253
    exists (iprod_singleton x y2); split; [by apply HQ|].
    intros x'; destruct (decide (x' = x)) as [->|].
254 255
    - by rewrite iprod_lookup_op iprod_lookup_singleton.
    - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
256
  Qed.
257 258 259
  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.
260 261 262 263 264 265 266
  Lemma iprod_singleton_update_empty x (y : B x) :
     ~~> y   ~~> iprod_singleton x y.
  Proof.
    rewrite !cmra_update_updateP;
      eauto using iprod_singleton_updateP_empty with subst.
  Qed.
End iprod_singleton.
267

268
(** * Functor *)
269
Definition iprod_map `{Finite A} {B1 B2 : A  ofeT} (f :  x, B1 x  B2 x)
270 271
  (g : iprod B1) : iprod B2 := λ x, f _ (g x).

272
Lemma iprod_map_ext `{Finite A} {B1 B2 : A  ofeT} (f1 f2 :  x, B1 x  B2 x) (g : iprod B1) :
273 274
  ( x, f1 x (g x)  f2 x (g x))  iprod_map f1 g  iprod_map f2 g.
Proof. done. Qed.
275
Lemma iprod_map_id `{Finite A} {B : A  ofeT} (g : iprod B) :
276
  iprod_map (λ _, id) g = g.
277
Proof. done. Qed.
278
Lemma iprod_map_compose `{Finite A} {B1 B2 B3 : A  ofeT}
279 280 281 282
    (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.

283
Instance iprod_map_ne `{Finite A} {B1 B2 : A  ofeT} (f :  x, B1 x  B2 x) n :
284 285 286
  ( 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.
287 288
Instance iprod_map_cmra_monotone
    `{Finite A} {B1 B2 : A  ucmraT} (f :  x, B1 x  B2 x) :
289 290
  ( x, CMRAMonotone (f x))  CMRAMonotone (iprod_map f).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  split; first apply _.
292
  - intros n g Hg x; rewrite /iprod_map; apply (cmra_monotone_validN (f _)), Hg.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
  - intros g1 g2; rewrite !iprod_included_spec=> Hf x.
294
    rewrite /iprod_map; apply (cmra_monotone _), Hf.
295 296
Qed.

297
Definition iprodC_map `{Finite A} {B1 B2 : A  ofeT}
298
    (f : iprod (λ x, B1 x -n> B2 x)) :
299
  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
300
Instance iprodC_map_ne `{Finite A} {B1 B2 : A  ofeT} n :
301
  Proper (dist n ==> dist n) (@iprodC_map A _ _ B1 B2).
302 303
Proof. intros f1 f2 Hf g x; apply Hf. Qed.

304
Program Definition iprodCF `{Finite C} (F : C  cFunctor) : cFunctor := {|
305 306
  cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
  cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
307
|}.
308
Next Obligation.
309
  intros C ?? F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
310
Qed.
311
Next Obligation.
312
  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
313
  apply iprod_map_ext=> y; apply cFunctor_id.
314 315
Qed.
Next Obligation.
316
  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
317 318
  apply iprod_map_ext=>y; apply cFunctor_compose.
Qed.
319
Instance iprodCF_contractive `{Finite C} (F : C  cFunctor) :
320 321 322 323 324 325
  ( c, cFunctorContractive (F c))  cFunctorContractive (iprodCF F).
Proof.
  intros ? A1 A2 B1 B2 n ?? g.
  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
Qed.

326 327 328
Program Definition iprodURF `{Finite C} (F : C  urFunctor) : urFunctor := {|
  urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
  urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
329
|}.
330
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
  intros C ?? F A1 A2 B1 B2 n ?? g.
332
  by apply iprodC_map_ne=>?; apply urFunctor_ne.
333
Qed.
334
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
336
  apply iprod_map_ext=> y; apply urFunctor_id.
337 338
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
340
  apply iprod_map_ext=>y; apply urFunctor_compose.
341
Qed.
342 343
Instance iprodURF_contractive `{Finite C} (F : C  urFunctor) :
  ( c, urFunctorContractive (F c))  urFunctorContractive (iprodURF F).
344 345
Proof.
  intros ? A1 A2 B1 B2 n ?? g.
346
  by apply iprodC_map_ne=>c; apply urFunctor_contractive.
347
Qed.