auth_excl.v 2.25 KB
Newer Older
1
2
(** This file provides utility for defining and using
the commonly used ghost functor over authoritative exclusive ownership. *)
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
21
22
23
24
25
26
27
28
29
30
31
32
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
  Excl' a.
Instance: Params (@to_auth_excl) 1.

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.