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.
@@ -97,17 +97,18 @@ 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.
-(** 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).
-Global Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
-Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
-Global Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
-Global Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : 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 (_ ## (_ ∖ _)) =>
@@ -115,6 +116,20 @@ Global Hint Extern 10 (_ ## (_ ∖ _)) =>
   | |- (_ ∖ _) ## _ => 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).
+Global Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
+Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
+Global Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
+Global Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with

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.