auth.v 2.5 KB
Newer Older
1
Require Export iris.excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
Local Arguments disjoint _ _ !_ !_ /.

Robbert Krebbers's avatar
Robbert Krebbers committed
4
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Arguments Auth {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Arguments authoritative {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
Arguments own {_} _.
Notation "∘ x" := (Auth ExclUnit x) (at level 20).
Notation "∙ x" := (Auth (Excl x) ) (at level 20).

11
Instance auth_empty `{Empty A} : Empty (auth A) := Auth  .
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
  valid (authoritative x)  excl_above (own x) (authoritative x).
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  authoritative x  authoritative y  own x  own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  Auth (unit (authoritative x)) (unit (own x)).
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Instance auth_op `{Op A} : Op (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  Auth (authoritative x  authoritative y) (own x  own y).
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
  Auth (authoritative x  authoritative y) (own x  own y).
Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
  x  y  authoritative x  authoritative y  own x  own y.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

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 split; simpl; rewrite (associative _).
  * by split; simpl; rewrite (commutative _).
  * by split; simpl; rewrite ?(ra_unit_l _).
  * by split; simpl; rewrite ?(ra_unit_idempotent _).
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
47
  * intros ??; rewrite! auth_included; intros [??].
    by split; simpl; apply ra_unit_preserving.
  * intros ?? [??]; split; [by apply ra_valid_op_l with (authoritative y)|].
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    by apply excl_above_weaken with (own x  own y)
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
      (authoritative x  authoritative y); try apply ra_included_l.
  * by intros ??; rewrite auth_included;
      intros [??]; split; simpl; apply ra_op_minus.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Qed.
53
54
Instance auth_ra_empty `{RA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
Proof. split. done. by intros x; constructor; simpl; rewrite (left_id _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Lemma auth_frag_op `{RA A} a b : (a  b)  a  b.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Proof. done. Qed.