iprod.v 12.2 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 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
  Instance iprod_equiv : Equiv (iprod B) := λ f g,  x, f x  g x.
  Instance iprod_dist : Dist (iprod B) := λ n f g,  x, f x ={n}= g x.
  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.
    * by intros f g x.
    * 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.

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

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

59 60 61 62 63 64 65 66
  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 _.
67

68 69 70 71 72 73 74 75 76
  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.

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

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

98 99 100 101 102
  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 _.
103

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

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

Arguments iprodC {_} _.

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

120 121 122 123
  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.
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

129 130 131 132 133 134 135
  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.
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 169 170 171 172 173
  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).
    * by intros f x.
    * 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.
    * by intros f Hf x; apply (timeless _).
  Qed.

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

177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
  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.
196
    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
197 198
  Qed.

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

202 203
  Lemma iprod_singleton_validN n x (y : B x) :
    {n} (iprod_singleton x y)  {n} y.
204
  Proof.
205 206 207 208
    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.
209 210
  Qed.

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

219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
  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 
    iprod_singleton x y1 ~~>: λ g',  y2, g' = iprod_singleton x y2  P y2.
  Proof. eauto using iprod_singleton_updateP. Qed.
235 236 237
  Lemma iprod_singleton_update x y1 y2 :
    y1 ~~> y2  iprod_singleton x y1 ~~> iprod_singleton x y2.
  Proof. eauto using iprod_insert_update. Qed.
238 239

  Lemma iprod_singleton_updateP_empty x (P : B x  Prop) (Q : iprod B  Prop) :
240
     ~~>: P  ( y2, P y2  Q (iprod_singleton x y2))   ~~>: Q.
241
  Proof.
242 243 244 245 246
    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.
247 248 249 250 251
  Qed.
End iprod_cmra.

Arguments iprodRA {_} _.

252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
(** * 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.
270 271 272 273 274 275 276 277 278
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.

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

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