From 36159b492a7a1524e180a6fee5d735d597b63a8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Sep 2016 17:00:21 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20variants=20of=20CMRA=20facts=20for=20CM?=
 =?UTF-8?q?RAs=20with=20=3D=20=E2=86=94=20=E2=89=A1.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 algebra/cmra.v   | 58 ++++++++++++++++++++++++++++++++++++++++++++++++
 heap_lang/heap.v |  2 +-
 2 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index f08e33c9d..4959b78d7 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -520,6 +520,64 @@ Section ucmra.
 End ucmra.
 Hint Immediate cmra_unit_total.
 
+
+(** * Properties about CMRAs with Leibniz equality *)
+Section cmra_leibniz.
+  Context {A : cmraT} `{!LeibnizEquiv A}.
+  Implicit Types x y : A.
+
+  Global Instance cmra_assoc_L : Assoc (=) (@op A _).
+  Proof. intros x y z. unfold_leibniz. by rewrite assoc. Qed.
+  Global Instance cmra_comm_L : Comm (=) (@op A _).
+  Proof. intros x y. unfold_leibniz. by rewrite comm. Qed.
+
+  Lemma cmra_pcore_l_L x cx : pcore x = Some cx → cx ⋅ x = x.
+  Proof. unfold_leibniz. apply cmra_pcore_l'. Qed.
+  Lemma cmra_pcore_idemp_L x cx : pcore x = Some cx → pcore cx = Some cx.
+  Proof. unfold_leibniz. apply cmra_pcore_idemp'. Qed.
+
+  Lemma cmra_opM_assoc_L x y mz : (x â‹… y) â‹…? mz = x â‹… (y â‹…? mz).
+  Proof. unfold_leibniz. apply cmra_opM_assoc. Qed.
+
+  (** ** Core *)
+  Lemma cmra_pcore_r_L x cx : pcore x = Some cx → x ⋅ cx = x.
+  Proof. unfold_leibniz. apply cmra_pcore_r'. Qed.
+  Lemma cmra_pcore_dup_L x cx : pcore x = Some cx → cx = cx ⋅ cx.
+  Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
+
+  (** ** Persistent elements *)
+  Lemma persistent_dup_L x `{!Persistent x} : x ≡ x ⋅ x.
+  Proof. unfold_leibniz. by apply persistent_dup. Qed.
+
+  (** ** Total core *)
+  Section total_core.
+    Context `{CMRATotal A}.
+
+    Lemma cmra_core_r_L x : x â‹… core x = x.
+    Proof. unfold_leibniz. apply cmra_core_r. Qed.
+    Lemma cmra_core_l_L x : core x â‹… x = x.
+    Proof. unfold_leibniz. apply cmra_core_l. Qed.
+    Lemma cmra_core_idemp_L x : core (core x) = core x.
+    Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
+    Lemma cmra_core_dup_L x : core x = core x â‹… core x.
+    Proof. unfold_leibniz. apply cmra_core_dup. Qed.
+    Lemma persistent_total_L x : Persistent x ↔ core x = x.
+    Proof. unfold_leibniz. apply persistent_total. Qed.
+    Lemma persistent_core_L x `{!Persistent x} : core x = x.
+    Proof. by apply persistent_total_L. Qed.
+  End total_core.
+End cmra_leibniz.
+
+Section ucmra_leibniz.
+  Context {A : ucmraT} `{!LeibnizEquiv A}.
+  Implicit Types x y z : A.
+
+  Global Instance ucmra_unit_left_id_L : LeftId (=) ∅ (@op A _).
+  Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
+  Global Instance ucmra_unit_right_id_L : RightId (=) ∅ (@op A _).
+  Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
+End ucmra_leibniz.
+
 (** * Constructing a CMRA with total core *)
 Section cmra_total.
   Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 597066ded..58f5b6192 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -142,7 +142,7 @@ Section heap.
     iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
     iVs (auth_empty heap_name) as "Hh".
     iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
-    rewrite left_id /heap_inv. iDestruct "Hv" as %?.
+    rewrite left_id_L /heap_inv. iDestruct "Hv" as %?.
     iApply wp_alloc_pst. iFrame "Hh". iNext.
     iIntros (l) "[% Hh] !==>".
     iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").
-- 
GitLab