Merge branch 'robbert/set_unfold_dom' into 'master'

Add `set_solver` support for `dom`

Closes #53

See merge request !116

CHANGELOG.md

@@ -13,6 +13,8 @@ API-breaking change is listed.
   https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
 - Add type class `TopSet` for sets with a `⊤` element. Provide instances for
   `boolset`, `propset`, and `coPset`.
+- Add `set_solver` support for `dom`.
+
 
 ## std++ 1.2.1 (released 2019-08-29)
 

tests/fin_maps.v

-From stdpp Require Import fin_maps.
+From stdpp Require Import fin_maps fin_map_dom.
 
 Section map_disjoint.
   Context `{FinMap K M}.
@@ -11,3 +11,14 @@ Section map_disjoint.
     m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ##ₘ <[i:=x]> m1 ∧ m1 !! i = None.
   Proof. intros. solve_map_disjoint. Qed.
 End map_disjoint.
+
+Section map_dom.
+  Context `{FinMapDom K M D}.
+
+  Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
+    {[i; j]} ⊆ dom D (<[i:=x]> (<[j:=y]> (∅ : M A))).
+  Proof. set_solver. Qed.
+
+  Lemma set_solver_dom_disjoint {A} (X : D) : dom D (∅ : M A) ## X.
+  Proof. set_solver. Qed.
+End map_dom.

theories/fin_map_dom.v

@@ -142,32 +142,84 @@ Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
   Proper ((≡@{M A}) ==> (=)) (dom D) | 0.
 Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
 
-Context `{!LeibnizEquiv D}.
-Lemma dom_map_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
-  (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
-  dom D (filter P m) = X.
-Proof. unfold_leibniz. apply dom_map_filter. Qed.
-Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
-Proof. unfold_leibniz; apply dom_empty. Qed.
-Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
-Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
-Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
-Proof. unfold_leibniz; apply dom_alter. Qed.
-Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
-Proof. unfold_leibniz; apply dom_insert. Qed.
-Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
-Proof. unfold_leibniz; apply dom_singleton. Qed.
-Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}.
-Proof. unfold_leibniz; apply dom_delete. Qed.
-Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1 ∪ m2) = dom D m1 ∪ dom D m2.
-Proof. unfold_leibniz; apply dom_union. Qed.
-Lemma dom_intersection_L {A} (m1 m2 : M A) :
-  dom D (m1 ∩ m2) = dom D m1 ∩ dom D m2.
-Proof. unfold_leibniz; apply dom_intersection. Qed.
-Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2.
-Proof. unfold_leibniz; apply dom_difference. Qed.
-Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
-Proof. unfold_leibniz; apply dom_fmap. Qed.
+Section leibniz.
+  Context `{!LeibnizEquiv D}.
+  Lemma dom_map_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
+    (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
+    dom D (filter P m) = X.
+  Proof. unfold_leibniz. apply dom_map_filter. Qed.
+  Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
+  Proof. unfold_leibniz; apply dom_empty. Qed.
+  Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
+  Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
+  Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
+  Proof. unfold_leibniz; apply dom_alter. Qed.
+  Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
+  Proof. unfold_leibniz; apply dom_insert. Qed.
+  Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
+  Proof. unfold_leibniz; apply dom_singleton. Qed.
+  Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}.
+  Proof. unfold_leibniz; apply dom_delete. Qed.
+  Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1 ∪ m2) = dom D m1 ∪ dom D m2.
+  Proof. unfold_leibniz; apply dom_union. Qed.
+  Lemma dom_intersection_L {A} (m1 m2 : M A) :
+    dom D (m1 ∩ m2) = dom D m1 ∩ dom D m2.
+  Proof. unfold_leibniz; apply dom_intersection. Qed.
+  Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2.
+  Proof. unfold_leibniz; apply dom_difference. Qed.
+  Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
+  Proof. unfold_leibniz; apply dom_fmap. Qed.
+End leibniz.
+
+(** * Set solver instances *)
+Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom D (∅:M A)) False.
+Proof. constructor. by rewrite dom_empty, elem_of_empty. Qed.
+Global Instance set_unfold_dom_alter {A} f i j (m : M A) Q :
+  SetUnfoldElemOf i (dom D m) Q →
+  SetUnfoldElemOf i (dom D (alter f j m)) Q.
+Proof. constructor. by rewrite dom_alter, (set_unfold_elem_of _ (dom _ _) _). Qed.
+Global Instance set_unfold_dom_insert {A} i j x (m : M A) Q :
+  SetUnfoldElemOf i (dom D m) Q →
+  SetUnfoldElemOf i (dom D (<[j:=x]> m)) (i = j ∨ Q).
+Proof.
+  constructor. by rewrite dom_insert, elem_of_union,
+    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
+Qed.
+Global Instance set_unfold_dom_delete {A} i j (m : M A) Q :
+  SetUnfoldElemOf i (dom D m) Q →
+  SetUnfoldElemOf i (dom D (delete j m)) (Q ∧ i ≠ j).
+Proof.
+  constructor. by rewrite dom_delete, elem_of_difference,
+    (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
+Qed.
+Global Instance set_unfold_dom_singleton {A} i j :
+  SetUnfoldElemOf i (dom D ({[ j := x ]} : M A)) (i = j).
+Proof. constructor. by rewrite dom_singleton, elem_of_singleton. Qed.
+Global Instance set_unfold_dom_union {A} i (m1 m2 : M A) Q1 Q2 :
+  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
+  SetUnfoldElemOf i (dom D (m1 ∪ m2)) (Q1 ∨ Q2).
+Proof.
+  constructor. by rewrite dom_union, elem_of_union,
+    !(set_unfold_elem_of _ (dom _ _) _).
+Qed.
+Global Instance set_unfold_dom_intersection {A} i (m1 m2 : M A) Q1 Q2 :
+  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
+  SetUnfoldElemOf i (dom D (m1 ∩ m2)) (Q1 ∧ Q2).
+Proof.
+  constructor. by rewrite dom_intersection, elem_of_intersection,
+    !(set_unfold_elem_of _ (dom _ _) _).
+Qed.
+Global Instance set_unfold_dom_difference {A} i (m1 m2 : M A) Q1 Q2 :
+  SetUnfoldElemOf i (dom D m1) Q1 → SetUnfoldElemOf i (dom D m2) Q2 →
+  SetUnfoldElemOf i (dom D (m1 ∖ m2)) (Q1 ∧ ¬Q2).
+Proof.
+  constructor. by rewrite dom_difference, elem_of_difference,
+    !(set_unfold_elem_of _ (dom _ _) _).
+Qed.
+Global Instance set_unfold_dom_fmap {A B} (f : A → B) i (m : M A) Q :
+  SetUnfoldElemOf i (dom D m) Q →
+  SetUnfoldElemOf i (dom D (f <$> m)) Q.
+Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _ _) _). Qed.
 End fin_map_dom.
 
 Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
@@ -180,3 +232,7 @@ Qed.
 Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
   dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
 Proof. unfold_leibniz. apply dom_seq. Qed.
+
+Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
+  SetUnfoldElemOf i (dom D (map_seq start (M:=M A) xs)) (start ≤ i < start + length xs).
+Proof. constructor. by rewrite dom_seq, elem_of_set_seq. Qed.