persistently rules

theories/base_logic/derived.v

@@ -579,7 +579,10 @@ Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed.
 Lemma plainly_laterN n P : ■ ▷^n P ⊣⊢ ▷^n ■ P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. Qed.
 
-(* Always derived *)
+(* Persistently derived *)
+Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros HPQ. apply persistently_intro'. rewrite <-HPQ. exact: persistently_elim. Qed.
+
 Hint Resolve persistently_mono persistently_elim.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M).
 Proof. intros P Q; apply persistently_mono. Qed.
@@ -587,10 +590,8 @@ Global Instance persistently_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@uPred_persistently M).
 Proof. intros P Q; apply persistently_mono. Qed.
 
-Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros <-. apply persistently_idemp_2. Qed.
 Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
-Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
+Proof. apply (anti_symm _); auto using persistently_intro'. Qed.
 
 Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. by rewrite -plainly_pure persistently_plainly. Qed.

theories/base_logic/primitive.v

@@ -446,16 +446,18 @@ Proof.
     split; eapply HPQ; eauto using @ucmra_unit_least.
 Qed.
 
-(* Always *)
-Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
+(* Persistently *)
+Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Proof.
+  unseal. intros HPQ; split=> n x ? /= HP.
+  apply HPQ; first by apply cmra_core_validN.
+  simpl. rewrite cmra_core_idemp. done.
+Qed.
 Lemma persistently_elim P : □ P ⊢ P.
 Proof.
   unseal; split=> n x ? /=.
   eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
 Qed.
-Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
-Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
 Proof. by unseal. Qed.