From 979b6b5bb862d267306b3fc4cb16f7d346c548f9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Feb 2016 23:02:59 +0100
Subject: [PATCH] Transport an equality between CMRAs.

---
 algebra/cmra.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 84f6ea449..75c088480 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -393,6 +393,35 @@ Section cmra_monotone.
   Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
 End cmra_monotone.
 
+(** * Transporting a CMRA equality *)
+Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
+  eq_rect A id x _ H.
+
+Section cmra_transport.
+  Context {A B : cmraT} (H : A = B).
+  Notation T := (cmra_transport H).
+  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
+  Proof. by intros ???; destruct H. Qed.
+  Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
+  Proof. by intros ???; destruct H. Qed.
+  Lemma cmra_transport_op x y : T (x â‹… y) = T x â‹… T y.
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_unit x : T (unit x) = unit (T x).
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x.
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_valid x : ✓ (T x) ↔ ✓ x.
+  Proof. by destruct H. Qed.
+  Global Instance cmra_transport_timeless x : Timeless x → Timeless (T x).
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
+    x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
+  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
+  Lemma cmra_transport_updateP' (P : A → Prop) x :
+    x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
+  Proof. eauto using cmra_transport_updateP. Qed.
+End cmra_transport.
+
 (** * Instances *)
 (** ** Discrete CMRA *)
 Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
-- 
GitLab