From 33e5782592493831be980a83fb5c79f9fa797fc9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Sep 2020 16:21:38 +0200
Subject: [PATCH] add internal_eq_entails uPred law

---
 theories/base_logic/bi.v    | 10 +++++++++-
 theories/base_logic/upred.v |  8 ++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 516274c02..1def67daf 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -180,7 +180,7 @@ Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_n
 Global Instance cmra_valid_ne {A : cmraT} : NonExpansive (@uPred_cmra_valid M A)
   := uPred_primitive.cmra_valid_ne.
 
-(** Re-exporting primitive Own and valid lemmas *)
+(** Re-exporting primitive lemmas that are not in any interface *)
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
 Proof. exact: uPred_primitive.ownM_op. Qed.
@@ -194,6 +194,14 @@ 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
+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 internal_eq_entails {A B : ofeT} (a1 a2 : A) (b1 b2 : B) :
+  (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
+Proof. exact: uPred_primitive.internal_eq_entails. Qed.
+
 Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
 Proof. exact: uPred_primitive.ownM_valid. Qed.
 Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index fe44e0323..2155c2a19 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -722,6 +722,14 @@ Proof.
   unseal=> ?. split=> n x ?. by apply (discrete_iff n).
 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 internal_eq_entails {A B : ofeT} (a1 a2 : A) (b1 b2 : B) :
+  (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
+Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
+
 (** Basic update modality *)
 Lemma bupd_intro P : P ⊢ |==> P.
 Proof.
-- 
GitLab