theories/mapset.v → stdpp/mapset.v

@@ -8,8 +8,14 @@ From stdpp Require Import options.
 locally (or things moved out of sections) as no default works well enough. *)
 Unset Default Proof Using.
 
-Record mapset (M : Type → Type) : Type :=
-  Mapset { mapset_car: M (unit : Type) }.
+(** Given a type of maps [M : Type → Type], we construct sets as [M ()], i.e.,
+maps with unit values. To avoid unnecessary universe constraints, we first
+define [mapset' Munit] with [Munit : Type] as a record, and then [mapset M] with
+[M : Type → Type] as a notation. See [tests/universes.v] for a test case that
+fails otherwise. *)
+Record mapset' (Munit : Type) : Type :=
+  Mapset { mapset_car: Munit }.
+Notation mapset M := (mapset' (M unit)).
 Global Arguments Mapset {_} _ : assert.
 Global Arguments mapset_car {_} _ : assert.
 
@@ -103,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)).
@@ -120,20 +124,19 @@ 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 by done. destruct (m !! i) as [a|].
+  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.
 
-(** [mapset_elem_of] internally contains an equality; make sure that tactics do
-not unfold it and try to unify [∈] against goals with [=]. *)
-Opaque mapset_elem_of.
-
 Global Arguments mapset_eq_dec : simpl never.

theories/namespaces.v → stdpp/namespaces.v

@@ -4,21 +4,21 @@ From stdpp Require Import options.
 Definition namespace := list positive.
 Global Instance namespace_eq_dec : EqDecision namespace := _.
 Global Instance namespace_countable : Countable namespace := _.
-Typeclasses Opaque namespace.
+Global Typeclasses Opaque namespace.
 
 Definition nroot : namespace := nil.
 
-Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
+Local Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
-Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
+Local Definition ndot_aux : seal (@ndot_def). by eexists. Qed.
 Definition ndot {A A_dec A_count}:= unseal ndot_aux A A_dec A_count.
-Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux.
+Local Definition ndot_unseal : @ndot = @ndot_def := seal_eq ndot_aux.
 
-Definition nclose_def (N : namespace) : coPset :=
+Local Definition nclose_def (N : namespace) : coPset :=
   coPset_suffixes (positives_flatten N).
-Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
+Local Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
 Global Instance nclose : UpClose namespace coPset := unseal nclose_aux.
-Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
+Local Definition nclose_unseal : @nclose = @nclose_def := seal_eq nclose_aux.
 
 Notation "N .@ x" := (ndot N x)
   (at level 19, left associativity, format "N .@ x") : stdpp_scope.
@@ -33,14 +33,14 @@ Section namespace.
   Implicit Types E : coPset.
 
   Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
-  Proof. intros N1 x1 N2 x2; rewrite !ndot_eq; naive_solver. Qed.
+  Proof. intros N1 x1 N2 x2; rewrite !ndot_unseal; naive_solver. Qed.
 
   Lemma nclose_nroot : ↑nroot = (⊤:coPset).
-  Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
+  Proof. rewrite nclose_unseal. by apply (sig_eq_pi _). Qed.
 
   Lemma nclose_subseteq N x : ↑N.@x ⊆ (↑N : coPset).
   Proof.
-    intros p. unfold up_close. rewrite !nclose_eq, !ndot_eq.
+    intros p. unfold up_close. rewrite !nclose_unseal, !ndot_unseal.
     unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
     intros [q ->]. destruct (positives_flatten_suffix N (ndot_def N x)) as [q' ?].
     { by exists [encode x]. }
@@ -51,11 +51,11 @@ Section namespace.
   Proof. intros. etrans; eauto using nclose_subseteq. Qed.
 
   Lemma nclose_infinite N : ¬set_finite (↑ N : coPset).
-  Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
+  Proof. rewrite nclose_unseal. apply coPset_suffixes_infinite. Qed.
 
   Lemma ndot_ne_disjoint N x y : x ≠ y → N.@x ## N.@y.
   Proof.
-    intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
+    intros Hxy a. unfold up_close. rewrite !nclose_unseal, !ndot_unseal.
     unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
     intros [qx ->] [qy Hqy].
     revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq.
@@ -84,6 +84,11 @@ Local Definition coPset_empty_subseteq := empty_subseteq (C:=coPset).
 Global Hint Resolve coPset_empty_subseteq : ndisj.
 Local Definition coPset_union_least := union_least (C:=coPset).
 Global Hint Resolve coPset_union_least : ndisj.
+(** For goals like [X ⊆ L ∪ R], backtrack for the two sides. *)
+Local Definition coPset_union_subseteq_l' := union_subseteq_l' (C:=coPset).
+Global Hint Resolve coPset_union_subseteq_l' | 50 : ndisj.
+Local Definition coPset_union_subseteq_r' := union_subseteq_r' (C:=coPset).
+Global Hint Resolve coPset_union_subseteq_r' | 50 : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Local Definition coPset_subseteq_difference_l := subseteq_difference_l (C:=coPset).
 Global Hint Resolve coPset_subseteq_difference_l | 100 : ndisj.
@@ -92,6 +97,32 @@ Global Hint Resolve nclose_subseteq' | 100 : ndisj.
 (** Rules for goals of the form [_ ## _] *)
 (** The base rule that we want to ultimately get down to. *)
 Global Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
+(** Trivial cases. *)
+Local Definition coPset_disjoint_empty_l := disjoint_empty_l (C:=coPset).
+Global Hint Resolve coPset_disjoint_empty_l : ndisj.
+Local Definition coPset_disjoint_empty_r := disjoint_empty_r (C:=coPset).
+Global Hint Resolve coPset_disjoint_empty_r : ndisj.
+(** If-and-only-if rules for ∪ on the left/right. *)
+Local Definition coPset_disjoint_union_l X1 X2 Y :=
+  proj2 (disjoint_union_l (C:=coPset) X1 X2 Y).
+Global Hint Resolve coPset_disjoint_union_l : ndisj.
+Local Definition coPset_disjoint_union_r X Y1 Y2 :=
+  proj2 (disjoint_union_r (C:=coPset) X Y1 Y2).
+Global Hint Resolve coPset_disjoint_union_r : ndisj.
+(** We prefer ∖ on the left of ## (for the [disjoint_difference] lemmas to
+apply), so try moving it there. *)
+Global Hint Extern 10 (_ ## (_ ∖ _)) =>
+  lazymatch goal with
+  | |- (_ ∖ _) ## _ => fail (* ∖ on both sides, leave it be *)
+  | |- _ => symmetry
+  end : ndisj.
+(** Before we apply disjoint_difference, let's make sure we normalize the goal
+to [_ ∖ (_ ∪ _)]. *)
+Local Lemma coPset_difference_difference (X1 X2 X3 Y : coPset) :
+  X1 ∖ (X2 ∪ X3) ## Y →
+  X1 ∖ X2 ∖ X3 ## Y.
+Proof. set_solver. Qed.
+Global Hint Resolve coPset_difference_difference | 20 : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress.
 Tests show trying [disjoint_difference_l1] first gives better performance. *)
 Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).

theories/options.v → stdpp/options.v

-(** Coq configuration for std++ (not meant to leak to clients) *)
+(** Coq configuration for std++ (not meant to leak to clients).
+If you are a user of std++, note that importing this file means
+you are implicitly opting-in to every new option we will add here
+in the future. We are *not* guaranteeing any kind of stability here.
+Instead our advice is for you to have your own options file; then
+you can re-export the std++ file there but if we ever add an option
+you disagree with you can easily overwrite it in one central location. *)
 (* Everything here should be [Export Set], which means when this
 file is *imported*, the option will only apply on the import site
 but not transitively. *)
 
-Export Set Default Proof Using "Type".
+(** Allow async proof-checking of sections. *)
+#[export] Set Default Proof Using "Type".
 (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
-Export Set Suggest Proof Using. *)
-Export Set Default Goal Selector "!".
+#[export] Set Suggest Proof Using. *)
+
+(** Enforces that every tactic is executed with a single focused goal, meaning
+that bullets and curly braces must be used to structure the proof. *)
+#[export] Set Default Goal Selector "!".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.