Merge branch 'robbert/map_singleton_subseteq' into 'master'

Add lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.

See merge request !308

CHANGELOG.md

@@ -132,6 +132,7 @@ API-breaking change is listed.
   `gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
   Iris.
 - Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
+- Add lemmas `map_singleton_subseteq_l` and `map_singleton_subseteq` for maps.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

theories/fin_maps.v

@@ -602,6 +602,17 @@ Lemma delete_singleton_ne {A} i j (x : A) :
   i ≠ j → delete i {[j := x]} =@{M A} {[j := x]}.
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
+Lemma map_singleton_subseteq_l {A} i (x : A) (m : M A) :
+  {[i := x]} ⊆ m ↔ m !! i = Some x.
+Proof.
+  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
+Qed.
+Lemma map_singleton_subseteq {A} i j (x y : A) :
+  {[i := x]} ⊆@{M A} {[j := y]} ↔ i = j ∧ x = y.
+Proof.
+  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
+Qed.
+
 (** ** Properties of the map operations *)
 Global Instance map_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).