From 89ce6ae2525f27cdd2c7fe92540ec3179de6a12f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Jul 2016 01:21:48 +0200
Subject: [PATCH] Local update for discrete CMRAs.

---
 algebra/updates.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/algebra/updates.v b/algebra/updates.v
index 36851cff2..c856ab53e 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -79,6 +79,19 @@ Proof.
   intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
 Qed.
 
+(** ** Local updates for discrete CMRAs *)
+Lemma local_update_total `{CMRADiscrete A} x y mz :
+  x ~l~> y @ mz ↔
+    (✓ (x ⋅? mz) → ✓ (y ⋅? mz)) ∧
+    (∀ mz', ✓ (x ⋅? mz) → x ⋅? mz ≡ x ⋅? mz' → y ⋅? mz ≡ y ⋅? mz').
+Proof.
+  split.
+  - destruct 1. split; intros until 0;
+      rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto.
+  - intros [??]; split; intros until 0;
+      rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto.
+Qed.
+
 (** ** Frame preserving updates *)
 Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
 Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
-- 
GitLab