some inversion lemmas for map domain

theories/fin_map_dom.v

@@ -163,6 +163,63 @@ Proof.
   - by rewrite dom_empty.
   - simpl. by rewrite dom_insert, IH.
 Qed.
+
+Lemma dom_singleton_inv {A} (m : M A) i :
+  dom D m ≡ {[i]} → ∃ v, m = {[i := v]}.
+Proof.
+  intros Hdom.
+  destruct (m !! i) as [x|] eqn:He.
+  - exists x. rewrite <-insert_empty.
+    apply map_eq; intros i'.
+    destruct (decide (i = i')); subst.
+    + rewrite lookup_insert; eauto.
+    + rewrite lookup_insert_ne; eauto.
+      rewrite lookup_empty.
+      apply not_elem_of_dom. set_solver.
+  - cut (i ∈ dom D m); [|set_solver].
+    rewrite elem_of_dom, He.
+    intros [x ?]; congruence.
+Qed.
+Lemma dom_union_inv `{!RelDecision (∈@{D})} {A} (m : M A) (d1 d2 : D) :
+  d1 ## d2 →
+  dom D m ≡ d1 ∪ d2 →
+  ∃ m1 m2, m1 ##ₘ m2 ∧ m = m1 ∪ m2 ∧ dom D m1 ≡ d1 ∧ dom D m2 ≡ d2.
+Proof.
+  revert d1 d2.
+  induction m as [|a v m Hfresh IHm] using map_ind; intros d1 d2 Hdisj Hdom.
+  - eexists ∅, ∅.
+    rewrite dom_empty in Hdom. rewrite dom_empty.
+    rewrite (left_id_L _ (∪)).
+    split_and!; [ apply map_disjoint_empty_l | set_solver .. ].
+  - rename select (m !! a = None) into Hma.
+    apply not_elem_of_dom in Hma.
+    rewrite dom_insert in Hdom.
+    assert (a ∈ d1 ∨ a ∈ d2) as [Ha|Ha] by set_solver.
+    (* With ssreflect we could do a [wlog] proof here since these
+       two cases are symmetric. *)
+    + rewrite (union_difference_singleton a d1) in Hdom by done.
+      rewrite <-(assoc _) in Hdom.
+      apply union_cancel_l in Hdom; [ | set_solver.. ].
+      apply IHm in Hdom as (m1&m2&Hmdisj&Hmunion&Hm1&Hm2); [ | set_solver ].
+      exists (<[a:=v]> m1), m2.
+      split_and!; auto.
+      * apply map_disjoint_dom. rewrite dom_insert. set_solver -Hma Hmdisj Hmunion.
+      * rewrite <-insert_union_l. congruence.
+      * rewrite dom_insert, Hm1. by rewrite <-union_difference_singleton.
+    + rewrite (union_difference_singleton a d2) in Hdom by done.
+      rewrite (assoc _), (comm _ d1), <-(assoc _) in Hdom.
+      apply union_cancel_l in Hdom; [ | set_solver.. ].
+      apply IHm in Hdom as (m1&m2&Hmdisj&Hmunion&Hm1&Hm2); [ | set_solver ].
+      exists m1, (<[a:=v]>m2).
+      split_and!; auto.
+      * apply map_disjoint_dom. rewrite dom_insert. set_solver -Hma Hmdisj Hmunion.
+      * rewrite !insert_union_singleton_l, (assoc _).
+        rewrite (map_union_comm m1), <-(assoc _), Hmunion; [done|].
+        apply map_disjoint_dom. rewrite dom_singleton, Hm1.
+        set_solver -Hma Hmdisj Hmunion.
+      * rewrite dom_insert, Hm2. by rewrite <-union_difference_singleton.
+Qed.
+
 (** If [D] has Leibniz equality, we can show an even stronger result.  This is a
 common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
 (and thus also [gset K], the usual domain) but the value type [A] does not. *)
@@ -207,6 +264,14 @@ Section leibniz.
   Lemma dom_list_to_map_L {A} (l : list (K * A)) :
     dom D (list_to_map l : M A) = list_to_set l.*1.
   Proof. unfold_leibniz. apply dom_list_to_map. Qed.
+  Lemma dom_singleton_inv_L {A} (m : M A) i :
+  dom D m = {[i]} → ∃ v, m = {[i := v]}.
+  Proof. unfold_leibniz. apply dom_singleton_inv. Qed.
+  Lemma dom_union_inv_L `{!RelDecision (∈@{D})} {A} (m : M A) (d1 d2 : D) :
+    d1 ## d2 →
+    dom D m = d1 ∪ d2 →
+    ∃ m1 m2, m1 ##ₘ m2 ∧ m = m1 ∪ m2 ∧ dom D m1 = d1 ∧ dom D m2 = d2.
+  Proof. unfold_leibniz. apply dom_union_inv. Qed.
 End leibniz.
 
 (** * Set solver instances *)

theories/sets.v

@@ -779,6 +779,8 @@ Section set.
       intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
       destruct (decide (x ∈ X)); intuition.
     Qed.
+    Lemma union_difference_singleton x Y : x ∈ Y → Y ≡ {[x]} ∪ Y ∖ {[x]}.
+    Proof. intros ?. apply union_difference. set_solver. Qed.
     Lemma difference_union X Y : X ∖ Y ∪ Y ≡ X ∪ Y.
     Proof.
       intros x. rewrite !elem_of_union; rewrite elem_of_difference.
@@ -800,6 +802,8 @@ Section set.
     Context `{!LeibnizEquiv C}.
     Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
     Proof. unfold_leibniz. apply union_difference. Qed.
+    Lemma union_difference_singleton_L x Y : x ∈ Y → Y = {[x]} ∪ Y ∖ {[x]}.
+    Proof. unfold_leibniz. apply union_difference_singleton. Qed.
     Lemma difference_union_L X Y : X ∖ Y ∪ Y = X ∪ Y.
     Proof. unfold_leibniz. apply difference_union. Qed.
     Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅.