From a3885d05d0c192b4018e93b9960d9b37f7f70f47 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Wed, 11 Oct 2023 11:45:26 +0200
Subject: [PATCH] Need to upstream an id_freeI lemma

---
 iris/base_logic/algebra.v                   | 19 +++++++++++++++++-
 iris/base_logic/lib/combine_own_instances.v | 22 +++------------------
 2 files changed, 21 insertions(+), 20 deletions(-)

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index c33e5b8fd..e569a7ce6 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -12,7 +12,7 @@ Section upred.
   (* Force implicit argument M *)
   Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
   Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-  Notation "⊢ Q" := (bi_entails (PROP:=uPredI M) True Q).
+  Notation "⊢ Q" := (bi_emp_valid (PROP:=uPredI M) Q).
 
   Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
   Proof. by uPred.unseal. Qed.
@@ -23,6 +23,23 @@ Section upred.
     ✓ g ⊣⊢ ∀ i, ✓ g i.
   Proof. by uPred.unseal. Qed.
 
+  (* Analogues of [id_freeN_l] and [id_freeN_r] in the logic, stated in a way
+    that allows us to do [iDestruct (id_freeI_r with "H✓ H≡") as %[]]*)
+  Lemma id_freeI_r {A : cmra} (x y : A) :
+    IdFree x → ⊢ ✓ x -∗ (x ⋅ y) ≡ x -∗ False.
+  Proof.
+    intros HIdFree. apply bi.wand_intro_l. rewrite bi.sep_and right_id.
+    apply bi.wand_intro_r. rewrite bi.sep_and.
+    uPred.unseal. split => n m Hm. case. by apply id_freeN_r.
+  Qed.
+  Lemma id_freeI_l {A : cmra} (x y : A) :
+    IdFree x → ⊢ ✓ x -∗ (y ⋅ x) ≡ x -∗ False.
+  Proof.
+    intros HIdFree. apply bi.wand_intro_l. rewrite bi.sep_and right_id.
+    apply bi.wand_intro_r. rewrite bi.sep_and.
+    uPred.unseal. split => n m Hm. case. by apply id_freeN_l.
+  Qed.
+
   Section gmap_ofe.
     Context `{Countable K} {A : ofe}.
     Implicit Types m : gmap K A.
diff --git a/iris/base_logic/lib/combine_own_instances.v b/iris/base_logic/lib/combine_own_instances.v
index 767be9f16..4948cf806 100644
--- a/iris/base_logic/lib/combine_own_instances.v
+++ b/iris/base_logic/lib/combine_own_instances.v
@@ -9,23 +9,6 @@ Set Default Proof Using "Type".
 (** We start with some general lemmas and [Proper] instances for constructing
   instances of the [IsValidGives], [IsValidOp], [IsIncluded] and 
   [IsIncludedOrEq] classes. *)
-
-Section included_upred.
-  Context {M : ucmra}.
-  Implicit Type A : cmra.
-  Notation "P ⊢ Q" := (P ⊢@{uPredI M} Q).
-  Notation "P ⊣⊢ Q" := (P ⊣⊢@{uPredI M} Q).
-
-  (** TODO: Move to !944. I dont think this can be proven inside the model. *)
-  Lemma internal_included_id_free {A} (a : A) `{!IdFree a} : a ≼ a ∗ ✓ a ⊢ False.
-  Proof.
-    iIntros "[[%c Hc] Hv]". iStopProof. rewrite bi.sep_and.
-    split => n x Hx. uPred.unseal. repeat rewrite /uPred_holds /=.
-    move => [He Hv]. by eapply id_freeN_r.
-  Qed.
-End included_upred.
-
-
 Section proper.
   Context {M : ucmra} {A : cmra}.
   Implicit Types a : A.
@@ -182,8 +165,9 @@ Section cmra_instances.
   Proof.
     split; last eauto 10.
     rewrite /IsIncluded; iIntros "#H✓". iSplit; last eauto.
-    iIntros "H≼".
-    iDestruct (internal_included_id_free with "[$]") as "[]".
+    iIntros "[%z Hz]".
+    iDestruct (id_freeI_r with "H✓ [Hz]") as %[].
+    by iApply internal_eq_sym.
   Qed.
 
   (* If no better [IsIncludedOrEq] instance is found, build it the stupid way *)
-- 
GitLab