More now_True laws.

algebra/upred.v

@@ -1141,6 +1141,9 @@ Lemma now_True_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
 Proof. by intros ->. Qed.
 Lemma now_True_idemp P : ◇ ◇ P ⊢ ◇ P.
 Proof. rewrite /uPred_now_True; auto. Qed.
+
+Lemma now_True_True : ◇ True ⊣⊢ True.
+Proof. rewrite /uPred_now_True. apply (anti_symm _); auto. Qed.
 Lemma now_True_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
 Proof. rewrite /uPred_now_True. apply (anti_symm _); auto. Qed.
 Lemma now_True_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
@@ -1160,6 +1163,8 @@ Lemma now_True_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /uPred_now_True -later_or False_or. Qed.
 Lemma now_True_always P : ◇ □ P ⊣⊢ □ ◇ P.
 Proof. by rewrite /uPred_now_True always_or always_later always_pure. Qed.
+Lemma now_True_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
+Proof. destruct p; simpl; auto using now_True_always. Qed.
 Lemma now_True_frame_l P Q : P ★ ◇ Q ⊢ ◇ (P ★ Q).
 Proof. by rewrite {1}(now_True_intro P) now_True_sep. Qed.
 Lemma now_True_frame_r P Q : ◇ P ★ Q ⊢ ◇ (P ★ Q).
@@ -1238,6 +1243,11 @@ Proof.
   exists (y ⋅ x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
+Lemma now_True_rvs P : ◇ (|=r=> ◇ P) ⊢ (|=r=> ◇ P).
+Proof.
+  rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
+  by rewrite -rvs_intro -or_intro_l.
+Qed.
 
 (** * Derived rules *)
 Global Instance rvs_mono' : Proper ((⊢) ==> (⊢)) (@uPred_rvs M).

proofmode/class_instances.v

@@ -272,10 +272,8 @@ Proof.
 Qed.
 
 Class MakeNowTrue (P Q : uPred M) := make_now_True : ◇ P ⊣⊢ Q.
-Global Instance make_now_True_true : MakeNowTrue True True.
-Proof.
-  rewrite /MakeNowTrue /uPred_now_True. apply (anti_symm _); auto with I.
-Qed.
+Global Instance make_now_True_True : MakeNowTrue True True.
+Proof. by rewrite /MakeNowTrue now_True_True. Qed.
 Global Instance make_now_True_default P : MakeNowTrue P (◇ P) | 100.
 Proof. done. Qed.