Merge branch 'robbert/internal_eq_soundness' into 'master'

Soundness lemma for internal equality of `uPred`.

See merge request iris/iris!315

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. *)

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 _.