Merge branch 'robbert/mapset_dom_with' into 'master'

Simplify definition of `mapset_dom_with`.

Closes #183

See merge request !476

stdpp/mapset.v

@@ -109,11 +109,9 @@ Definition mapset_map_with {A B} (f : bool → A → option B)
     match x, y with
     | Some _, Some a => f true a | None, Some a => f false a | _, None => None
     end) mX.
+
 Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M :=
-  Mapset $ merge (λ x _,
-    match x with
-    | Some a => if f a then Some () else None | None => None
-    end) m (@empty (M A) _).
+  Mapset $ omap (λ a, if f a then Some () else None) m.
 
 Lemma lookup_mapset_map_with {A B} (f : bool → A → option B) X m i :
   mapset_map_with f X m !! i = m !! i ≫= f (bool_decide (i ∈ X)).
@@ -126,15 +124,18 @@ Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
   i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x.
 Proof.
   unfold mapset_dom_with, elem_of, mapset_elem_of.
-  simpl. rewrite lookup_merge, lookup_empty. destruct (m !! i) as [a|]; simpl.
+  simpl. rewrite lookup_omap. destruct (m !! i) as [a|]; simpl.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.
-Local Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+
+Local Instance mapset_dom {A} : Dom (M A) (mapset M) := λ m,
+  Mapset $ fmap (λ _, ()) m.
 Local Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
-  split; try apply _. intros. unfold dom, mapset_dom, is_Some.
-  rewrite elem_of_mapset_dom_with; naive_solver.
+  split; try apply _. intros A m i.
+  unfold dom, mapset_dom, is_Some, elem_of, mapset_elem_of; simpl.
+  rewrite lookup_fmap. destruct (m !! i); naive_solver.
 Qed.
 End mapset.
 

tests/fin_maps.v

@@ -289,6 +289,13 @@ Theorem gmap_insert_positives_union_reflexivity_1000 :
   = gmap_insert_positives 1 1 1000.
 Proof. (* this should less than a second *) reflexivity. Qed.
 
+(** This should be immediate, see std++ issue #183 *)
+Goal dom ((<[10%positive:=1]> ∅) : Pmap _) = dom ((<[10%positive:=2]> ∅) : Pmap _).
+Proof. reflexivity. Qed.
+
+Goal dom ((<["f":=1]> ∅) : gmap _ _) = dom ((<["f":=2]> ∅) : gmap _ _).
+Proof. reflexivity. Qed.
+
 (** Make sure that [pmap] and [gmap] can be used in nested inductive
 definitions *)