excl_auth.v 2.93 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 51 52 53 54 55 56 57 58 59 60 61
From iris.algebra Require Export auth excl updates.
From iris.algebra Require Import local_updates.
From iris.base_logic Require Import base_logic.

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|]|];
62
      by rewrite option_equivI /= excl_equivI //= bi.False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65 66 67 68 69 70 71 72 73 74
  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.