From dfdb0afefe570e9ef503b7f763e3fad041c0e80a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Sep 2019 08:04:10 +0200
Subject: [PATCH] Soundness lemma for internal equality of `uPred`.

---
 theories/base_logic/bi.v    | 3 +++
 theories/base_logic/upred.v | 8 ++++++++
 2 files changed, 11 insertions(+)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 7c86fd444..1f47dcf15 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -209,6 +209,9 @@ Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
 Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
 Proof. apply pure_soundness. Qed.
 
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Proof. apply internal_eq_soundness. Qed.
+
 Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
 Proof. apply later_soundness. Qed.
 (** See [derived.v] for a similar soundness result for basic updates. *)
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b2bf5f05c..6d4df735c 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -800,9 +800,17 @@ Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g 
 Proof. by unseal. Qed.
 
 (** Consistency/soundness statement *)
+(** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
+instance of [siProp] soundness in the future. *)
 Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
 Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
 
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Proof.
+  unseal=> -[H]. apply equiv_dist=> n.
+  by apply (H n ε); eauto using ucmra_unit_validN.
+Qed.
+
 Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
 Proof.
   unseal=> -[HP]; split=> n x Hx _.
-- 
GitLab