auth.v 2.18 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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
47
48
49
50
Require Export excl.
Local Arguments disjoint _ _ !_ !_ /.
Local Arguments included _ _ !_ !_ /.

Record auth (A : Type) : Type := Auth { authorative : excl A ; own : A }.
Arguments Auth {_} _ _.
Arguments authorative {_} _.
Arguments own {_} _.
Notation "∘ x" := (Auth ExclUnit x) (at level 20).
Notation "∙ x" := (Auth (Excl x) ) (at level 20).

Instance auth_valid `{Valid A, Included A} : Valid (auth A) := λ x,
  valid (authorative x)  excl_above (own x) (authorative x).
Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
  authorative x  authorative y  own x  own y.
Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
  Auth (unit (authorative x)) (unit (own x)).
Instance auth_op `{Op A} : Op (auth A) := λ x y,
  Auth (authorative x  authorative y) (own x  own y).
Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
  Auth (authorative x  authorative y) (own x  own y).
Instance auth_included `{Equiv A, Included A} : Included (auth A) := λ x y,
  authorative x  authorative y  own x  own y.

Instance auth_ra `{RA A} : RA (auth A).
Proof.
  split.
  * split.
    + by intros ?; split.
    + by intros ?? [??]; split.
    + intros ??? [??] [??]; split; etransitivity; eauto.
  * by intros x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
  * by intros y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
  * by intros y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
  * by intros x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
      split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
  * by intros x y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
  * by split; simpl; rewrite (associative _).
  * by split; simpl; rewrite (commutative _).
  * by split; simpl; rewrite ?(ra_unit_l _).
  * by split; simpl; rewrite ?(ra_unit_idempotent _).
  * split; simpl; auto using ra_unit_weaken.
  * intros ?? [??]; split; [by apply ra_valid_op_l with (authorative y)|].
    by apply excl_above_weaken with (own x  own y)
      (authorative x  authorative y); try apply ra_included_l.
  * split; simpl; apply ra_included_l.
  * by intros ?? [??]; split; simpl; apply ra_op_difference.
Qed.
Lemma auth_frag_op `{RA A} a b : (a  b)  a  b.
Proof. done. Qed.