From f25bdcf3dadbc4e9c5a44ad61f4d494501a0c693 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Mon, 12 Jul 2021 13:30:12 +0200
Subject: [PATCH] Initial experiment with internal_eq for bi with siProp
 embedding

---
 _CoqProject                   |  1 +
 iris/base_logic/internal_eq.v | 79 +++++++++++++++++++++++++++++++++++
 2 files changed, 80 insertions(+)
 create mode 100644 iris/base_logic/internal_eq.v

diff --git a/_CoqProject b/_CoqProject
index 17a6dd76a..c512af653 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -83,6 +83,7 @@ iris/bi/lib/relations.v
 iris/base_logic/upred.v
 iris/base_logic/upred_derived.v
 iris/base_logic/cmra_valid.v
+iris/base_logic/internal_eq.v
 iris/base_logic/bi.v
 iris/base_logic/derived.v
 iris/base_logic/proofmode.v
diff --git a/iris/base_logic/internal_eq.v b/iris/base_logic/internal_eq.v
new file mode 100644
index 000000000..cb81d3cd9
--- /dev/null
+++ b/iris/base_logic/internal_eq.v
@@ -0,0 +1,79 @@
+From iris.si_logic Require Import siprop.
+From iris.si_logic Require Export bi.
+From iris.prelude Require Import options.
+
+Definition bi_internal_eq_def
+  {PROP : bi} `{BiEmbed siPropI PROP} {A : ofe} (a b : A) : PROP :=
+  ⎡ a ≡ b ⎤.
+Definition bi_internal_eq_aux : seal (@bi_internal_eq_def). Proof. by eexists. Qed.
+Definition bi_internal_eq := bi_internal_eq_aux.(unseal).
+Global Arguments bi_internal_eq {PROP _ A}.
+Definition bi_internal_eq_eq :
+  @bi_internal_eq = @bi_internal_eq_def := bi_internal_eq_aux.(seal_eq).
+
+Module bi_internal_eq.
+Ltac unseal :=
+  rewrite !bi_internal_eq_eq /bi_internal_eq_def /=.
+End bi_internal_eq.
+
+Section internal_eq_props.
+Context {PROP : bi} `{BiEmbed siPropI PROP}.
+Implicit Types (P : PROP).
+
+Local Definition unseal_eqs :=
+  (@embed_emp, @embed_pure,
+    @embed_and, @embed_or, @embed_impl, @embed_forall, @embed_exist,
+    @embed_sep, @embed_wand,
+    @embed_later).
+Local Ltac unseal_embed :=
+  bi_internal_eq.unseal;
+  rewrite -?unseal_eqs;
+  first [apply embed_ne | apply embed_proper | apply embed_mono | idtac ].
+
+Lemma internal_eq_ne (A : ofe) :
+  NonExpansive2 (@bi_internal_eq PROP _ A).
+Proof.
+  intros n x x' Hx y y' Hy. unseal_embed. exact: siProp_primitive.internal_eq_ne.
+Qed.
+
+(* Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
+Proof.
+  unseal. apply embed_mono. etrans; [apply emp_valid_and_2|apply emp_valid_siProp_internal_eq].
+Qed. *)
+
+Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ bi_internal_eq a a.
+Proof.
+  etrans; first apply bi.persistently_emp_intro.
+  rewrite embed_emp_2 -embed_persistently.
+  unseal_embed. exact: siProp_primitive.internal_eq_refl.
+Qed.
+Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
+  NonExpansive Ψ → bi_internal_eq a b ⊢ Ψ a → Ψ b.
+Proof.
+Abort.
+
+Lemma fun_ext {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
+  (∀ i, bi_internal_eq (g1 i) (g2 i)) ⊢ bi_internal_eq g1 g2.
+Proof. unseal_embed. exact: siProp_primitive.fun_ext. Qed.
+Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
+  bi_internal_eq (proj1_sig x) (proj1_sig y) ⊢ bi_internal_eq x y.
+Proof. unseal_embed. exact: siProp_primitive.sig_eq. Qed.
+
+Lemma later_eq_1 `{BiEmbedLater siPropI PROP} {A : ofe} (x y : A) :
+  bi_internal_eq (Next x) (Next y) ⊢ ▷ (bi_internal_eq x y).
+Proof. unseal_embed. exact: siProp_primitive.later_eq_1. Qed.
+Lemma later_eq_2 `{BiEmbedLater siPropI PROP} {A : ofe} (x y : A) :
+  ▷ (bi_internal_eq x y) ⊢ bi_internal_eq (Next x) (Next y).
+Proof. unseal_embed. exact: siProp_primitive.later_eq_2. Qed.
+
+Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → bi_internal_eq a b ⊢ ⌜a ≡ b⌝.
+Proof. intros. unseal_embed. exact: siProp_primitive.discrete_eq_1. Qed.
+
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+  (a1 ≡ a2 ⊢@{siPropI} b1 ≡ b2) → bi_internal_eq a1 a2 ⊢ bi_internal_eq b1 b2.
+Proof. intros. by unseal_embed. Qed.
+
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢ bi_internal_eq x y) → x ≡ y.
+Proof. unseal_embed. intros ?%embed_emp_valid_inj. exact: siProp_primitive.internal_eq_soundness. Qed.
+
+End internal_eq_props.
-- 
GitLab