From 953a4d67e31dd31569da512f8584b7894da5cbc6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 11:43:43 +0200
Subject: [PATCH] Some properties about set disjointness.

---
 theories/collections.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index da7ecf8d..16a265da 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -41,6 +41,25 @@ Section simple_collection.
   Lemma elem_of_disjoint X Y : X ⊥ Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
   Proof. done. Qed.
 
+  Global Instance disjoint_sym : Symmetric (@disjoint C _).
+  Proof. intros ??. rewrite !elem_of_disjoint; naive_solver. Qed.
+  Lemma disjoint_empty_l Y : ∅ ⊥ Y.
+  Proof. rewrite elem_of_disjoint; intros x; by rewrite elem_of_empty. Qed.
+  Lemma disjoint_empty_r X : X ⊥ ∅.
+  Proof. rewrite (symmetry_iff _); apply disjoint_empty_l. Qed.
+  Lemma disjoint_singleton_l x Y : {[ x ]} ⊥ Y ↔ x ∉ Y.
+  Proof.
+    rewrite elem_of_disjoint; setoid_rewrite elem_of_singleton; naive_solver.
+  Qed.
+  Lemma disjoint_singleton_r y X : X ⊥ {[ y ]} ↔ y ∉ X.
+  Proof. rewrite (symmetry_iff (⊥)). apply disjoint_singleton_l. Qed.
+  Lemma disjoint_union_l X1 X2 Y : X1 ∪ X2 ⊥ Y ↔ X1 ⊥ Y ∧ X2 ⊥ Y.
+  Proof.
+    rewrite !elem_of_disjoint; setoid_rewrite elem_of_union; naive_solver.
+  Qed.
+  Lemma disjoint_union_r X Y1 Y2 : X ⊥ Y1 ∪ Y2 ↔ X ⊥ Y1 ∧ X ⊥ Y2.
+  Proof. rewrite !(symmetry_iff (⊥) X). apply disjoint_union_l. Qed.
+
   Lemma collection_positive_l X Y : X ∪ Y ≡ ∅ → X ≡ ∅.
   Proof.
     rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
-- 
GitLab