Add `valid_entails` to lift `✓{n}` entailments into `uPred`.

theories/base_logic/bi.v

@@ -197,7 +197,7 @@ Lemma bupd_ownM_updateP x (Φ : M → Prop) :
   x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
 Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
 
-(* This is really just a special case of an entailment
+(** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
 be replaced by the proper one eventually. *)
@@ -225,6 +225,14 @@ Proof. exact: uPred_primitive.discrete_valid. Qed.
 Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
 
+(** This is really just a special case of an entailment
+between two [siProp], but we do not have the infrastructure
+to express the more general case. This temporary proof rule will
+be replaced by the proper one eventually. *)
+Lemma valid_entails {A B : cmraT} (a : A) (b : B) :
+  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
+Proof. exact: uPred_primitive.valid_entails. Qed.
+
 (** Consistency/soundness statement *)
 Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
 Proof. apply pure_soundness. Qed.

theories/base_logic/upred.v

@@ -720,7 +720,7 @@ Proof.
   unseal=> ?. split=> n x ?. by apply (discrete_iff n).
 Qed.
 
-(* This is really just a special case of an entailment
+(** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
 be replaced by the proper one eventually. *)
@@ -818,6 +818,14 @@ Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. by unseal. Qed.
 
+(** This is really just a special case of an entailment
+between two [siProp], but we do not have the infrastructure
+to express the more general case. This temporary proof rule will
+be replaced by the proper one eventually. *)
+Lemma valid_entails {A B : cmraT} (a : A) (b : B) :
+  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
+Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
+
 (** Consistency/soundness statement *)
 (** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
 instance of [siProp] soundness in the future. *)