From 646e26fabdd1f1e1ce90c228211c1796a67622ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Oct 2020 11:18:46 +0200
Subject: [PATCH] =?UTF-8?q?Add=20`valid=5Fentails`=20to=20lift=20`?=
 =?UTF-8?q?=E2=9C=93{n}`=20entailments=20into=20`uPred`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/bi.v    | 10 +++++++++-
 theories/base_logic/upred.v | 10 +++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 261641c77..8f86b9c02 100644
--- a/theories/base_logic/bi.v
+++ b/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.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 9c836e3b3..44a5aaea8 100644
--- a/theories/base_logic/upred.v
+++ b/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. *)
-- 
GitLab