From fa8d690852c8fbadc0d0f7258dca6f4e2b53b07b Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 23 Mar 2016 15:53:01 +0100 Subject: [PATCH] Disjointness of sets. --- theories/collections.v | 20 ++++++++++++++++---- theories/fin_collections.v | 4 ++-- theories/fin_map_dom.v | 12 +++++------- 3 files changed, 23 insertions(+), 13 deletions(-) diff --git a/theories/collections.v b/theories/collections.v index 4bcb31e..a4d6a23 100644 --- a/theories/collections.v +++ b/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. diff --git a/theories/fin_collections.v b/theories/fin_collections.v index 7967af1..21d8476 100644 --- a/theories/fin_collections.v +++ b/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. diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v index 9fcdae0..dec60be 100644 --- a/theories/fin_map_dom.v +++ b/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. -- GitLab