derive that when we obtain validity of an ownG, we can keep ownership

iris/ownership.v

@@ -55,6 +55,8 @@ Proof.
 Qed.
 Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
+Lemma ownG_valid_r m : (ownG m) ⊑ (ownG m ★ ✓ m).
+Proof. apply uPred.always_entails_r', ownG_valid; by apply _. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 

iris/viewshifts.v

@@ -19,7 +19,7 @@ Implicit Types P Q : iProp Σ.
 Implicit Types m : iGst Σ.
 Import uPred.
 
-Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q.
+Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P >{E1,E2}> Q.
 Proof.
   intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
   by rewrite always_const (right_id _ _).

modures/logic.v

@@ -433,6 +433,15 @@ Lemma impl_elim_l' P Q R : P ⊑ (Q → R) → (P ∧ Q) ⊑ R.
 Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : Q ⊑ (P → R) → (P ∧ Q) ⊑ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
+Lemma impl_entails P Q : True ⊑ (P → Q) → P ⊑ Q.
+Proof.
+  intros H; eapply impl_elim; last reflexivity. rewrite -H.
+  by apply True_intro.
+Qed.
+Lemma entails_impl P Q : (P ⊑ Q) → True ⊑ (P → Q).
+Proof.
+  intros H; apply impl_intro_l. by rewrite -H and_elim_l.
+Qed.
 
 Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
@@ -737,6 +746,26 @@ Proof.
   apply always_intro, impl_intro_r.
   by rewrite always_and_sep_l always_elim wand_elim_l.
 Qed.
+Lemma always_impl_l P Q : (P → □ Q) ⊑ (P → □ Q ★ P).
+Proof.
+  rewrite -always_and_sep_l. apply impl_intro_l, and_intro.
+  - by rewrite impl_elim_r.
+  - by rewrite and_elim_l.
+Qed.
+Lemma always_impl_r P Q : (P → □ Q) ⊑ (P → P ★ □ Q).
+Proof.
+  by rewrite commutative always_impl_l.
+Qed.
+Lemma always_entails_l P Q : (P ⊑ □ Q) → P ⊑ (□ Q ★ P).
+Proof.
+  intros H. apply impl_entails. rewrite -always_impl_l.
+  by apply entails_impl.
+Qed.
+Lemma always_entails_r P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
+Proof.
+  intros H. apply impl_entails. rewrite -always_impl_r.
+  by apply entails_impl.
+Qed.
 
 (* Own *)
 Lemma own_op (a1 a2 : M) :
@@ -909,4 +938,13 @@ Lemma always_and_sep_r' P Q `{!AlwaysStable Q} : (P ∧ Q)%I ≡ (P ★ Q)%I.
 Proof. by rewrite -(always_always Q) always_and_sep_r. Qed.
 Lemma always_sep_dup' P `{!AlwaysStable P} : P ≡ (P ★ P)%I.
 Proof. by rewrite -(always_always P) -always_sep_dup. Qed.
+Lemma always_impl_l' P Q `{!AlwaysStable Q} : (P → Q) ⊑ (P → Q ★ P).
+Proof. by rewrite -(always_always Q) always_impl_l. Qed.
+Lemma always_impl_r' P Q `{!AlwaysStable Q} : (P → Q) ⊑ (P → P ★ Q).
+Proof. by rewrite -(always_always Q) always_impl_r. Qed.
+Lemma always_entails_l' P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (Q ★ P).
+Proof. by rewrite -(always_always Q); apply always_entails_l. Qed.
+Lemma always_entails_r' P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (P ★ Q).
+Proof. by rewrite -(always_always Q); apply always_entails_r. Qed.
+
 End uPred_logic. End uPred.