Merge branch 'robbert/singleton_subseteq' into 'master'

Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`

See merge request !306

CHANGELOG.md

@@ -127,6 +127,11 @@ API-breaking change is listed.
   `or_intro_{l,r}'`.
 - Add `union_subseteq_l'`, `union_subseteq_r'` as transitive versions of
   `union_subseteq_l`, `union_subseteq_r` that can be more easily `apply`ed.
+- Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l`
+  and swap the equivalence to be consistent with Iris's `singleton_included_l`. Add
+  `gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
+  Iris.
+- Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -169,6 +174,8 @@ s/\bhcurry_uncurry\b/huncurry_curry/g
 s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
 # map_union_subseteq
 s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
+# singleton
+s/\bgmultiset_elem_of_singleton_subseteq\b/gmultiset_singleton_subseteq_l/g
 ' $(find theories -name "*.v")
 ```
 

theories/gmultiset.v

@@ -568,8 +568,17 @@ Section more_lemmas.
   Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
   Proof. multiset_solver. Qed.
 
-  Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[+ x +]} ⊆ X.
+  Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
   Proof. multiset_solver. Qed.
+  Lemma gmultiset_singleton_subseteq x y :
+    {[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
+  Proof.
+    split; [|multiset_solver].
+    (* FIXME: [multiset_solver] should solve this *)
+    intros Hxy. specialize (Hxy x).
+    rewrite multiplicity_singleton, multiplicity_singleton' in Hxy.
+    case_decide; [done|lia].
+  Qed.
 
   Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
   Proof. multiset_solver. Qed.

theories/sets.v

@@ -471,6 +471,11 @@ Section semi_set.
   Lemma not_elem_of_singleton_2 x y : x ≠ y → x ∉ ({[ y ]} : C).
   Proof. apply not_elem_of_singleton. Qed.
 
+  Lemma singleton_subseteq_l x X : {[ x ]} ⊆ X ↔ x ∈ X.
+  Proof. set_solver. Qed.
+  Lemma singleton_subseteq x y : {[ x ]} ⊆@{C} {[ y ]} ↔ x = y.
+  Proof. set_solver. Qed.
+
   (** Disjointness *)
   Lemma elem_of_disjoint X Y : X ## Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
   Proof. done. Qed.