frac_auth.v 5.25 KB
Newer Older
1
From iris.algebra Require Export frac auth updates local_updates.
2
From iris.algebra Require Import proofmode_classes.
3

4 5 6 7 8 9 10
(** Authoritative CMRA where the NON-authoritative parts can be fractional.
  This CMRA allows the original non-authoritative element `◯ a` to be split into
  fractional parts `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as
  using the original `◯ a`. Currently, however, this CMRA hides the ability to
  split the authoritative part into fractions.
*)

11 12 13 14 15 16 17 18 19 20 21 22
Definition frac_authR (A : cmraT) : cmraT :=
  authR (optionUR (prodR fracR A)).
Definition frac_authUR (A : cmraT) : ucmraT :=
  authUR (optionUR (prodR fracR A)).

Definition frac_auth_auth {A : cmraT} (x : A) : frac_authR A :=
   (Some (1%Qp,x)).
Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A :=
   (Some (q,x)).

Typeclasses Opaque frac_auth_auth frac_auth_frag.

23 24
Instance: Params (@frac_auth_auth) 1 := {}.
Instance: Params (@frac_auth_frag) 2 := {}.
25

Ralf Jung's avatar
Ralf Jung committed
26 27 28
Notation "●F a" := (frac_auth_auth a) (at level 10).
Notation "◯F{ q } a" := (frac_auth_frag q a) (at level 10, format "◯F{ q }  a").
Notation "◯F a" := (frac_auth_frag 1 a) (at level 10).
29 30 31 32 33 34 35 36 37 38 39 40 41 42

Section frac_auth.
  Context {A : cmraT}.
  Implicit Types a b : A.

  Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth A).
  Proof. solve_proper. Qed.
  Global Instance frac_auth_auth_proper : Proper (() ==> ()) (@frac_auth_auth A).
  Proof. solve_proper. Qed.
  Global Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag A q).
  Proof. solve_proper. Qed.
  Global Instance frac_auth_frag_proper q : Proper (() ==> ()) (@frac_auth_frag A q).
  Proof. solve_proper. Qed.

Ralf Jung's avatar
Ralf Jung committed
43
  Global Instance frac_auth_auth_discrete a : Discrete a  Discrete (F a).
44
  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
45
  Global Instance frac_auth_frag_discrete q a : Discrete a  Discrete (F{q} a).
46
  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
47

Ralf Jung's avatar
Ralf Jung committed
48
  Lemma frac_auth_validN n a : {n} a  {n} (F a  F a).
49
  Proof. by rewrite auth_both_validN. Qed.
Ralf Jung's avatar
Ralf Jung committed
50
  Lemma frac_auth_valid a :  a   (F a  F a).
51
  Proof. intros. by apply auth_both_valid_2. Qed.
52

Ralf Jung's avatar
Ralf Jung committed
53
  Lemma frac_auth_agreeN n a b : {n} (F a  F b)  a {n} b.
54
  Proof.
55
    rewrite auth_both_validN /= => -[Hincl Hvalid].
56 57
    by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
  Qed.
Ralf Jung's avatar
Ralf Jung committed
58
  Lemma frac_auth_agree a b :  (F a  F b)  a  b.
59 60 61
  Proof.
    intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
62
  Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b :  (F a  F b)  a = b.
63 64
  Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.

Ralf Jung's avatar
Ralf Jung committed
65
  Lemma frac_auth_includedN n q a b : {n} (F a  F{q} b)  Some b {n} Some a.
66
  Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
67
  Lemma frac_auth_included `{CmraDiscrete A} q a b :
Ralf Jung's avatar
Ralf Jung committed
68
     (F a  F{q} b)  Some b  Some a.
69
  Proof. by rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _]. Qed.
70
  Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
Ralf Jung's avatar
Ralf Jung committed
71
    {n} (F a  F{q} b)  b {n} a.
72
  Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
73
  Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b :
Ralf Jung's avatar
Ralf Jung committed
74
     (F a  F{q} b)  b  a.
75 76
  Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.

Ralf Jung's avatar
Ralf Jung committed
77
  Lemma frac_auth_auth_validN n a : {n} (F a)  {n} a.
78
  Proof.
79 80
    rewrite auth_auth_frac_validN Some_validN. split.
    by intros [?[]]. intros. by split.
81
  Qed.
Ralf Jung's avatar
Ralf Jung committed
82
  Lemma frac_auth_auth_valid a :  (F a)   a.
83 84
  Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.

Ralf Jung's avatar
Ralf Jung committed
85
  Lemma frac_auth_frag_validN n q a : {n} (F{q} a)  {n} q  {n} a.
86
  Proof. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
87
  Lemma frac_auth_frag_valid q a :  (F{q} a)   q   a.
88 89
  Proof. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
90
  Lemma frac_auth_frag_op q1 q2 a1 a2 : F{q1+q2} (a1  a2)  F{q1} a1  F{q2} a2.
91 92
  Proof. done. Qed.

Ralf Jung's avatar
Ralf Jung committed
93
  Lemma frac_auth_frag_validN_op_1_l n q a b : {n} (F{1} a  F{q} b)  False.
94
  Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
Ralf Jung's avatar
Ralf Jung committed
95
  Lemma frac_auth_frag_valid_op_1_l q a b :  (F{1} a  F{q} b)  False.
96
  Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
97

98
  Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
Ralf Jung's avatar
Ralf Jung committed
99
    IsOp q q1 q2  IsOp a a1 a2  IsOp' (F{q} a) (F{q1} a1) (F{q2} a2).
100 101
  Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
102
  Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a  : A) :
Ralf Jung's avatar
Ralf Jung committed
103
    CoreId a  IsOp q q1 q2  IsOp' (F{q} a) (F{q1} a) (F{q2} a).
104
  Proof.
105
    rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
106
    by rewrite -frac_auth_frag_op -core_id_dup.
107 108 109
  Qed.

  Lemma frac_auth_update q a b a' b' :
Ralf Jung's avatar
Ralf Jung committed
110
    (a,b) ~l~> (a',b')  F a  F{q} b ~~> F a'  F{q} b'.
111 112 113
  Proof.
    intros. by apply auth_update, option_local_update, prod_local_update_2.
  Qed.
114

Ralf Jung's avatar
Ralf Jung committed
115
  Lemma frac_auth_update_1 a b a' :  a'  F a  F b ~~> F a'  F a'.
116 117 118
  Proof.
    intros. by apply auth_update, option_local_update, exclusive_local_update.
  Qed.
119
End frac_auth.