auth.v 20.1 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.algebra Require Export frac agree local_updates.
3 4
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Import base_logic.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7 8 9 10 11 12 13 14 15
(** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
  of elements: the fractional authoritative `●{q} a`, the full authoritative
  `● a ≡ ●{1} a`, and the non-authoritative `◯ a`. Updates are only possible
  with the full authoritative element `● a`, while fractional authoritative
  elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`.
*)

Record auth (A : Type) :=
  Auth { auth_auth_proj : option (frac * agree A) ; auth_frag_proj : A }.
16
Add Printing Constructor auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Arguments Auth {_} _ _.
18 19
Arguments auth_auth_proj {_} _.
Arguments auth_frag_proj {_} _.
20
Instance: Params (@Auth) 1 := {}.
21 22 23
Instance: Params (@auth_auth_proj) 1 := {}.
Instance: Params (@auth_frag_proj) 1 := {}.

24 25 26
Definition auth_frag {A: ucmraT} (a: A) : auth A := Auth None a.
Definition auth_auth {A: ucmraT} (q: Qp) (a: A) : auth A :=
  Auth (Some (q, to_agree a)) ε.
27 28 29 30 31 32 33 34 35

Typeclasses Opaque auth_auth auth_frag.

Instance: Params (@auth_frag) 1 := {}.
Instance: Params (@auth_auth) 1 := {}.

Notation "◯ a" := (auth_frag a) (at level 20).
Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q }  a").
Notation "● a" := (auth_auth 1 a) (at level 20).
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37 38
(* Ofe *)
Section ofe.
39
Context {A : ofeT}.
40
Implicit Types a : option (frac * agree A).
41
Implicit Types b : A.
42
Implicit Types x y : auth A.
43 44

Instance auth_equiv : Equiv (auth A) := λ x y,
45
  auth_auth_proj x  auth_auth_proj y  auth_frag_proj x  auth_frag_proj y.
46
Instance auth_dist : Dist (auth A) := λ n x y,
47 48
  auth_auth_proj x {n} auth_auth_proj y 
  auth_frag_proj x {n} auth_frag_proj y.
Robbert Krebbers's avatar
Robbert Krebbers committed
49

50
Global Instance Auth_ne : NonExpansive2 (@Auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Proof. by split. Qed.
52 53
Global Instance Auth_proper : Proper (() ==> () ==> ()) (@Auth A).
Proof. by split. Qed.
54
Global Instance auth_auth_proj_ne: NonExpansive (@auth_auth_proj A).
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Proof. by destruct 1. Qed.
56
Global Instance auth_auth_proj_proper : Proper (() ==> ()) (@auth_auth_proj A).
57
Proof. by destruct 1. Qed.
58
Global Instance auth_frag_proj_ne : NonExpansive (@auth_frag_proj A).
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof. by destruct 1. Qed.
60
Global Instance auth_frag_proj_proper : Proper (() ==> ()) (@auth_frag_proj A).
61
Proof. by destruct 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62

63
Definition auth_ofe_mixin : OfeMixin (auth A).
64
Proof. by apply (iso_ofe_mixin (λ x, (auth_auth_proj x, auth_frag_proj x))). Qed.
65
Canonical Structure authO := OfeT (auth A) auth_ofe_mixin.
66

67 68 69
Global Instance Auth_discrete a b :
  Discrete a  Discrete b  Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
70
Global Instance auth_ofe_discrete : OfeDiscrete A  OfeDiscrete authO.
71
Proof. intros ? [??]; apply _. Qed.
72
End ofe.
73

74
Arguments authO : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
75

76
(* Camera *)
77
Section cmra.
78
Context {A : ucmraT}.
79 80
Implicit Types a b : A.
Implicit Types x y : auth A.
81

82 83 84 85 86 87 88 89 90 91 92 93 94 95
Global Instance auth_frag_ne: NonExpansive (@auth_frag A).
Proof. done. Qed.
Global Instance auth_frag_proper : Proper (() ==> ()) (@auth_frag A).
Proof. done. Qed.
Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
Proof. solve_proper. Qed.
Global Instance auth_auth_proper : Proper (() ==> () ==> ()) (@auth_auth A).
Proof. solve_proper. Qed.
Global Instance auth_auth_discrete q a :
  Discrete a  Discrete (ε : A)  Discrete ({q} a).
Proof. intros. apply Auth_discrete; apply _. Qed.
Global Instance auth_frag_discrete a : Discrete a  Discrete ( a).
Proof. intros. apply Auth_discrete; apply _. Qed.

96
Instance auth_valid : Valid (auth A) := λ x,
97 98 99 100
  match auth_auth_proj x with
  | Some (q, ag) =>
       q  ( n,  a, ag {n} to_agree a  auth_frag_proj x {n} a  {n} a)
  | None =>  auth_frag_proj x
101 102
  end.
Global Arguments auth_valid !_ /.
103
Instance auth_validN : ValidN (auth A) := λ n x,
104 105 106 107
  match auth_auth_proj x with
  | Some (q, ag) =>
      {n} q   a, ag {n} to_agree a  auth_frag_proj x {n} a  {n} a
  | None => {n} auth_frag_proj x
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  end.
109
Global Arguments auth_validN _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Instance auth_pcore : PCore (auth A) := λ x,
111
  Some (Auth (core (auth_auth_proj x)) (core (auth_frag_proj x))).
112
Instance auth_op : Op (auth A) := λ x y,
113
  Auth (auth_auth_proj x  auth_auth_proj y) (auth_frag_proj x  auth_frag_proj y).
114

115
Definition auth_valid_eq :
116 117 118
  valid = λ x, match auth_auth_proj x with
               | Some (q, ag) =>  q  ( n,  a, ag {n} to_agree a  auth_frag_proj x {n} a  {n} a)
               | None =>  auth_frag_proj x
119 120
               end := eq_refl _.
Definition auth_validN_eq :
121 122 123
  validN = λ n x, match auth_auth_proj x with
                  | Some (q, ag) => {n} q   a, ag {n} to_agree a  auth_frag_proj x {n} a  {n} a
                  | None => {n} auth_frag_proj x
124 125
                  end := eq_refl _.

126
Lemma auth_included (x y : auth A) :
127 128
  x  y 
  auth_auth_proj x  auth_auth_proj y  auth_frag_proj x  auth_frag_proj y.
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132
Proof.
  split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
  intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
133

134 135 136
Lemma auth_auth_proj_validN n x : {n} x  {n} auth_auth_proj x.
Proof. destruct x as [[[]|]]; [by intros (? & ? & -> & ?)|done]. Qed.
Lemma auth_frag_proj_validN n x : {n} x  {n} auth_frag_proj x.
137 138
Proof.
  rewrite auth_validN_eq.
139 140 141 142 143 144 145 146 147 148 149 150 151 152
  destruct x as [[[]|]]; [|done]. naive_solver eauto using cmra_validN_includedN.
Qed.
Lemma auth_auth_proj_valid x :  x   auth_auth_proj x.
Proof.
  destruct x as [[[]|]]; [intros [? H]|done]. split; [done|].
  intros n. by destruct (H n) as [? [-> [? ?]]].
Qed.
Lemma auth_frag_proj_valid x :  x   auth_frag_proj x.
Proof.
  destruct x as [[[]|]]; [intros [? H]|done]. apply cmra_valid_validN.
  intros n. destruct (H n) as [? [? [? ?]]].
  naive_solver eauto using cmra_validN_includedN.
Qed.

153
Lemma auth_frag_validN n a : {n} ( a)  {n} a.
154 155 156 157 158
Proof. done. Qed.
Lemma auth_auth_frac_validN n q a :
  {n} ({q} a)  {n} q  {n} a.
Proof.
  rewrite auth_validN_eq /=. apply and_iff_compat_l. split.
159
  - by intros [?[->%(inj to_agree) []]].
160 161 162 163 164 165 166 167 168 169 170
  - naive_solver eauto using ucmra_unit_leastN.
Qed.
Lemma auth_auth_validN n a : {n} a  {n} ( a).
Proof.
  rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.
Lemma auth_both_frac_validN n q a b :
  {n} ({q} a   b)  {n} q  b {n} a  {n} a.
Proof.
  rewrite auth_validN_eq /=. apply and_iff_compat_l.
  setoid_rewrite (left_id _ _ b). split.
171
  - by intros [?[->%(inj to_agree)]].
172 173 174 175 176 177 178
  - naive_solver.
Qed.
Lemma auth_both_validN n a b : {n} ( a   b)  b {n} a  {n} a.
Proof.
  rewrite auth_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
Qed.

179
Lemma auth_frag_valid a :  ( a)   a.
180
Proof. done. Qed.
181
Lemma auth_auth_frac_valid q a :  ({q} a)   q   a.
182 183 184
Proof.
  rewrite auth_valid_eq /=. apply and_iff_compat_l. split.
  - intros H'. apply cmra_valid_validN. intros n.
185
    by destruct (H' n) as [? [->%(inj to_agree) [??]]].
186 187
  - intros. exists a. split; [done|].
    split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
188
Qed.
189 190 191 192 193 194
Lemma auth_auth_valid a :  ( a)   a.
Proof. rewrite auth_auth_frac_valid frac_valid'. naive_solver. Qed.

(* The reverse direction of the two lemmas below only holds if the camera is
discrete. *)
Lemma auth_both_frac_valid_2 q a b :  q   a  b  a   ({q} a   b).
195 196 197 198
Proof.
  intros Val1 Val2 Incl. rewrite auth_valid_eq /=. split; [done|].
  intros n. exists a. split; [done|]. rewrite left_id.
  split; by [apply cmra_included_includedN|apply cmra_valid_validN].
199
Qed.
200 201
Lemma auth_both_valid_2 a b :  a  b  a   ( a   b).
Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
202

203
Lemma auth_valid_discrete `{!CmraDiscrete A} x :
204 205 206
   x  match auth_auth_proj x with
        | Some (q, ag) =>  q   a, ag  to_agree a  auth_frag_proj x  a   a
        | None =>  auth_frag_proj x
207 208
        end.
Proof.
209 210 211 212
  rewrite auth_valid_eq. destruct x as [[[??]|] ?]; simpl; [|done].
  setoid_rewrite <-cmra_discrete_included_iff.
  setoid_rewrite <-(discrete_iff _ a).
  setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using O.
213
Qed.
214
Lemma auth_both_frac_valid `{!CmraDiscrete A} q a b :
215
   ({q} a   b)   q  b  a   a.
216
Proof.
217 218
  rewrite auth_valid_discrete /=. apply and_iff_compat_l.
  setoid_rewrite (left_id _ _ b). split.
219
  - by intros [?[->%(inj to_agree)]].
220
  - naive_solver.
221
Qed.
222 223
Lemma auth_both_valid `{!CmraDiscrete A} a b :  ( a   b)  b  a   a.
Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
224

225
Lemma auth_cmra_mixin : CmraMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
226
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228
  apply cmra_total_mixin.
  - eauto.
229 230
  - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
  - by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
231
  - intros n [x a] [y b] [Hx Ha]; simpl in *. rewrite !auth_validN_eq.
232 233 234 235 236 237
    destruct Hx as [x y Hx|]; first destruct Hx as [? Hx];
      [destruct x,y|]; intros VI; ofe_subst; auto.
  - intros [[[]|] ]; rewrite /= ?auth_valid_eq ?auth_validN_eq /=
      ?cmra_valid_validN; naive_solver.
  - intros n [[[]|] ]; rewrite !auth_validN_eq /=;
      naive_solver eauto using dist_S, cmra_includedN_S, cmra_validN_S.
238 239
  - by split; simpl; rewrite assoc.
  - by split; simpl; rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
240 241
  - by split; simpl; rewrite ?cmra_core_l.
  - by split; simpl; rewrite ?cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  - intros ??; rewrite! auth_included; intros [??].
Ralf Jung's avatar
Ralf Jung committed
243
    by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
244
  - assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
245
    { intros n a b1 b2 <-; apply cmra_includedN_l. }
246 247 248 249 250 251
    intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; rewrite auth_validN_eq /=;
      try naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
    intros [? [a [Eq [? Valid]]]].
    assert (Eq': a1 {n} a2). { by apply agree_op_invN; rewrite Eq. }
    split; [naive_solver eauto using cmra_validN_op_l|].
    exists a. rewrite -Eq -Eq' agree_idemp. naive_solver.
252
  - intros n x y1 y2 ? [??]; simpl in *.
253 254 255 256
    destruct (cmra_extend n (auth_auth_proj x) (auth_auth_proj y1)
      (auth_auth_proj y2)) as (ea1&ea2&?&?&?); auto using auth_auth_proj_validN.
    destruct (cmra_extend n (auth_frag_proj x) (auth_frag_proj y1) (auth_frag_proj y2))
      as (b1&b2&?&?&?); auto using auth_frag_proj_validN.
257
    by exists (Auth ea1 b1), (Auth ea2 b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Qed.
259
Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
260

261
Global Instance auth_cmra_discrete : CmraDiscrete A  CmraDiscrete authR.
262 263
Proof.
  split; first apply _.
264
  intros [[[]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
265
  - setoid_rewrite <-cmra_discrete_included_iff.
266 267 268
    rewrite -cmra_discrete_valid_iff.
    setoid_rewrite <-cmra_discrete_valid_iff.
    setoid_rewrite <-(discrete_iff _ a). tauto.
269 270
  - by rewrite -cmra_discrete_valid_iff.
Qed.
271

Robbert Krebbers's avatar
Robbert Krebbers committed
272
Instance auth_empty : Unit (auth A) := Auth ε ε.
273
Lemma auth_ucmra_mixin : UcmraMixin (auth A).
274 275
Proof.
  split; simpl.
276
  - rewrite auth_valid_eq /=. apply ucmra_unit_valid.
277
  - by intros x; constructor; rewrite /= left_id.
278
  - do 2 constructor; [done| apply (core_id_core _)].
279
Qed.
280
Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin.
281

282 283
Global Instance auth_frag_core_id a : CoreId a  CoreId ( a).
Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
284

285
Lemma auth_frag_op a b :  (a  b) =  a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
Proof. done. Qed.
287 288
Lemma auth_frag_mono a b : a  b   a   b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
289

290
Global Instance auth_frag_sep_homomorphism :
291
  MonoidHomomorphism op op () (@auth_frag A).
292
Proof. by split; [split; try apply _|]. Qed.
293

294
Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b  {q} a   b.
295
Proof. by rewrite /op /auth_op /= left_id. Qed.
296 297 298
Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b   a   b.
Proof. by rewrite auth_both_frac_op. Qed.

299
Lemma auth_auth_frac_op p q a : {p + q} a  {p} a  {q} a.
300 301
Proof.
  intros; split; simpl; last by rewrite left_id.
302
  by rewrite -Some_op -pair_op agree_idemp.
303 304 305
Qed.
Lemma auth_auth_frac_op_invN n p a q b : {n} ({p} a  {q} b)  a {n} b.
Proof.
306
  rewrite /op /auth_op /= left_id -Some_op -pair_op auth_validN_eq /=.
307
  intros (?&?& Eq &?&?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
Qed.
Lemma auth_auth_frac_op_inv p a q b :  ({p} a  {q} b)  a  b.
Proof.
  intros ?. apply equiv_dist. intros n.
  by eapply auth_auth_frac_op_invN, cmra_valid_validN.
Qed.
Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b :
   ({p} a  {q} b)  a = b.
Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed.

(** Internalized properties *)
Lemma auth_equivI {M} x y :
  x  y @{uPredI M} auth_auth_proj x  auth_auth_proj y  auth_frag_proj x  auth_frag_proj y.
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} x :
   x @{uPredI M} match auth_auth_proj x with
                    | Some (q, ag) =>  q 
                       a, ag  to_agree a  ( b, a  auth_frag_proj x  b)   a
                    | None =>  auth_frag_proj x
                    end.
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
Lemma auth_frag_validI {M} (a : A):
   ( a) @{uPredI M}  a.
Proof. by rewrite auth_validI. Qed.

Lemma auth_both_validI {M} q (a b: A) :
   ({q} a   b) @{uPredI M}  q  ( c, a  b  c)   a.
Proof.
  rewrite -auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|].
  setoid_rewrite agree_equivI. iSplit.
  - iDestruct 1 as (a') "[#Eq [H V]]". iDestruct "H" as (b') "H".
    iRewrite -"Eq" in "H". iRewrite -"Eq" in "V". auto.
  - iDestruct 1 as "[H V]". iExists a. auto.
Qed.
Lemma auth_auth_validI {M} q (a b: A) :
   ({q} a) @{uPredI M}  q   a.
Proof.
  rewrite auth_validI /=. apply bi.and_proper; [done|].
  setoid_rewrite agree_equivI. iSplit.
  - iDestruct 1 as (a') "[Eq [_ V]]". by iRewrite -"Eq" in "V".
  - iIntros "V". iExists a. iSplit; [done|]. iSplit; [|done]. iExists a.
    by rewrite left_id.
Qed.
351

352 353
Lemma auth_update a b a' b' :
  (a,b) ~l~> (a',b')   a   b ~~>  a'   b'.
354
Proof.
355
  intros Hup; apply cmra_total_update.
356 357 358
  move=> n [[[??]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
  + exfalso. move : VL => /frac_valid'.
    rewrite frac_op'. by apply Qp_not_plus_q_ge_1.
359
  + split; [done|]. apply (inj to_agree) in Eq.
360 361 362 363
    move: Ha; rewrite !left_id -assoc => Ha.
    destruct (Hup n (Some (bf1  bf2))); [by rewrite Eq..|]. simpl in *.
    exists a'. split; [done|]. split; [|done]. exists bf2.
    by rewrite left_id -assoc.
Ralf Jung's avatar
Ralf Jung committed
364
Qed.
Ralf Jung's avatar
Ralf Jung committed
365

Robbert Krebbers's avatar
Robbert Krebbers committed
366
Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b')   a ~~>  a'   b'.
367
Proof. intros. rewrite -(right_id _ _ ( a)). by apply auth_update. Qed.
Ralf Jung's avatar
Ralf Jung committed
368

369 370 371 372 373 374
Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b')   a ~~>  a'.
Proof.
  intros. etrans; first exact: auth_update_alloc.
  exact: cmra_update_op_l.
Qed.

Ralf Jung's avatar
Ralf Jung committed
375 376 377 378 379 380 381
Lemma auth_update_core_id a b `{!CoreId b} :
  b  a   a ~~>  a   b.
Proof.
  intros Hincl. apply: auth_update_alloc.
  rewrite -(left_id ε _ b). apply: core_id_local_update. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
382
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε)   a   b ~~>  a'.
383
Proof. intros. rewrite -(right_id _ _ ( a')). by apply auth_update. Qed.
384 385 386 387 388

Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
  (b0, b1) ~l~> (b0', b1')  b0'  a'   a' 
  ( a   b0,  a   b1) ~l~> ( a'   b0',  a'   b1').
Proof.
389
  rewrite !local_update_unital=> Hup ? ? n /=.
390
    move=> [[[qc ac]|] bc] /auth_both_validN [Le Val] [] /=.
391
  - move => Ha. exfalso. move : Ha. rewrite right_id -Some_op -pair_op frac_op'.
392
    move => /Some_dist_inj [/= Eq _].
393 394 395 396 397 398
    apply (Qp_not_plus_q_ge_1 qc). by rewrite -Eq.
  - move => _. rewrite !left_id=> ?.
    destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.
    rewrite -!auth_both_op auth_validN_eq /=.
    split_and!; [done| |done]. exists a'.
    split_and!; [done|by apply cmra_included_includedN|by apply cmra_valid_validN].
399
Qed.
400 401
End cmra.

402
Arguments authR : clear implicits.
403
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
404

405
(* Proof mode class instances *)
406 407
Instance is_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
  IsOp a b1 b2  IsOp' ( a) ( b1) ( b2).
408
Proof. done. Qed.
409 410 411
Instance is_op_auth_auth_frac {A : ucmraT} (q q1 q2 : frac) (a : A) :
  IsOp q q1 q2  IsOp' ({q} a) ({q1} a) ({q2} a).
Proof. rewrite /IsOp' /IsOp => ->. by rewrite -auth_auth_frac_op. Qed.
412

Robbert Krebbers's avatar
Robbert Krebbers committed
413
(* Functor *)
414
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
415
  Auth (prod_map id (agree_map f) <$> auth_auth_proj x) (f (auth_frag_proj x)).
416
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
417
Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_id. Qed.
418 419
Lemma auth_map_compose {A B C} (f : A  B) (g : B  C) (x : auth A) :
  auth_map (g  f) x = auth_map g (auth_map f x).
420
Proof. destruct x as [[[]|] ];  by rewrite // /auth_map /= agree_map_compose. Qed.
421
Lemma auth_map_ext {A B : ofeT} (f g : A  B) `{!NonExpansive f} x :
422
  ( x, f x  g x)  auth_map f x  auth_map g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
423 424
Proof.
  constructor; simpl; auto.
425
  apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
Qed.
427
Instance auth_map_ne {A B : ofeT} (f : A -> B) `{Hf : !NonExpansive f} :
428
  NonExpansive (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
429
Proof.
430 431 432
  intros n [??] [??] [??]; split; simpl in *; [|by apply Hf].
  apply option_fmap_ne; [|done]=> x y ?. apply prod_map_ne; [done| |done].
  by apply agree_map_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
Qed.
434
Instance auth_map_cmra_morphism {A B : ucmraT} (f : A  B) :
435
  CmraMorphism f  CmraMorphism (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
436
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
  split; try apply _.
438 439 440 441 442
  - intros n [[[??]|] b]; rewrite !auth_validN_eq;
      [|naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN].
    intros [? [a' [Eq [? ?]]]]. split; [done|]. exists (f a').
    rewrite -agree_map_to_agree -Eq.
    naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
443 444
  - intros [??]. apply Some_proper; rewrite /auth_map /=.
    by f_equiv; rewrite /= cmra_morphism_core.
445
  - intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
446
Qed.
447 448 449
Definition authO_map {A B} (f : A -n> B) : authO A -n> authO B :=
  OfeMor (auth_map f).
Lemma authO_map_ne A B : NonExpansive (@authO_map A B).
450
Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
451
  apply agreeO_map_ne; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
452

453
Program Definition authRF (F : urFunctor) : rFunctor := {|
454
  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
455
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
456 457
|}.
Next Obligation.
458
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
459 460
Qed.
Next Obligation.
461
  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
462
  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
463 464
Qed.
Next Obligation.
465
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
466
  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
467 468 469 470 471
Qed.

Instance authRF_contractive F :
  urFunctorContractive F  rFunctorContractive (authRF F).
Proof.
472
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
473 474
Qed.

475
Program Definition authURF (F : urFunctor) : urFunctor := {|
476
  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
477
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
Ralf Jung's avatar
Ralf Jung committed
478
|}.
479
Next Obligation.
480
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
481
Qed.
Ralf Jung's avatar
Ralf Jung committed
482
Next Obligation.
483
  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
484
  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
Ralf Jung's avatar
Ralf Jung committed
485 486
Qed.
Next Obligation.
487
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
488
  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
Ralf Jung's avatar
Ralf Jung committed
489
Qed.
490

491 492
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
493
Proof.
494
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
495
Qed.