excl_auth.v 3.14 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
From iris.algebra Require Export auth excl updates.
From iris.algebra Require Import local_updates.
From iris.base_logic Require Import base_logic.
4
From iris Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6 7 8 9
(** Authoritative CMRA where the fragment is exclusively owned.
This is effectively a single "ghost variable" with two views, the frament [◯E a]
and the authority [●E a]. *)

Robbert Krebbers's avatar
Robbert Krebbers committed
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 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
Definition excl_authR (A : ofeT) : cmraT :=
  authR (optionUR (exclR A)).
Definition excl_authUR (A : ofeT) : ucmraT :=
  authUR (optionUR (exclR A)).

Definition excl_auth_auth {A : ofeT} (a : A) : excl_authR A :=
   (Some (Excl a)).
Definition excl_auth_frag {A : ofeT} (a : A) : excl_authR A :=
   (Some (Excl a)).

Typeclasses Opaque excl_auth_auth excl_auth_frag.

Instance: Params (@excl_auth_auth) 1 := {}.
Instance: Params (@excl_auth_frag) 2 := {}.

Notation "●E a" := (excl_auth_auth a) (at level 10).
Notation "◯E a" := (excl_auth_frag a) (at level 10).

Section excl_auth.
  Context {A : ofeT}.
  Implicit Types a b : A.

  Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth A).
  Proof. solve_proper. Qed.
  Global Instance excl_auth_auth_proper : Proper (() ==> ()) (@excl_auth_auth A).
  Proof. solve_proper. Qed.
  Global Instance excl_auth_frag_ne : NonExpansive (@excl_auth_frag A).
  Proof. solve_proper. Qed.
  Global Instance excl_auth_frag_proper : Proper (() ==> ()) (@excl_auth_frag A).
  Proof. solve_proper. Qed.

  Global Instance excl_auth_auth_discrete a : Discrete a  Discrete (E a).
  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
  Global Instance excl_auth_frag_discrete a : Discrete a  Discrete (E a).
  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.

  Lemma excl_auth_validN n a : {n} (E a  E a).
  Proof. by rewrite auth_both_validN. Qed.
  Lemma excl_auth_valid a :  (E a  E a).
  Proof. intros. by apply auth_both_valid_2. Qed.

  Lemma excl_auth_agreeN n a b : {n} (E a  E b)  a {n} b.
  Proof.
    rewrite auth_both_validN /= => -[Hincl Hvalid].
    move: Hincl=> /Some_includedN_exclusive /(_ I) ?. by apply (inj Excl).
  Qed.
  Lemma excl_auth_agree a b :  (E a  E b)  a  b.
  Proof.
    intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
  Qed.
  Lemma excl_auth_agreeL `{!LeibnizEquiv A} a b :  (E a  E b)  a = b.
  Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.

  Lemma excl_auth_agreeI {M} a b :  (E a  E b) @{uPredI M} (a  b).
  Proof.
    rewrite auth_both_validI bi.and_elim_r bi.and_elim_l.
    apply bi.exist_elim=> -[[c|]|];
67
      by rewrite option_equivI /= excl_equivI //= bi.False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71 72 73 74 75 76 77 78 79
  Qed.

  Lemma excl_auth_frag_validN_op_1_l n a b : {n} (E a  E b)  False.
  Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
  Lemma excl_auth_frag_valid_op_1_l a b :  (E a  E b)  False.
  Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.

  Lemma excl_auth_update a b a' : E a  E b ~~> E a'  E a'.
  Proof.
    intros. by apply auth_update, option_local_update, exclusive_local_update.
  Qed.
End excl_auth.