From 38f75bf33f4ce4c90247c0570e9bf1c125c811c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Nov 2019 21:47:39 +0100
Subject: [PATCH] Add `excl_auth` camera.

---
 _CoqProject                  |  1 +
 theories/algebra/excl_auth.v | 74 ++++++++++++++++++++++++++++++++++++
 2 files changed, 75 insertions(+)
 create mode 100644 theories/algebra/excl_auth.v

diff --git a/_CoqProject b/_CoqProject
index a4fe3512e..4a568257d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -18,6 +18,7 @@ theories/algebra/cmra_big_op.v
 theories/algebra/sts.v
 theories/algebra/auth.v
 theories/algebra/frac_auth.v
+theories/algebra/excl_auth.v
 theories/algebra/gmap.v
 theories/algebra/ofe.v
 theories/algebra/base.v
diff --git a/theories/algebra/excl_auth.v b/theories/algebra/excl_auth.v
new file mode 100644
index 000000000..25a06edf1
--- /dev/null
+++ b/theories/algebra/excl_auth.v
@@ -0,0 +1,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.
-- 
GitLab