From e13d484b0f8c9d2209ce60e24d809b8e863056fb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jan 2016 17:23:53 +0100
Subject: [PATCH] Properties about excl.

---
 modures/excl.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/modures/excl.v b/modures/excl.v
index fcac96f26..e1a73d31f 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -66,6 +66,10 @@ Proof.
 Qed.
 Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
 
+Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
+Proof. by inversion_clear 1. Qed.
+Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
+Proof. by inversion_clear 1. Qed.
 Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
@@ -133,6 +137,11 @@ Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
 Proof. by destruct y. Qed.
 Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
 Proof. by destruct x. Qed.
+Lemma Excl_includedN n x y : ✓{n} y → Excl x ≼{n} y ↔ y ={n}= Excl x.
+Proof.
+  intros Hvalid; split; [destruct n as [|n]; [done|]|by intros ->].
+  by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
+Qed.
 
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.
-- 
GitLab