Merge branch 'misc-lemma' into 'master'

Misc lemma for sets and `gset_to_gmap`

See merge request !553

CHANGELOG.md

@@ -8,6 +8,8 @@ API-breaking change is listed.
 - Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
   thereby make them consistent with the corresponding lemmas for sets.
 - Add support for compiling the packages with dune. (by Rodolphe Lepigre)
+- Add lemmas `gset_to_gmap_singleton`, `difference_union_intersection`,
+  `difference_union_intersection_L`. (by Léo Stefanesco)
 
 ## std++ 1.10.0 (2024-04-12)
 

stdpp/gmap.v

@@ -739,6 +739,12 @@ Section gset.
     rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
       elem_of_singleton; destruct (decide (i = j)); intuition.
   Qed.
+  Lemma gset_to_gmap_singleton {A} (x : A) i :
+    gset_to_gmap x {[ i ]} = {[i:=x]}.
+  Proof.
+    rewrite <-(right_id_L ∅ (∪) {[ i ]}), gset_to_gmap_union_singleton.
+    by rewrite gset_to_gmap_empty.
+  Qed.
   Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y :
     gset_to_gmap x (Y ∖ {[i]}) = delete i (gset_to_gmap x Y).
   Proof.

stdpp/sets.v

@@ -820,6 +820,8 @@ Section set.
     Qed.
     Lemma difference_difference_r X Y Z : X ∖ (Y ∖ Z) ≡ (X ∖ Y) ∪ (X ∩ Z).
     Proof. intros x. destruct (decide (x ∈ Z)); set_solver. Qed.
+    Lemma difference_union_intersection X Y : (X ∖ Y) ∪ (X ∩ Y) ≡ X.
+    Proof. rewrite union_intersection_l, difference_union. set_solver. Qed.
 
     Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ## Z.
     Proof.
@@ -855,6 +857,8 @@ Section set.
     Proof. unfold_leibniz. apply singleton_union_difference. Qed.
     Lemma difference_difference_r_L X Y Z : X ∖ (Y ∖ Z) = (X ∖ Y) ∪ (X ∩ Z).
     Proof. unfold_leibniz. apply difference_difference_r. Qed.
+    Lemma difference_union_intersection_L X Y : (X ∖ Y) ∪ (X ∩ Y) = X.
+    Proof. unfold_leibniz. apply difference_union_intersection. Qed.
 
   End dec_leibniz.
 End set.