iprod.v 12.4 KB
Newer Older
1 2 3
Require Export algebra.cmra.
Require Import algebra.functor.

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 33 34 35 36 37 38 39 40 41 42 43 44 45
  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.
    * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
      intros Hfg k; apply equiv_dist; intros n; apply Hfg.
    * intros n; split.
      + by intros f x.
      + by intros f g ? x.
      + by intros f g h ?? x; transitivity (g x).
    * intros n f g Hfg x; apply dist_S, Hfg.
    * intros c n x.
      rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n).
      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 52 53 54
      ( x : A, Timeless ( : B x))  Timeless ( : iprod B).
    Proof. intros ? f Hf x. by apply (timeless _). Qed.
  End empty.

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

58 59 60 61 62 63 64 65
  Global Instance iprod_insert_ne x n :
    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 81 82
    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
    by apply (timeless _)=>x'; destruct (decide (x = x')) as [->|];
      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 88 89 90 91
    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
    * rewrite iprod_lookup_insert.
      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert.
    * rewrite iprod_lookup_insert_ne //.
      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

97 98 99 100 101
  Global Instance iprod_singleton_ne x n :
    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 121 122
  Instance iprod_op : Op (iprod B) := λ f g x, f x  g x.
  Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
  Instance iprod_validN : ValidN (iprod B) := λ n f,  x, {n} (f x).
  Instance iprod_minus : Minus (iprod B) := λ f g x, f x  g x.
123 124 125

  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.
126
  Definition iprod_lookup_minus f g x : (f  g) x = f x  g x := eq_refl.
127

128 129 130 131 132 133 134
  Lemma iprod_includedN_spec (f g : iprod B) n : 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.
135

136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168
  Definition iprod_cmra_mixin : CMRAMixin (iprod B).
  Proof.
    split.
    * 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).
    * intros n f Hf x; apply cmra_validN_S, Hf.
    * by intros f1 f2 f3 x; rewrite iprod_lookup_op associative.
    * by intros f1 f2 x; rewrite iprod_lookup_op commutative.
    * by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
    * by intros f x; rewrite iprod_lookup_unit cmra_unit_idempotent.
    * intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x.
      by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf.
    * intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
    * intros n f1 f2; rewrite iprod_includedN_spec=> Hf x.
      by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
  Qed.
  Definition iprod_cmra_extend_mixin : CMRAExtendMixin (iprod B).
  Proof.
    intros n f f1 f2 Hf Hf12.
    set (g x := cmra_extend_op 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_ands; intros x; apply (proj2_sig (g x)).
  Qed.
  Canonical Structure iprodRA : cmraT :=
    CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin.
  Global Instance iprod_cmra_identity `{ x, Empty (B x)} :
    ( x, CMRAIdentity (B x))  CMRAIdentity iprodRA.
  Proof.
    intros ?; split.
    * intros n x; apply cmra_empty_valid.
    * by intros f x; rewrite iprod_lookup_op left_id.
169
    * by apply _.
170 171
  Qed.

172
  (** Properties of iprod_insert. *)
173
  Context `{ x x' : A, Decision (x = x')}.
174

175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
  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.
    intros Hy1 HP gf n Hg. destruct (Hy1 (gf x) n) as (y2&?&?).
    { 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.
194
    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
195 196
  Qed.

197
  (** Properties of iprod_singleton. *)
198
  Context `{ x, Empty (B x),  x, CMRAIdentity (B x)}.
199

200 201
  Lemma iprod_singleton_validN n x (y : B x) :
    {n} (iprod_singleton x y)  {n} y.
202
  Proof.
203 204 205 206
    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
    move=>Hx x'; destruct (decide (x = x')) as [->|];
      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
    by apply cmra_empty_valid.
207 208
  Qed.

209 210 211
  Lemma iprod_unit_singleton x (y : B x) :
    unit (iprod_singleton x y)  iprod_singleton x (unit y).
  Proof.
212 213 214
    by move=>x'; destruct (decide (x = x')) as [->|];
      rewrite iprod_lookup_unit ?iprod_lookup_singleton
      ?iprod_lookup_singleton_ne // cmra_unit_empty.
215 216
  Qed.

217 218 219 220 221 222 223 224 225 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 [->|].
    * by rewrite iprod_lookup_op !iprod_lookup_singleton.
    * by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
  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 
231
    iprod_singleton x y1 ~~>: λ g,  y2, g = iprod_singleton x y2  P y2.
232
  Proof. eauto using iprod_singleton_updateP. Qed.
233 234 235
  Lemma iprod_singleton_update x y1 y2 :
    y1 ~~> y2  iprod_singleton x y1 ~~> iprod_singleton x y2.
  Proof. eauto using iprod_insert_update. Qed.
236 237

  Lemma iprod_singleton_updateP_empty x (P : B x  Prop) (Q : iprod B  Prop) :
238
     ~~>: P  ( y2, P y2  Q (iprod_singleton x y2))   ~~>: Q.
239
  Proof.
240 241 242 243 244
    intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?); first apply Hg.
    exists (iprod_singleton x y2); split; [by apply HQ|].
    intros x'; destruct (decide (x' = x)) as [->|].
    * by rewrite iprod_lookup_op iprod_lookup_singleton.
    * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
245
  Qed.
246 247 248
  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.
249 250 251 252
End iprod_cmra.

Arguments iprodRA {_} _.

253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
(** * 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.
271 272 273 274 275 276 277 278 279
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.
  * intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x.
    rewrite /iprod_map; apply includedN_preserving, Hf.
  * intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
Qed.

280 281 282 283 284 285
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.

286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
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.