auth_excl.v 2.26 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
(** This file provides some utilities for the commonly used camera of
authoritative exclusive ownership, [auth (option (excl A))]. *)
3 4
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.base_logic.lib Require Import own.
6 7
Set Default Proof Using "Type".

8 9 10
Class auth_exclG (A : ofeT) (Σ : gFunctors) := AuthExclG {
  exclG_authG :> inG Σ (authR (optionUR (exclR A)));
}.
11

Robbert Krebbers's avatar
Robbert Krebbers committed
12
Definition auth_exclΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
13
  #[GFunctor (authRF (optionURF (exclRF F)))].
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15
Instance subG_auth_exclG (F : oFunctor) `{!oFunctorContractive F} {Σ} :
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  subG (auth_exclΣ F) Σ  auth_exclG (F (iPrePropO Σ) _) Σ.
17 18
Proof. solve_inG. Qed.

19 20
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
  Excl' a.
Jonas Kastberg's avatar
Jonas Kastberg committed
21
Instance: Params (@to_auth_excl) 1 := {}.
22 23 24 25 26 27 28 29 30 31 32

Section auth_excl_ofe.
  Context {A : ofeT}.

  Global Instance to_auth_excl_ne : NonExpansive (@to_auth_excl A).
  Proof. solve_proper. Qed.

  Global Instance to_auth_excl_proper :
    Proper (() ==> ()) (@to_auth_excl A).
  Proof. solve_proper. Qed.
End auth_excl_ofe.
33 34

Section auth_excl.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
35
  Context `{!auth_exclG A Σ}.
36 37 38 39 40 41
  Implicit Types x y : A.

  Lemma to_auth_excl_valid x y :
     ( to_auth_excl x   to_auth_excl y) - (x  y : iProp Σ).
  Proof.
    iIntros "Hvalid".
42 43 44
    iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
    iDestruct "Hle" as ([z|]) "Hy"; last first.
    - by rewrite bi.option_equivI /= excl_equivI.
45
    - iRewrite "Hy" in "Hvalid".
46
      by rewrite uPred.option_validI /= excl_validI /=.
47
  Qed.
48 49

  Lemma excl_eq γ x y :
50
    own γ ( to_auth_excl x) - own γ ( to_auth_excl y) - x  y.
51 52
  Proof.
    iIntros "Hauth Hfrag".
53 54
    iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
    iDestruct (to_auth_excl_valid with "Hvalid") as "$".
55
  Qed.
56

57
  Lemma excl_update γ x y z :
58 59
    own γ ( to_auth_excl y) - own γ ( to_auth_excl x) ==
    own γ ( to_auth_excl z)  own γ ( to_auth_excl z).
60 61 62 63 64 65
  Proof.
    iIntros "Hauth Hfrag".
    iDestruct (own_update_2 with "Hauth Hfrag") as "H".
    { eapply (auth_update _ _ (to_auth_excl z) (to_auth_excl z)).
      eapply option_local_update.
      eapply exclusive_local_update. done. }
66
    by rewrite own_op.
67
  Qed.
68
End auth_excl.