Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

prelude/gmultiset.v

@@ -39,11 +39,15 @@ Section definitions.
     let (X) := X in let (Y) := Y in
     GMultiSet $ difference_with (λ x y,
       let z := x - y in guard (0 < z); Some (pred z)) X Y.
+
+  Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
+    let (X) := X in dom _ X.
 End definitions.
 
 Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
 Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
 Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
+Typeclasses Opaque gmultiset_dom.
 
 (** These instances are declared using [Hint Extern] to avoid too
 eager type class search. *)
@@ -63,6 +67,8 @@ Hint Extern 1 (Elements _ (gmultiset _)) =>
   eapply @gmultiset_elements : typeclass_instances.
 Hint Extern 1 (Size (gmultiset _)) =>
   eapply @gmultiset_size : typeclass_instances.
+Hint Extern 1 (Dom (gmultiset _) _) =>
+  eapply @gmultiset_dom : typeclass_instances.
 
 Section lemmas.
 Context `{Countable A}.
@@ -196,6 +202,12 @@ Proof.
     exists (x,n); split; [|by apply elem_of_map_to_list].
     apply elem_of_replicate; auto with omega.
 Qed.
+Lemma gmultiset_elem_of_dom x X : x ∈ dom (gset A) X ↔ x ∈ X.
+Proof.
+  unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
+  destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
+  destruct (X !! x); naive_solver omega.
+Qed.
 
 (* Properties of the size operation *)
 Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.

prelude/tactics.v

@@ -478,8 +478,13 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | |- ∀ _, _ => intro
   (**i simplification of assumptions *)
   | H : False |- _ => destruct H
-  | H : _ ∧ _ |- _ => destruct H
-  | H : ∃ _, _  |- _ => destruct H
+  | H : _ ∧ _ |- _ =>
+     (* Work around bug https://coq.inria.fr/bugs/show_bug.cgi?id=2901 *)
+     let H1 := fresh in let H2 := fresh in
+     destruct H as [H1 H2]; try clear H
+  | H : ∃ _, _  |- _ =>
+     let x := fresh in let Hx := fresh in
+     destruct H as [x Hx]; try clear H
   | H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
   | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
   | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
@@ -491,7 +496,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | |- _ ∧ _ => split
   | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
   | |- Is_true (_ && _) => apply andb_True; split
-  | H : _ ∨ _ |- _ => destruct H
+  | H : _ ∨ _ |- _ =>
+     let H1 := fresh in destruct H as [H1|H1]; try clear H
   (**i solve the goal using the user supplied tactic *)
   | |- _ => solve [tac]
   end;