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

prelude/collections.v

@@ -41,6 +41,25 @@ Section simple_collection.
   Lemma elem_of_disjoint X Y : X ⊥ Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
   Proof. done. Qed.
 
+  Global Instance disjoint_sym : Symmetric (@disjoint C _).
+  Proof. intros ??. rewrite !elem_of_disjoint; naive_solver. Qed.
+  Lemma disjoint_empty_l Y : ∅ ⊥ Y.
+  Proof. rewrite elem_of_disjoint; intros x; by rewrite elem_of_empty. Qed.
+  Lemma disjoint_empty_r X : X ⊥ ∅.
+  Proof. rewrite (symmetry_iff _); apply disjoint_empty_l. Qed.
+  Lemma disjoint_singleton_l x Y : {[ x ]} ⊥ Y ↔ x ∉ Y.
+  Proof.
+    rewrite elem_of_disjoint; setoid_rewrite elem_of_singleton; naive_solver.
+  Qed.
+  Lemma disjoint_singleton_r y X : X ⊥ {[ y ]} ↔ y ∉ X.
+  Proof. rewrite (symmetry_iff (⊥)). apply disjoint_singleton_l. Qed.
+  Lemma disjoint_union_l X1 X2 Y : X1 ∪ X2 ⊥ Y ↔ X1 ⊥ Y ∧ X2 ⊥ Y.
+  Proof.
+    rewrite !elem_of_disjoint; setoid_rewrite elem_of_union; naive_solver.
+  Qed.
+  Lemma disjoint_union_r X Y1 Y2 : X ⊥ Y1 ∪ Y2 ↔ X ⊥ Y1 ∧ X ⊥ Y2.
+  Proof. rewrite !(symmetry_iff (⊥) X). apply disjoint_union_l. Qed.
+
   Lemma collection_positive_l X Y : X ∪ Y ≡ ∅ → X ≡ ∅.
   Proof.
     rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.

proofmode/tactics.v

@@ -24,8 +24,10 @@ Ltac iFresh :=
   |- of_envs ?Δ ⊢ _ =>
       match goal with
       | _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
-      (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
-      | _ => eval cbv in (fresh_string_of_set "~" (dom stringset Δ))
+      | _ =>
+         (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
+         let Hs := eval cbv in (dom stringset Δ) in
+         eval vm_compute in (fresh_string_of_set "~" Hs)
       end
   | _ => constr:"~"
   end.