cmra.v 36.5 KB
Newer Older
1
From iris.algebra Require Export cofe.
2

Ralf Jung's avatar
Ralf Jung committed
3
4
Class Core (A : Type) := core : A  A.
Instance: Params (@core) 2.
5
6
7
8
9
10
11
12
13

Class Op (A : Type) := op : A  A  A.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

Definition included `{Equiv A, Op A} (x y : A) :=  z, y  x  z.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
14
Hint Extern 0 (_  _) => reflexivity.
15
16
Instance: Params (@included) 3.

Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
Class ValidN (A : Type) := validN : nat  A  Prop.
Instance: Params (@validN) 3.
19
Notation "✓{ n } x" := (validN n x)
20
  (at level 20, n at next level, format "✓{ n }  x").
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22
23
Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.
24
Notation "✓ x" := (valid x) (at level 20) : C_scope.
25

26
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) :=  z, y {n} x  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Notation "x ≼{ n } y" := (includedN n x y)
28
  (at level 70, n at next level, format "x  ≼{ n }  y") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Instance: Params (@includedN) 4.
30
Hint Extern 0 (_ {_} _) => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
31

Robbert Krebbers's avatar
Robbert Krebbers committed
32
Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  (* setoids *)
34
  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
Ralf Jung's avatar
Ralf Jung committed
35
  mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
36
  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  (* valid *)
38
  mixin_cmra_valid_validN x :  x   n, {n} x;
39
  mixin_cmra_validN_S n x : {S n} x  {n} x;
Robbert Krebbers's avatar
Robbert Krebbers committed
40
  (* monoid *)
41
42
  mixin_cmra_assoc : Assoc () ();
  mixin_cmra_comm : Comm () ();
Ralf Jung's avatar
Ralf Jung committed
43
44
45
  mixin_cmra_core_l x : core x  x  x;
  mixin_cmra_core_idemp x : core (core x)  core x;
  mixin_cmra_core_preserving x y : x  y  core x  core y;
46
  mixin_cmra_validN_op_l n x y : {n} (x  y)  {n} x;
47
48
49
  mixin_cmra_extend n x y1 y2 :
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }
Robbert Krebbers's avatar
Robbert Krebbers committed
50
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
57
(** Bundeled version *)
Structure cmraT := CMRAT {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_dist : Dist cmra_car;
  cmra_compl : Compl cmra_car;
Ralf Jung's avatar
Ralf Jung committed
58
  cmra_core : Core cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  cmra_op : Op cmra_car;
60
  cmra_valid : Valid cmra_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  cmra_validN : ValidN cmra_car;
62
  cmra_cofe_mixin : CofeMixin cmra_car;
63
  cmra_mixin : CMRAMixin cmra_car
Robbert Krebbers's avatar
Robbert Krebbers committed
64
}.
65
Arguments CMRAT _ {_ _ _ _ _ _ _} _ _.
66
67
68
69
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_compl : simpl never.
Ralf Jung's avatar
Ralf Jung committed
70
Arguments cmra_core : simpl never.
71
Arguments cmra_op : simpl never.
72
Arguments cmra_valid : simpl never.
73
74
75
Arguments cmra_validN : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Add Printing Constructor cmraT.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
78
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
Canonical Structure cmra_cofeC.

81
82
83
84
85
86
(** Lifting properties from the mixin *)
Section cmra_mixin.
  Context {A : cmraT}.
  Implicit Types x y : A.
  Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
  Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
Ralf Jung's avatar
Ralf Jung committed
87
88
  Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
  Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed.
89
90
  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
91
92
  Lemma cmra_valid_validN x :  x   n, {n} x.
  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
93
94
  Lemma cmra_validN_S n x : {S n} x  {n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
95
96
97
98
  Global Instance cmra_assoc : Assoc () (@op A _).
  Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
  Global Instance cmra_comm : Comm () (@op A _).
  Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
Ralf Jung's avatar
Ralf Jung committed
99
100
101
102
103
104
  Lemma cmra_core_l x : core x  x  x.
  Proof. apply (mixin_cmra_core_l _ (cmra_mixin A)). Qed.
  Lemma cmra_core_idemp x : core (core x)  core x.
  Proof. apply (mixin_cmra_core_idemp _ (cmra_mixin A)). Qed.
  Lemma cmra_core_preserving x y : x  y  core x  core y.
  Proof. apply (mixin_cmra_core_preserving _ (cmra_mixin A)). Qed.
105
106
  Lemma cmra_validN_op_l n x y : {n} (x  y)  {n} x.
  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
107
  Lemma cmra_extend n x y1 y2 :
108
109
    {n} x  x {n} y1  y2 
    { z | x  z.1  z.2  z.1 {n} y1  z.2 {n} y2 }.
110
  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
111
112
End cmra_mixin.

Ralf Jung's avatar
Ralf Jung committed
113
(** * CMRAs with a unit element *)
114
(** We use the notation ∅ because for most instances (maps, sets, etc) the
Ralf Jung's avatar
Ralf Jung committed
115
`empty' element is the unit. *)
116
117
118
119
Record UCMRAMixin A `{Dist A, Equiv A, Op A, Valid A, Empty A} := {
  mixin_ucmra_unit_valid :  ;
  mixin_ucmra_unit_left_id : LeftId ()  ();
  mixin_ucmra_unit_timeless : Timeless 
120
}.
121
122
123
124
125
126
127
128
129
130
131
132
133
134
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

Structure ucmraT := UCMRAT {
  ucmra_car :> Type;
  ucmra_equiv : Equiv ucmra_car;
  ucmra_dist : Dist ucmra_car;
  ucmra_compl : Compl ucmra_car;
  ucmra_core : Core ucmra_car;
  ucmra_op : Op ucmra_car;
  ucmra_valid : Valid ucmra_car;
  ucmra_validN : ValidN ucmra_car;
  ucmra_empty : Empty ucmra_car;
  ucmra_cofe_mixin : CofeMixin ucmra_car;
  ucmra_cmra_mixin : CMRAMixin ucmra_car;
  ucmra_mixin : UCMRAMixin ucmra_car
}.
Arguments UCMRAT _ {_ _ _ _ _ _ _ _} _ _ _.
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Arguments ucmra_compl : simpl never.
Arguments ucmra_core : simpl never.
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
Arguments ucmra_cofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Existing Instances ucmra_empty.
Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
Canonical Structure ucmra_cofeC.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
  CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.

(** Lifting properties from the mixin *)
Section ucmra_mixin.
  Context {A : ucmraT}.
  Implicit Types x y : A.
  Lemma ucmra_unit_valid :  ( : A).
  Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
  Global Instance ucmra_unit_left_id : LeftId ()  (@op A _).
  Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
  Global Instance ucmra_unit_timeless : Timeless ( : A).
  Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
167

168
169
170
171
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : core x  x.
Arguments persistent {_} _ {_}.

172
(** * Discrete CMRAs *)
173
Class CMRADiscrete (A : cmraT) := {
174
175
176
177
  cmra_discrete :> Discrete A;
  cmra_discrete_valid (x : A) : {0} x   x
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
178
(** * Morphisms *)
179
Class CMRAMonotone {A B : cmraT} (f : A  B) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
182
  cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
  validN_preserving n x : {n} x  {n} f x;
  included_preserving x y : x  y  f x  f y
183
}.
184
185
Arguments validN_preserving {_ _} _ {_} _ _ _.
Arguments included_preserving {_ _} _ {_} _ _ _.
186

187
(** * Local updates *)
Ralf Jung's avatar
Ralf Jung committed
188
189
(** The idea is that lemams taking this class will usually have L explicit,
    and leave Lv implicit - it will be inferred by the typeclass machinery. *)
190
191
192
Class LocalUpdate {A : cmraT} (Lv : A  Prop) (L : A  A) := {
  local_update_ne n :> Proper (dist n ==> dist n) L;
  local_updateN n x y : Lv x  {n} (x  y)  L (x  y) {n} L x  y
193
194
195
}.
Arguments local_updateN {_ _} _ {_} _ _ _ _ _.

196
(** * Frame preserving updates *)
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  n z,
198
  {n} (x  z)   y, P y  {n} (y  z).
199
Instance: Params (@cmra_updateP) 1.
200
Infix "~~>:" := cmra_updateP (at level 70).
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Definition cmra_update {A : cmraT} (x y : A) :=  n z,
202
  {n} (x  z)  {n} (y  z).
203
Infix "~~>" := cmra_update (at level 70).
204
Instance: Params (@cmra_update) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
205

Robbert Krebbers's avatar
Robbert Krebbers committed
206
(** * Properties **)
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Section cmra.
208
Context {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Implicit Types x y z : A.
210
Implicit Types xs ys zs : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
211

212
(** ** Setoids *)
Ralf Jung's avatar
Ralf Jung committed
213
Global Instance cmra_core_proper : Proper (() ==> ()) (@core A _).
214
215
216
217
Proof. apply (ne_proper _). Qed.
Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
Proof.
  intros x1 x2 Hx y1 y2 Hy.
218
  by rewrite Hy (comm _ x1) Hx (comm _ y2).
219
220
221
222
223
224
225
226
227
Qed.
Global Instance ra_op_proper' : Proper (() ==> () ==> ()) (@op A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
Global Instance cmra_validN_proper : Proper (() ==> iff) (@validN A _ n) | 1.
Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.

Global Instance cmra_valid_proper : Proper (() ==> iff) (@valid A _).
228
229
230
231
Proof.
  intros x y Hxy; rewrite !cmra_valid_validN.
  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
Qed.
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
Global Instance cmra_includedN_ne n :
  Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_includedN_proper n :
  Proper (() ==> () ==> iff) (@includedN A _ _ n) | 1.
Proof.
  intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
  by rewrite (Hx n) (Hy n).
Qed.
Global Instance cmra_included_proper :
  Proper (() ==> () ==> iff) (@included A _ _) | 1.
Proof.
  intros x x' Hx y y' Hy.
  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
250
251
252
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto.
254
255
256
257
Qed.
Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  intros x1 x2 Hx P1 P2 HP; split=>Hup n z;
259
260
    [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto.
Qed.
261
262

(** ** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Lemma cmra_validN_le n n' x : {n} x  n'  n  {n'} x.
264
265
266
Proof. induction 2; eauto using cmra_validN_S. Qed.
Lemma cmra_valid_op_l x y :  (x  y)   x.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Lemma cmra_validN_op_r n x y : {n} (x  y)  {n} y.
268
Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
269
270
271
Lemma cmra_valid_op_r x y :  (x  y)   y.
Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.

Ralf Jung's avatar
Ralf Jung committed
272
273
274
275
276
277
278
279
280
(** ** Core *)
Lemma cmra_core_r x : x  core x  x.
Proof. by rewrite (comm _ x) cmra_core_l. Qed.
Lemma cmra_core_core x : core x  core x  core x.
Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
Lemma cmra_core_validN n x : {n} x  {n} core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_core_valid x :  x   core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
281
282
Global Instance cmra_core_persistent x : Persistent (core x).
Proof. apply cmra_core_idemp. Qed.
283
284

(** ** Order *)
Robbert Krebbers's avatar
Robbert Krebbers committed
285
286
Lemma cmra_included_includedN n x y : x  y  x {n} y.
Proof. intros [z ->]. by exists z. Qed.
287
288
289
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
290
  - by intros x; exists (core x); rewrite cmra_core_r.
291
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
292
    by rewrite assoc -Hy -Hz.
293
294
295
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
298
299
  split.
  - by intros x; exists (core x); rewrite cmra_core_r.
  - intros x y z [z1 Hy] [z2 Hz]; exists (z1  z2).
    by rewrite assoc -Hy -Hz.
300
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Lemma cmra_validN_includedN n x y : {n} y  x {n} y  {n} x.
302
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Lemma cmra_validN_included n x y : {n} y  x  y  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
305

Robbert Krebbers's avatar
Robbert Krebbers committed
306
Lemma cmra_includedN_S n x y : x {S n} y  x {n} y.
307
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Lemma cmra_includedN_le n n' x y : x {n} y  n'  n  x {n'} y.
309
310
311
312
313
314
315
Proof. induction 2; auto using cmra_includedN_S. Qed.

Lemma cmra_includedN_l n x y : x {n} x  y.
Proof. by exists y. Qed.
Lemma cmra_included_l x y : x  x  y.
Proof. by exists y. Qed.
Lemma cmra_includedN_r n x y : y {n} x  y.
316
Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
317
Lemma cmra_included_r x y : y  x  y.
318
Proof. rewrite (comm op); apply cmra_included_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
319

Ralf Jung's avatar
Ralf Jung committed
320
Lemma cmra_core_preservingN n x y : x {n} y  core x {n} core y.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
Proof.
  intros [z ->].
Ralf Jung's avatar
Ralf Jung committed
323
  apply cmra_included_includedN, cmra_core_preserving, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Qed.
Ralf Jung's avatar
Ralf Jung committed
325
326
Lemma cmra_included_core x : core x  x.
Proof. by exists x; rewrite cmra_core_l. Qed.
327
Lemma cmra_preservingN_l n x y z : x {n} y  z  x {n} z  y.
328
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
329
Lemma cmra_preserving_l x y z : x  y  z  x  z  y.
330
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
331
Lemma cmra_preservingN_r n x y z : x {n} y  x  z {n} y  z.
332
Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
333
Lemma cmra_preserving_r x y z : x  y  x  z  y  z.
334
Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.
335

Robbert Krebbers's avatar
Robbert Krebbers committed
336
Lemma cmra_included_dist_l n x1 x2 x1' :
337
  x1  x2  x1' {n} x1   x2', x1'  x2'  x2' {n} x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Proof.
339
340
  intros [z Hx2] Hx1; exists (x1'  z); split; auto using cmra_included_l.
  by rewrite Hx1 Hx2.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Qed.
342

Robbert Krebbers's avatar
Robbert Krebbers committed
343
(** ** Timeless *)
344
Lemma cmra_timeless_included_l x y : Timeless x  {0} y  x {0} y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
346
Proof.
  intros ?? [x' ?].
347
  destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
  by exists z'; rewrite Hy (timeless x z).
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Qed.
350
Lemma cmra_timeless_included_r n x y : Timeless y  x {0} y  x {n} y.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
352
Lemma cmra_op_timeless x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
353
   (x1  x2)  Timeless x1  Timeless x2  Timeless (x1  x2).
Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
Proof.
  intros ??? z Hz.
356
  destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
357
  { rewrite -?Hz. by apply cmra_valid_validN. }
Robbert Krebbers's avatar
Robbert Krebbers committed
358
  by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
359
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
360

361
362
363
364
365
366
367
368
(** ** Discrete *)
Lemma cmra_discrete_valid_iff `{CMRADiscrete A} n x :  x  {n} x.
Proof.
  split; first by rewrite cmra_valid_validN.
  eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x  y  x {n} y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
369
  split; first by apply cmra_included_includedN.
370
371
372
373
374
375
376
377
378
  intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A  Prop) :
  ( z,  (x  z)   y, P y   (y  z))  x ~~>: P.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
  ( z,  (x  z)   (y  z))  x ~~> y.
Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.

379
(** ** Local updates *)
380
381
Global Instance local_update_proper Lv (L : A  A) :
  LocalUpdate Lv L  Proper (() ==> ()) L.
382
383
Proof. intros; apply (ne_proper _). Qed.

384
385
Lemma local_update L `{!LocalUpdate Lv L} x y :
  Lv x   (x  y)  L (x  y)  L x  y.
386
387
388
Proof.
  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
Qed.
389
390

Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
391
Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
392

Ralf Jung's avatar
Ralf Jung committed
393
394
395
Global Instance local_update_id : LocalUpdate (λ _, True) (@id A).
Proof. split; auto with typeclass_instances. Qed.

396
(** ** Updates *)
397
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Robbert Krebbers's avatar
Robbert Krebbers committed
398
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
399
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =).
Robbert Krebbers's avatar
Robbert Krebbers committed
400
401
Proof.
  split.
402
  - by intros Hx z ?; exists y; split; [done|apply (Hx z)].
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Qed.
405
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
Proof. by intros ? n z ?; exists x. Qed.
407
Lemma cmra_updateP_compose (P Q : A  Prop) x :
408
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
409
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y).
411
Qed.
412
413
414
415
416
Lemma cmra_updateP_compose_l (Q : A  Prop) x y : x ~~> y  y ~~>: Q  x ~~>: Q.
Proof.
  rewrite cmra_update_updateP.
  intros; apply cmra_updateP_compose with (y =); intros; subst; auto.
Qed.
417
Lemma cmra_updateP_weaken (P Q : A  Prop) x : x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
418
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
419

420
Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
421
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2))  x1  x2 ~~>: Q.
422
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
424
425
  intros Hx1 Hx2 Hy n z ?.
  destruct (Hx1 n (x2  z)) as (y1&?&?); first by rewrite assoc.
  destruct (Hx2 n (y1  z)) as (y2&?&?);
426
427
    first by rewrite assoc (comm _ x2) -assoc.
  exists (y1  y2); split; last rewrite (comm _ y1) -assoc; auto.
428
Qed.
429
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
430
  x1 ~~>: P1  x2 ~~>: P2  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
431
Proof. eauto 10 using cmra_updateP_op. Qed.
432
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
433
Proof.
434
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
435
Qed.
436
437
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
439
End cmra.

440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
(** * Properties about CMRAs with a unit element **)
Section ucmra.
Context {A : ucmraT}.
Implicit Types x y z : A.

Global Instance ucmra_unit_inhabited : Inhabited A := populate .

Lemma ucmra_unit_validN n : {n} (:A).
Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
Lemma ucmra_unit_leastN n x :  {n} x.
Proof. by exists x; rewrite left_id. Qed.
Lemma ucmra_unit_least x :   x.
Proof. by exists x; rewrite left_id. Qed.
Global Instance ucmra_unit_right_id : RightId ()  (@op A _).
Proof. by intros x; rewrite (comm op) left_id. Qed.
Global Instance ucmra_unit_persistent : Persistent (:A).
Proof. by rewrite /Persistent -{2}(cmra_core_l ) right_id. Qed.
Lemma ucmra_core_unit : core (:A)  .
Proof. by rewrite -{2}(cmra_core_l ) right_id. Qed.

Lemma ucmra_update_unit x : x ~~> .
Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
Lemma ucmra_update_unit_alt y :  ~~> y   x, x ~~> y.
Proof. split; [intros; trans |]; auto using ucmra_update_unit. Qed.
End ucmra.

466
(** * Properties about monotone functions *)
467
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Proof. repeat split; by try apply _. Qed.
469
470
Instance cmra_monotone_compose {A B C : cmraT} (f : A  B) (g : B  C) :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
471
472
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
  - apply _. 
474
  - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
  - move=> x y Hxy /=. by apply included_preserving, included_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
Qed.
477

478
479
Section cmra_monotone.
  Context {A B : cmraT} (f : A  B) `{!CMRAMonotone f}.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
481
  Global Instance cmra_monotone_proper : Proper (() ==> ()) f := ne_proper _.
  Lemma includedN_preserving n x y : x {n} y  f x {n} f y.
482
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
    intros [z ->].
484
    apply cmra_included_includedN, (included_preserving f), cmra_included_l.
485
  Qed.
486
  Lemma valid_preserving x :  x   f x.
487
488
489
  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.

490
491
(** Functors *)
Structure rFunctor := RFunctor {
492
  rFunctor_car : cofeT  cofeT  cmraT;
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
  rFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
  rFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x  x;
  rFunctor_compose {A1 A2 A3 B1 B2 B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    rFunctor_map (fg, g'f') x  rFunctor_map (g,g') (rFunctor_map (f,f') x);
  rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CMRAMonotone (rFunctor_map fg) 
}.
Existing Instances rFunctor_ne rFunctor_mono.
Instance: Params (@rFunctor_map) 5.

Class rFunctorContractive (F : rFunctor) :=
  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).

Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
Coercion rFunctor_diag : rFunctor >-> Funclass.

Program Definition constRF (B : cmraT) : rFunctor :=
  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.

Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.

520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
Structure urFunctor := URFunctor {
  urFunctor_car : cofeT  cofeT  ucmraT;
  urFunctor_map {A1 A2 B1 B2} :
    ((A2 -n> A1) * (B1 -n> B2))  urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
  urFunctor_ne A1 A2 B1 B2 n :
    Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2);
  urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x  x;
  urFunctor_compose {A1 A2 A3 B1 B2 B3}
      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
    urFunctor_map (fg, g'f') x  urFunctor_map (g,g') (urFunctor_map (f,f') x);
  urFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
    CMRAMonotone (urFunctor_map fg) 
}.
Existing Instances urFunctor_ne urFunctor_mono.
Instance: Params (@urFunctor_map) 5.

Class urFunctorContractive (F : urFunctor) :=
  urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).

Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A.
Coercion urFunctor_diag : urFunctor >-> Funclass.

Program Definition constURF (B : ucmraT) : urFunctor :=
  {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.

Instance constURF_contractive B : urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.

549
550
551
552
553
554
555
556
557
558
559
560
561
(** * Transporting a CMRA equality *)
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
  eq_rect A id x _ H.

Section cmra_transport.
  Context {A B : cmraT} (H : A = B).
  Notation T := (cmra_transport H).
  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
  Proof. by intros ???; destruct H. Qed.
  Global Instance cmra_transport_proper : Proper (() ==> ()) T.
  Proof. by intros ???; destruct H. Qed.
  Lemma cmra_transport_op x y : T (x  y) = T x  T y.
  Proof. by destruct H. Qed.
Ralf Jung's avatar
Ralf Jung committed
562
  Lemma cmra_transport_core x : T (core x) = core (T x).
563
  Proof. by destruct H. Qed.
564
  Lemma cmra_transport_validN n x : {n} T x  {n} x.
565
  Proof. by destruct H. Qed.
566
  Lemma cmra_transport_valid x :  T x   x.
567
568
569
  Proof. by destruct H. Qed.
  Global Instance cmra_transport_timeless x : Timeless x  Timeless (T x).
  Proof. by destruct H. Qed.
570
571
  Global Instance cmra_transport_persistent x : Persistent x  Persistent (T x).
  Proof. by destruct H. Qed.
572
573
574
575
576
577
578
579
  Lemma cmra_transport_updateP (P : A  Prop) (Q : B  Prop) x :
    x ~~>: P  ( y, P y  Q (T y))  T x ~~>: Q.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma cmra_transport_updateP' (P : A  Prop) x :
    x ~~>: P  T x ~~>: λ y,  y', y = cmra_transport H y'  P y'.
  Proof. eauto using cmra_transport_updateP. Qed.
End cmra_transport.

580
581
(** * Instances *)
(** ** Discrete CMRA *)
582
Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := {
583
584
  (* setoids *)
  ra_op_ne (x : A) : Proper (() ==> ()) (op x);
585
586
  ra_core_ne : Proper (() ==> ()) core;
  ra_validN_ne : Proper (() ==> impl) valid;
587
  (* monoid *)
588
589
  ra_assoc : Assoc () ();
  ra_comm : Comm () ();
Ralf Jung's avatar
Ralf Jung committed
590
591
592
  ra_core_l x : core x  x  x;
  ra_core_idemp x : core (core x)  core x;
  ra_core_preserving x y : x  y  core x  core y;
Robbert Krebbers's avatar
Robbert Krebbers committed
593
  ra_valid_op_l x y :  (x  y)   x
594
595
}.

596
Section discrete.
597
598
599
  Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A ()}.
  Context (ra_mix : RAMixin A).
  Existing Instances discrete_dist discrete_compl.
600

601
  Instance discrete_validN : ValidN A := λ n x,  x.
602
  Definition discrete_cmra_mixin : CMRAMixin A.
603
  Proof.
604
    destruct ra_mix; split; try done.
605
    - intros x; split; first done. by move=> /(_ 0).
606
    - intros n x y1 y2 ??; by exists (y1,y2).
607
608
609
  Qed.
End discrete.

610
611
612
613
614
615
616
617
618
Notation discreteR A ra_mix :=
  (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
Notation discreteLeibnizR A ra_mix :=
  (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).

Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A,
  @Equivalence A ()} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
Proof. split. apply _. done. Qed.

619
620
621
(** ** CMRA for the unit type *)
Section unit.
  Instance unit_valid : Valid () := λ x, True.
622
  Instance unit_validN : ValidN () := λ n x, True.
Ralf Jung's avatar
Ralf Jung committed
623
  Instance unit_core : Core () := λ x, x.
624
  Instance unit_op : Op () := λ x y, ().
625
626

  Lemma unit_cmra_mixin : CMRAMixin ().
627
628
  Proof. by split; last exists ((),()). Qed.
  Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
629
630
631
632
633
634
635

  Instance unit_empty : Empty () := ().
  Lemma unit_ucmra_mixin : UCMRAMixin ().
  Proof. done. Qed.
  Canonical Structure unitUR : ucmraT :=
    UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin.

636
  Global Instance unit_cmra_discrete : CMRADiscrete unitR.
637
  Proof. done. Qed.
638
639
  Global Instance unit_persistent (x : ()) : Persistent x.
  Proof. done. Qed.
640
End unit.
641

642
(** ** Product *)
643
644
645
Section prod.
  Context {A B : cmraT}.
  Instance prod_op : Op (A * B) := λ x y, (x.1  y.1, x.2  y.2).
Ralf Jung's avatar
Ralf Jung committed
646
  Instance prod_core : Core (A * B) := λ x, (core (x.1), core (x.2)).
647
  Instance prod_valid : Valid (A * B) := λ x,  x.1   x.2.
648
  Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1  {n} x.2.
649

650
651
652
653
654
655
656
657
658
659
  Lemma prod_included (x y : A * B) : x  y  x.1  y.1  x.2  y.2.
  Proof.
    split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
  Qed.
  Lemma prod_includedN (x y : A * B) n : x {n} y  x.1 {n} y.1  x.2 {n} y.2.
  Proof.
    split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
  Qed.
660

661
662
663
  Definition prod_cmra_mixin : CMRAMixin (A * B).
  Proof.
    split; try apply _.
664
665
666
    - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
    - by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
    - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
667
668
669
    - intros x; split.
      + intros [??] n; split; by apply cmra_valid_validN.
      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
670
671
672
    - by intros n x [??]; split; apply cmra_validN_S.
    - by split; rewrite /= assoc.
    - by split; rewrite /= comm.
Ralf Jung's avatar
Ralf Jung committed
673
674
    - by split; rewrite /= cmra_core_l.
    - by split; rewrite /= cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
675
    - intros x y; rewrite !prod_included.
Ralf Jung's avatar
Ralf Jung committed
676
      by intros [??]; split; apply cmra_core_preserving.
677
    - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
678
679
680
681
    - intros n x y1 y2 [??] [??]; simpl in *.
      destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
      destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
      by exists ((z1.1,z2.1),(z1.2,z2.2)).
682
  Qed.
683
  Canonical Structure prodR :=
684
    CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
685

686
  Global Instance prod_cmra_discrete :
687
    CMRADiscrete A  CMRADiscrete B  CMRADiscrete prodR.
688
689
  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.

690
691
692
693
  Global Instance pair_persistent x y :
    Persistent x  Persistent y  Persistent (x,y).
  Proof. by split. Qed.

694
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
695
  Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
696
  Lemma prod_updateP P1 P2 (Q : A * B  Prop)  x :
697
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
698
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
699
700
    intros Hx1 Hx2 HP n z [??]; simpl in *.
    destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto.
701
702
    exists (a,b); repeat split; auto.
  Qed.
703
  Lemma prod_updateP' P1 P2 x :
704
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
705
  Proof. eauto using prod_updateP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
706
707
708
709
710
711
712
713
714
715

  Global Instance prod_local_update
      (LA : A  A) `{!LocalUpdate LvA LA} (LB : B  B) `{!LocalUpdate LvB LB} :
    LocalUpdate (λ x, LvA (x.1)  LvB (x.2)) (prod_map LA LB).
  Proof.
    constructor.
    - intros n x y [??]; constructor; simpl; by apply local_update_ne.
    - intros n ?? [??] [??];
        constructor; simpl in *; eapply local_updateN; eauto.
  Qed.
716
End prod.
Robbert Krebbers's avatar
Robbert Krebbers committed
717

718
Arguments prodR : clear implicits.
719

720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
Section prod_unit.
  Context {A B : ucmraT}.

  Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (, ).
  Lemma prod_ucmra_mixin : UCMRAMixin (A * B).
  Proof.
    split.
    - split; apply ucmra_unit_valid.
    - by split; rewrite /=left_id.
    - by intros ? [??]; split; apply (timeless _).
  Qed.
  Canonical Structure prodUR :=
    UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.

  Lemma pair_split (x : A) (y : B) : (x, y)  (x, )  (, y).
  Proof. constructor; by rewrite /= ?left_id ?right_id. Qed.
End prod_unit.

Arguments prodUR : clear implicits.

740
741
Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A  A') (g : B  B') :
  CMRAMonotone f  CMRAMonotone g  CMRAMonotone (prod_map f g).
742
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
743
  split; first apply _.
744
  - by intros n x [??]; split; simpl; apply validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
745
746
  - intros x y; rewrite !prod_included=> -[??] /=.
    by split; apply included_preserving.
747
Qed.
748

749
750
751
752
753
Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
  rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
  rFunctor_map A1 A2 B1 B2 fg :=
    prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
|}.
754
Next Obligation.
755
  intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply rFunctor_ne.
756
Qed.
757
758
759
760
761
Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
Next Obligation.
  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
  by rewrite !rFunctor_compose.
Qed.