Disjointness of sets.

theories/collections.v

@@ -5,9 +5,11 @@ importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 From stdpp Require Export base tactics orders.
 
+Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y,
+  ∀ x, x ∈ X → x ∈ Y → False.
 Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
-Typeclasses Opaque collection_subseteq.
+Typeclasses Opaque collection_disjoint collection_subseteq.
 
 (** * Basic theorems *)
 Section simple_collection.
@@ -36,6 +38,9 @@ Section simple_collection.
   Proof. firstorder. Qed.
   Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
   Proof. firstorder. Qed.
+  Lemma elem_of_disjoint X Y : X ⊥ Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
+  Proof. done. Qed.
+
   Lemma collection_positive_l X Y : X ∪ Y ≡ ∅ → X ≡ ∅.
   Proof.
     rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
@@ -52,11 +57,14 @@ Section simple_collection.
     - intros ??. rewrite elem_of_singleton. by intros ->.
     - intros Ex. by apply (Ex x), elem_of_singleton.
   Qed.
+
   Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)).
   Proof. by repeat intro; subst. Qed.
   Global Instance elem_of_proper :
-    Proper ((=) ==> (≡) ==> iff) ((∈) : A → C → Prop) | 5.
+    Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5.
   Proof. intros ???; subst. firstorder. Qed.
+  Global Instance disjoint_prope : Proper ((≡) ==> (≡) ==> iff) (@disjoint C _).
+  Proof. intros ??????. by rewrite !elem_of_disjoint; setoid_subst. Qed.
   Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
     split.
@@ -196,6 +204,10 @@ Section set_unfold_simple.
     constructor. rewrite subset_spec, elem_of_subseteq, elem_of_equiv.
     repeat f_equiv; naive_solver.
   Qed.
+  Global Instance set_unfold_disjoint (P Q : A → Prop) :
+    (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
+    SetUnfold (X ⊥ Y) (∀ x, P x → Q x → False).
+  Proof. constructor. rewrite elem_of_disjoint. naive_solver. Qed.
 
   Context `{!LeibnizEquiv C}.
   Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
@@ -387,7 +399,7 @@ Section collection.
   Proof. set_solver. Qed.
   Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
   Proof. set_solver. Qed.
-  Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y.
+  Lemma disjoint_union_difference X Y : X ⊥ Y → (X ∪ Y) ∖ X ≡ Y.
   Proof. set_solver. Qed.
 
   Section leibniz.
@@ -407,7 +419,7 @@ Section collection.
     Lemma difference_intersection_distr_l_L X Y Z :
       (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
     Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
-    Lemma disjoint_union_difference_L X Y : X ∩ Y = ∅ → (X ∪ Y) ∖ X = Y.
+    Lemma disjoint_union_difference_L X Y : X ⊥ Y → (X ∪ Y) ∖ X = Y.
     Proof. unfold_leibniz. apply disjoint_union_difference. Qed.
   End leibniz.
 

theories/fin_collections.v

@@ -92,9 +92,9 @@ Proof.
   - rewrite elem_of_singleton. eauto using size_singleton_inv.
   - set_solver.
 Qed.
-Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
+Lemma size_union X Y : X ⊥ Y → size (X ∪ Y) = size X + size Y.
 Proof.
-  intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
+  intros. unfold size, collection_size. simpl. rewrite <-app_length.
   apply Permutation_length, NoDup_Permutation.
   - apply NoDup_elements.
   - apply NoDup_app; repeat split; try apply NoDup_elements.

theories/fin_map_dom.v

@@ -74,15 +74,14 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
 Lemma delete_insert_dom {A} (m : M A) i x :
   i ∉ dom D m → delete i (<[i:=x]>m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
-Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ₘ m2 ↔ dom D m1 ∩ dom D m2 ≡ ∅.
+Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ₘ m2 ↔ dom D m1 ⊥ dom D m2.
 Proof.
-  rewrite map_disjoint_spec, elem_of_equiv_empty.
-  setoid_rewrite elem_of_intersection.
+  rewrite map_disjoint_spec, elem_of_disjoint.
   setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
 Qed.
-Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → dom D m1 ∩ dom D m2 ≡ ∅.
+Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → dom D m1 ⊥ dom D m2.
 Proof. apply map_disjoint_dom. Qed.
-Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ∩ dom D m2 ≡ ∅ → m1 ⊥ₘ m2.
+Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ⊥ dom D m2 → m1 ⊥ₘ m2.
 Proof. apply map_disjoint_dom. Qed.
 Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2.
 Proof.
@@ -90,8 +89,7 @@ Proof.
   unfold is_Some. setoid_rewrite lookup_union_Some_raw.
   destruct (m1 !! i); naive_solver.
 Qed.
-Lemma dom_intersection {A} (m1 m2 : M A) :
-  dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2.
+Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2.
 Proof.
   apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.