Commit 09b0b3c9 by Robbert Krebbers

### Use more informative tags `Strong` and `Weak` for the modalities.

parent 655cbe71
 ... ... @@ -126,7 +126,7 @@ Section list. Proof. apply (big_opL_commute _). Qed. Lemma big_sepL_forall Φ l : (∀ k x, PersistentP true (Φ k x)) → (∀ k x, PersistentP Weak (Φ k x)) → ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x). Proof. intros HΦ. apply (anti_symm _). ... ... @@ -316,7 +316,7 @@ Section gmap. Proof. apply (big_opM_commute _). Qed. Lemma big_sepM_forall Φ m : (∀ k x, PersistentP true (Φ k x)) → (∀ k x, PersistentP Weak (Φ k x)) → ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x). Proof. intros. apply (anti_symm _). ... ... @@ -468,7 +468,7 @@ Section gset. Proof. apply (big_opS_commute _). Qed. Lemma big_sepS_forall Φ X : (∀ x, PersistentP true (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). (∀ x, PersistentP Weak (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x). Proof. intros. apply (anti_symm _). { apply forall_intro=> x. ... ...
 ... ... @@ -16,13 +16,13 @@ Notation "▷? p P" := (uPred_laterN (Nat.b2n p) P) (at level 20, p at level 9, P at level 20, format "▷? p P") : uPred_scope. Definition uPred_always_if {M} (c p : bool) (P : uPred M) : uPred M := Definition uPred_always_if {M} (c : strength) (p : bool) (P : uPred M) : uPred M := (if p then □{c} P else P)%I. Instance: Params (@uPred_always_if) 2. Arguments uPred_always_if _ _ !_ _/. Notation "□{ c }? p P" := (uPred_always_if c p P) (at level 20, c at next level, p at level 9, P at level 20, format "□{ c }? p P"). Notation "□? p P" := (uPred_always_if true p P) Notation "□? p P" := (uPred_always_if Weak p P) (at level 20, p at level 9, P at level 20, format "□? p P"). Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P. ... ... @@ -36,7 +36,7 @@ Arguments timelessP {_} _ {_}. Hint Mode TimelessP + ! : typeclass_instances. Instance: Params (@TimelessP) 1. Class PersistentP {M} (c : bool) (P : uPred M) := persistentP : P ⊢ □{c} P. Class PersistentP {M} (c : strength) (P : uPred M) := persistentP : P ⊢ □{c} P. Arguments persistentP {_} _ _ {_}. Hint Mode PersistentP + + ! : typeclass_instances. Instance: Params (@PersistentP) 2. ... ... @@ -743,7 +743,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q. Proof. rewrite /uPred_except_0. apply (anti_symm _). - apply or_elim; last by auto. by rewrite -!or_intro_l -(always_pure true) -always_later -always_sep_dup'. by rewrite -!or_intro_l -(always_pure Weak) -always_later -always_sep_dup'. - rewrite sep_or_r sep_elim_l sep_or_l; auto. Qed. Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a. ... ... @@ -840,7 +840,7 @@ Proof. apply or_mono, wand_intro_l; first done. rewrite -{2}(löb Q); apply impl_intro_l. rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto. rewrite -(always_pure true) -always_later always_and_sep_l'. rewrite -(always_pure Weak) -always_later always_and_sep_l'. by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r. Qed. Global Instance forall_timeless {A} (Ψ : A → uPred M) : ... ... @@ -885,7 +885,7 @@ Global Instance limit_preserving_PersistentP NonExpansive Φ → LimitPreserving (λ x, PersistentP c (Φ x)). Proof. intros. apply limit_preserving_entails; solve_proper. Qed. Lemma persistent_mask_weaken P : PersistentP false P → PersistentP true P. Lemma persistent_strength_weaken P : PersistentP Strong P → PersistentP Weak P. Proof. rewrite /PersistentP=> HP. by rewrite {1}HP always_mask_mono. Qed. Lemma always_always c P `{!PersistentP c P} : □{c} P ⊣⊢ P. ... ... @@ -894,43 +894,43 @@ Lemma always_if_always c p P `{!PersistentP c P} : □{c}?p P ⊣⊢ P. Proof. destruct p; simpl; auto using always_always. Qed. Lemma always_intro c P Q `{!PersistentP c P} : (P ⊢ Q) → P ⊢ □{c} Q. Proof. rewrite -(always_always c P); apply always_intro'. Qed. Lemma always_and_sep_l P Q `{!PersistentP true P} : P ∧ Q ⊣⊢ P ∗ Q. Proof. by rewrite -(always_always true P) always_and_sep_l'. Qed. Lemma always_and_sep_r P Q `{!PersistentP true Q} : P ∧ Q ⊣⊢ P ∗ Q. Proof. by rewrite -(always_always true Q) always_and_sep_r'. Qed. Lemma always_sep_dup P `{!PersistentP true P} : P ⊣⊢ P ∗ P. Proof. by rewrite -(always_always true P) -always_sep_dup'. Qed. Lemma always_entails_l P Q `{!PersistentP true Q} : (P ⊢ Q) → P ⊢ Q ∗ P. Proof. by rewrite -(always_always true Q); apply always_entails_l'. Qed. Lemma always_entails_r P Q `{!PersistentP true Q} : (P ⊢ Q) → P ⊢ P ∗ Q. Proof. by rewrite -(always_always true Q); apply always_entails_r'. Qed. Lemma always_impl_wand P `{!PersistentP true P} Q : (P → Q) ⊣⊢ (P -∗ Q). Lemma always_and_sep_l P Q `{!PersistentP Weak P} : P ∧ Q ⊣⊢ P ∗ Q. Proof. by rewrite -(always_always Weak P) always_and_sep_l'. Qed. Lemma always_and_sep_r P Q `{!PersistentP Weak Q} : P ∧ Q ⊣⊢ P ∗ Q. Proof. by rewrite -(always_always Weak Q) always_and_sep_r'. Qed. Lemma always_sep_dup P `{!PersistentP Weak P} : P ⊣⊢ P ∗ P. Proof. by rewrite -(always_always Weak P) -always_sep_dup'. Qed. Lemma always_entails_l P Q `{!PersistentP Weak Q} : (P ⊢ Q) → P ⊢ Q ∗ P. Proof. by rewrite -(always_always Weak Q); apply always_entails_l'. Qed. Lemma always_entails_r P Q `{!PersistentP Weak Q} : (P ⊢ Q) → P ⊢ P ∗ Q. Proof. by rewrite -(always_always Weak Q); apply always_entails_r'. Qed. Lemma always_impl_wand P `{!PersistentP Weak P} Q : (P → Q) ⊣⊢ (P -∗ Q). Proof. apply (anti_symm _); auto using impl_wand. apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r. Qed. Lemma bupd_persistent P `{!PersistentP false P} : (|==> P) ⊢ P. Proof. by rewrite -{1}(always_always false P) bupd_always. Qed. Lemma bupd_persistent P `{!PersistentP Strong P} : (|==> P) ⊢ P. Proof. by rewrite -{1}(always_always Strong P) bupd_always. Qed. (* Persistence *) Global Instance pure_persistent c φ : PersistentP c (⌜φ⌝ : uPred M)%I. Proof. by rewrite /PersistentP always_pure. Qed. Global Instance impl_persistent c P Q : PersistentP false P → PersistentP c Q → PersistentP c (P → Q). PersistentP Strong P → PersistentP c Q → PersistentP c (P → Q). Proof. rewrite /PersistentP=> HP HQ. rewrite {2}HP -always_impl_always. by rewrite -HQ always_elim. Qed. Global Instance wand_persistent c P Q : PersistentP false P → PersistentP c Q → PersistentP c (P -∗ Q)%I. PersistentP Strong P → PersistentP c Q → PersistentP c (P -∗ Q)%I. Proof. rewrite /PersistentP=> HP HQ. by rewrite {2}HP -{1}(always_elim false P) !wand_impl_always -always_impl_always -HQ. by rewrite {2}HP -{1}(always_elim Strong P) !wand_impl_always -always_impl_always -HQ. Qed. Global Instance always_persistent c P : PersistentP c (□{c} P). Proof. by apply always_intro'. Qed. Global Instance always_persistent' c P : PersistentP true (□{c} P). Global Instance always_persistent' c P : PersistentP Weak (□{c} P). Proof. by rewrite /PersistentP always_idemp'. Qed. Global Instance and_persistent c P Q : PersistentP c P → PersistentP c Q → PersistentP c (P ∧ Q). ... ... @@ -959,7 +959,7 @@ Global Instance except_0_persistent c P : PersistentP c P → PersistentP c (◇ Proof. by intros; rewrite /PersistentP -except_0_always; apply except_0_mono. Qed. Global Instance laterN_persistent c n P : PersistentP c P → PersistentP c (▷^n P). Proof. induction n; apply _. Qed. Global Instance ownM_persistent : Persistent a → PersistentP true (@uPred_ownM M a). Global Instance ownM_persistent : Persistent a → PersistentP Weak (@uPred_ownM M a). Proof. intros. by rewrite /PersistentP always_ownM. Qed. Global Instance from_option_persistent {A} c P (Ψ : A → uPred M) (mx : option A) : (∀ x, PersistentP c (Ψ x)) → PersistentP c P → PersistentP c (from_option Ψ P mx). ... ... @@ -1033,4 +1033,4 @@ the instance at any node in the proof search tree. To avoid that, we declare it using a [Hint Immediate], so that it will only be used at the leaves of the proof search tree, i.e. when the premise of the hint can be derived from just the current context. *) Hint Immediate uPred.persistent_mask_weaken : typeclass_instances. Hint Immediate uPred.persistent_strength_weaken : typeclass_instances.
 ... ... @@ -33,7 +33,7 @@ Section definitions. Global Instance auth_own_timeless a : TimelessP (auth_own a). Proof. apply _. Qed. Global Instance auth_own_persistent a : Persistent a → PersistentP true (auth_own a). Persistent a → PersistentP Weak (auth_own a). Proof. apply _. Qed. Global Instance auth_inv_ne n : ... ... @@ -52,7 +52,7 @@ Section definitions. Proper (pointwise_relation T (≡) ==> pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N). Proof. solve_proper. Qed. Global Instance auth_ctx_persistent N f φ : PersistentP true (auth_ctx N f φ). Global Instance auth_ctx_persistent N f φ : PersistentP Weak (auth_ctx N f φ). Proof. apply _. Qed. End definitions. ... ...
 ... ... @@ -65,7 +65,7 @@ Proof. solve_contractive. Qed. Global Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ). Proof. apply ne_proper, _. Qed. Global Instance slice_persistent γ P : PersistentP true (slice N γ P). Global Instance slice_persistent γ P : PersistentP Weak (slice N γ P). Proof. apply _. Qed. Global Instance box_contractive f : Contractive (box N f). ... ...
 ... ... @@ -34,7 +34,7 @@ Section proofs. Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ). Proof. exact: ne_proper. Qed. Global Instance cinv_persistent N γ P : PersistentP true (cinv N γ P). Global Instance cinv_persistent N γ P : PersistentP Weak (cinv N γ P). Proof. rewrite /cinv; apply _. Qed. Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ). ... ...
 ... ... @@ -5,7 +5,7 @@ Import uPred. (** The "core" of an assertion is its maximal persistent part. *) Definition coreP {M : ucmraT} (P : uPred M) : uPred M := (∀ Q, □{false} (Q → □ Q) → □{false} (P → Q) → Q)%I. (∀ Q, □{Strong} (Q → □ Q) → □{Strong} (P → Q) → Q)%I. Instance: Params (@coreP) 1. Typeclasses Opaque coreP. ... ... @@ -16,7 +16,7 @@ Section core. Lemma coreP_intro P : P -∗ coreP P. Proof. iIntros "HP". iIntros (Q) "_ HPQ". by iApply "HPQ". Qed. Global Instance coreP_persistent P : PersistentP true (coreP P). Global Instance coreP_persistent P : PersistentP Weak (coreP P). Proof. rewrite /coreP /PersistentP. iIntros "HC". iApply always_forall. iIntros (Q). (* FIXME: iIntros should apply always_forall automatically. *) ... ... @@ -36,7 +36,7 @@ Section core. iApply ("H" \$! Q with "[]"); first done. by rewrite HP. Qed. Lemma coreP_elim P : PersistentP true P → coreP P -∗ P. Lemma coreP_elim P : PersistentP Weak P → coreP P -∗ P. Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" \$! P); auto. Qed. Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q). ... ...
 ... ... @@ -12,7 +12,7 @@ Module savedprop. Section savedprop. (** Saved Propositions and the update modality *) Context (sprop : Type) (saved : sprop → iProp → iProp). Hypothesis sprop_persistent : ∀ i P, PersistentP true (saved i P). Hypothesis sprop_persistent : ∀ i P, PersistentP Weak (saved i P). Hypothesis sprop_alloc_dep : ∀ (P : sprop → iProp), (|==> (∃ i, saved i (P i)))%I. Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q). ... ... @@ -67,7 +67,7 @@ Module inv. Section inv. (** We have invariants *) Context (name : Type) (inv : name → iProp → iProp). Hypothesis inv_persistent : ∀ i P, PersistentP true (inv i P). Hypothesis inv_persistent : ∀ i P, PersistentP Weak (inv i P). Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P). Hypothesis inv_open : ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R). ... ... @@ -130,7 +130,7 @@ Module inv. Section inv. (** Now to the actual counterexample. We start with a weird form of saved propositions. *) Definition saved (γ : gname) (P : iProp) : iProp := ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)). Global Instance saved_persistent γ P : PersistentP true (saved γ P) := _. Global Instance saved_persistent γ P : PersistentP Weak (saved γ P) := _. Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)). Proof. ... ... @@ -163,7 +163,7 @@ Module inv. Section inv. (** And now we tie a bad knot. *) Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope. Definition A i : iProp := ∃ P, ¬P ∗ saved i P. Global Instance A_persistent i : PersistentP true (A i) := _. Global Instance A_persistent i : PersistentP Weak (A i) := _. Lemma A_alloc : fupd M1 (∃ i, saved i (A i)). Proof. by apply saved_alloc. Qed. ... ...
 ... ... @@ -141,7 +141,7 @@ Proof. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep. Qed. Lemma fupd_persistent' {E1 E2 E2'} P Q `{!PersistentP false P} : Lemma fupd_persistent' {E1 E2 E2'} P Q `{!PersistentP Strong P} : E1 ⊆ E2 → (Q ={E1, E2'}=∗ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P). Proof. ... ... @@ -159,7 +159,7 @@ Proof. iModIntro; iFrame; auto. Qed. Lemma fupd_plain {E1 E2} P Q `{!PersistentP false P} : Lemma fupd_plain {E1 E2} P Q `{!PersistentP Strong P} : E1 ⊆ E2 → (Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P). Proof. iIntros (HE HQP) "HQ". ... ... @@ -167,7 +167,7 @@ Proof. by iIntros "?"; iApply fupd_intro; iApply HQP. Qed. Lemma later_fupd_plain {E} P `{Hpl: !PersistentP false P} : Lemma later_fupd_plain {E} P `{Hpl: !PersistentP Strong P} : (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P. Proof. iIntros "HP". rewrite fupd_eq /fupd_def. ... ...
 ... ... @@ -13,7 +13,7 @@ Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q) format "P ={ E1 , E2 }=> Q") : uPred_scope. Context (vs_ne : ∀ E1 E2, NonExpansive2 (vs E1 E2)). Context (vs_persistent : ∀ E1 E2 P Q, PersistentP true (P ={E1,E2}=> Q)). Context (vs_persistent : ∀ E1 E2 P Q, PersistentP Weak (P ={E1,E2}=> Q)). Context (vs_impl : ∀ E P Q, □ (P → Q) ⊢ P ={E,E}=> Q). Context (vs_transitive : ∀ E1 E2 E3 P Q R, ... ... @@ -24,7 +24,7 @@ Context (vs_frame_r : ∀ E1 E2 P Q R, (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q Context (vs_exists : ∀ {A} E1 E2 (Φ : A → uPred M) Q, (∀ x, Φ x ={E1,E2}=> Q) ⊢ (∃ x, Φ x) ={E1,E2}=> Q). Context (vs_persistent_intro_r : ∀ E1 E2 P Q R, PersistentP true R → PersistentP Weak R → (R -∗ (P ={E1,E2}=> Q)) ⊢ P ∗ R ={E1,E2}=> Q). Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M := ... ...
 ... ... @@ -50,7 +50,7 @@ Section fractional. (** Fractional and logical connectives *) Global Instance persistent_fractional P : PersistentP true P → Fractional (λ _, P). PersistentP Weak P → Fractional (λ _, P). Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed. Global Instance fractional_sep Φ Ψ : ... ...
 ... ... @@ -31,7 +31,7 @@ Proof. apply contractive_ne, _. Qed. Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N). Proof. apply ne_proper, _. Qed. Global Instance inv_persistent N P : PersistentP true (inv N P). Global Instance inv_persistent N P : PersistentP Weak (inv N P). Proof. rewrite inv_eq /inv; apply _. Qed. Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset). ... ...
 ... ... @@ -40,7 +40,7 @@ Section proofs. Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N). Proof. apply (ne_proper _). Qed. Global Instance na_inv_persistent p N P : PersistentP true (na_inv p N P). Global Instance na_inv_persistent p N P : PersistentP Weak (na_inv p N P). Proof. rewrite /na_inv; apply _. Qed. Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I. ... ...
 ... ... @@ -108,7 +108,7 @@ Proof. by rewrite comm -own_valid_r. Qed. Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a). Proof. rewrite !own_eq /own_def; apply _. Qed. Global Instance own_core_persistent γ a : Persistent a → PersistentP true (own γ a). Global Instance own_core_persistent γ a : Persistent a → PersistentP Weak (own γ a). Proof. rewrite !own_eq /own_def; apply _. Qed. (** ** Allocation *) ... ...
 ... ... @@ -24,7 +24,7 @@ Section saved_prop. Implicit Types γ : gname. Global Instance saved_prop_persistent γ x : PersistentP true (saved_prop_own γ x). PersistentP Weak (saved_prop_own γ x). Proof. rewrite /saved_prop_own; apply _. Qed. Lemma saved_prop_alloc_strong x (G : gset gname) : ... ...
 ... ... @@ -43,11 +43,11 @@ Section definitions. Global Instance sts_ctx_proper `{!invG Σ} N : Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N). Proof. solve_proper. Qed. Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP true (sts_ctx N φ). Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP Weak (sts_ctx N φ). Proof. apply _. Qed. Global Instance sts_own_persistent s : PersistentP true (sts_own s ∅). Global Instance sts_own_persistent s : PersistentP Weak (sts_own s ∅). Proof. apply _. Qed. Global Instance sts_ownS_persistent S : PersistentP true (sts_ownS S ∅). Global Instance sts_ownS_persistent S : PersistentP Weak (sts_ownS S ∅). Proof. apply _. Qed. End definitions. ... ...
 ... ... @@ -49,7 +49,7 @@ Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ). Proof. solve_contractive. Qed. Global Instance ownI_contractive i : Contractive (@ownI Σ _ i). Proof. solve_contractive. Qed. Global Instance ownI_persistent i P : PersistentP true (ownI i P). Global Instance ownI_persistent i P : PersistentP Weak (ownI i P). Proof. rewrite /ownI. apply _. Qed. Lemma ownE_empty : (|==> ownE ∅)%I. ... ...
 ... ... @@ -97,8 +97,9 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M. Definition uPred_wand_eq : @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux. Program Definition uPred_always_def {M} (c : bool) (P : uPred M) : uPred M := {| uPred_holds n x := P n (if c then core x else ε) |}. Inductive strength := Weak | Strong. Program Definition uPred_always_def {M} (c : strength) (P : uPred M) : uPred M := {| uPred_holds n x := P n (if c is Weak return _ then core x else ε) |}. Next Obligation. intros M []; naive_solver eauto using uPred_mono, @cmra_core_monoN. Qed. ... ... @@ -181,10 +182,8 @@ Notation "∃ x .. y , P" := (at level 200, x binder, y binder, right associativity) : uPred_scope. Notation "□{ c } P" := (uPred_always c P) (at level 20, c at next level, right associativity, format "□{ c } P") : uPred_scope. Notation "□ P" := (□{true} P)%I Notation "□ P" := (□{Weak} P)%I (at level 20, right associativity) : uPred_scope. Notation "▷ P" := (uPred_later P) (at level 20, right associativity) : uPred_scope. Infix "≡" := uPred_internal_eq : uPred_scope. ... ... @@ -436,7 +435,7 @@ Proof. intros HP; unseal; split=> n x ? /=. apply HP; destruct c; auto using ucmra_unit_validN, cmra_core_validN. Qed. Lemma always_mask_mono P : □{false} P ⊢ □ P. Lemma always_mask_mono P : □{Strong} P ⊢ □ P. Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed. Lemma always_elim' P : □ P ⊢ P. Proof. ... ... @@ -451,19 +450,19 @@ Proof. by unseal. Qed. Lemma always_exist_1 {A} c (Ψ : A → uPred M) : (□{c} ∃ a, Ψ a) ⊢ (∃ a, □{c} Ψ a). Proof. by unseal. Qed. Lemma prop_ext P Q : □{false} ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q. Lemma prop_ext P Q : □{Strong} ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q. Proof. unseal; split=> n x ? /= HPQ; split=> n' x' ? HP; split; eapply HPQ; eauto using @ucmra_unit_least. Qed. Lemma always_and_sep_l_1' P Q : □{true} P ∧ Q ⊢ □{true} P ∗ Q. Lemma always_and_sep_l_1' P Q : □ P ∧ Q ⊢ □ P ∗ Q. Proof. unseal; split=> n x ? [??]; exists (core x), x; simpl in *. by rewrite cmra_core_l cmra_core_idemp. Qed. Lemma always_impl_always c P Q : (□{false} P → □{c} Q) ⊢ □{c} (□{false} P → Q). Lemma always_impl_always c P Q : (□{Strong} P → □{c} Q) ⊢ □{c} (□{Strong} P → Q). Proof. unseal; split=> /= n x ? HPQ n' x' ????. destruct c. - eapply uPred_mono with (core x), cmra_included_includedN; auto. ... ... @@ -541,7 +540,7 @@ Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → uPred_valid (M:=M) (✓ a Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed. Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False. Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed. Lemma always_cmra_valid_1' {A : cmraT} (a : A) : ✓ a ⊢ □{false} ✓ a. Lemma always_cmra_valid_1' {A : cmraT} (a : A) : ✓ a ⊢ □{Strong} ✓ a. Proof. by unseal. Qed. Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a. Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed. ... ... @@ -578,7 +577,7 @@ Proof. exists (y ⋅ x3); split; first by rewrite -assoc. exists y; eauto using cmra_includedN_l. Qed. Lemma bupd_always P : (|==> □{false} P) ⊢ P. Lemma bupd_always P : (|==> □{Strong} P) ⊢ P. Proof. unseal; split => n x Hnx /= Hng. destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto. ... ...
 ... ... @@ -29,7 +29,7 @@ Section mono_proof. (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I. (** The main proofs. *) Global Instance mcounter_persistent l n : PersistentP true (mcounter l n). Global Instance mcounter_persistent l n : PersistentP Weak (mcounter l n). Proof. apply _. Qed. Lemma newcounter_mono_spec : ... ...
 ... ... @@ -14,7 +14,7 @@ Structure lock Σ `{!heapG Σ} := Lock { locked (γ: name) : iProp Σ; (* -- general properties -- *) is_lock_ne N γ lk : NonExpansive (is_lock N γ lk); is_lock_persistent N γ lk R : PersistentP true (is_lock N γ lk R); is_lock_persistent N γ lk R : PersistentP Weak (is_lock N γ lk R); locked_timeless γ : TimelessP (locked γ); locked_exclusive γ : locked γ -∗ locked γ -∗ False; (* -- operation specs -- *) ... ...
 ... ... @@ -40,7 +40,7 @@ Section proof. Proof. solve_proper. Qed. (** The main proofs. *) Global Instance is_lock_persistent γ l R : PersistentP true (is_lock γ l R). Global Instance is_lock_persistent γ l R : PersistentP Weak (is_lock γ l R). Proof. apply _. Qed. Global Instance locked_timeless γ : TimelessP (locked γ). Proof. apply _. Qed. ... ...
 ... ... @@ -59,7 +59,7 @@ Section proof. Proof. solve_proper. Qed. Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk). Proof. solve_proper. Qed. Global Instance is_lock_persistent γ lk R : PersistentP true (is_lock γ lk R). Global Instance is_lock_persistent γ lk R : PersistentP Weak (is_lock γ lk R). Proof. apply _. Qed. Global Instance locked_timeless γ : TimelessP (locked γ). Proof. apply _. Qed. ... ...
 ... ... @@ -106,7 +106,7 @@ Proof. iModIntro; iNext; iMod "H" as ">?". by iApply IH. Qed. Lemma bupd_iter_laterN_mono n P Q `{!PersistentP false Q} : Lemma bupd_iter_laterN_mono n P Q `{!PersistentP Strong Q} : (P ⊢ Q) → Nat.iter n (λ P, |==> ▷ P)%I P ⊢ ▷^n Q. Proof. intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_persistent. ... ...
 ... ... @@ -146,7 +146,7 @@ Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed. Global Instance into_persistentP_always P : IntoPersistentP true P P | 1. Proof. done. Qed. Global Instance into_persistentP_persistent P : PersistentP true P → IntoPersistentP false P P | 100. PersistentP Weak P → IntoPersistentP false P P | 100. Proof. done. Qed. (* IntoLater *) ... ... @@ -339,10 +339,10 @@ Proof. by apply mk_from_and_and. Qed. Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100. Proof. done. Qed. Global Instance from_and_sep_persistent_l P1 P2 : PersistentP true P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9. PersistentP Weak P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9. Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed. Global Instance from_and_sep_persistent_r P1 P2 : PersistentP true P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10. PersistentP Weak P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10. Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed. Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝. ... ... @@ -385,7 +385,7 @@ Global Instance from_and_big_sepL_cons {A} (Φ : nat → A → uPred M) x l : FromAnd false ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y). Proof. by rewrite /FromAnd big_sepL_cons. Qed. Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l : PersistentP true (Φ 0 x) → PersistentP Weak (Φ 0 x) → FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y). Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed. ... ... @@ -394,7 +394,7 @@ Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 : ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y). Proof. by rewrite /FromAnd big_opL_app. Qed. Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 : (∀ k y, PersistentP true (Φ k y)) → (∀ k y, PersistentP Weak (Φ k y)) → FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y) ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y). Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed. ... ... @@ -430,10 +430,10 @@ Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) ownM_op. Qed. Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q. Proof. done. Qed. Global Instance into_and_and_persistent_l P Q : PersistentP true P → IntoAnd false (P ∧ Q) P Q. PersistentP Weak P → IntoAnd false (P ∧ Q) P Q. Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed. Global Instance into_and_and_persistent_r P Q : PersistentP true Q → IntoAnd false (P ∧ Q) P Q. PersistentP Weak Q → IntoAnd false (P ∧ Q) P Q. Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed. Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝. ... ... @@ -736,11 +736,11 @@ Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q). Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed. Global Instance elim_modal_bupd_plain_goal P Q : PersistentP false Q → ElimModal (|==> P) P Q Q. PersistentP Strong Q → ElimModal (|==> P) P Q Q. Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_persistent. Qed. Global Instance elim_modal_bupd_plain P Q : PersistentP false P → ElimModal (|==> P) P Q Q. PersistentP Strong P → ElimModal (|==> P) P Q Q. Proof. intros. by rewrite /ElimModal bupd_persistent wand_elim_r. Qed. Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q. ... ...
 ... ... @@ -95,7 +95,7 @@ Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) : (Q1 ∧ Q2 ⊢ P) → FromAnd p P Q1 Q2. Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed. Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) : Or (PersistentP true Q1) (PersistentP true Q2) → Or (PersistentP Weak Q1) (PersistentP Weak Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2. Proof. intros [?|?] ?; rewrite /FromAnd. ... ...
 ... ... @@ -302,7 +302,7 @@ Proof. Qed. Lemma env_spatial_is_nil_persistent Δ : env_spatial_is_nil Δ = true → PersistentP true Δ. env_spatial_is_nil Δ = true → PersistentP Weak Δ. Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed. Hint Immediate env_spatial_is_nil_persistent : typeclass_instances. ... ... @@ -467,7 +467,7 @@ Lemma tac_löb Δ Δ' i Q : envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ Q. Proof. intros ?? HQ. rewrite -(always_elim true Q) -(löb (□ Q)) -always_later. intros ?? HQ. rewrite -(always_elim Weak Q) -(löb (□ Q