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