From 04d0796ddef64034fe62deb570b6d8be12be772f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 14:08:37 +0100
Subject: [PATCH] show some dec_agree properties

---
 algebra/dec_agree.v | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 3adbb7eef..5931c648a 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -48,4 +48,20 @@ Qed.
 
 Canonical Structure dec_agreeRA : cmraT := discreteRA dec_agree_ra.
 
-End dec_agree.
\ No newline at end of file
+(* Some properties of this CMRA *)
+Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x ≡ x.
+Proof.
+  destruct x as [x|]; simpl; repeat (case_match; simpl); try subst; congruence.
+Qed.
+
+Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 ≡ x2.
+Proof.
+  destruct x1 as [x1|], x2 as [x2|]; simpl;repeat (case_match; simpl); by subst.
+Qed.
+
+Lemma dec_agree_equivI {M} a b : (DecAgree a ≡ DecAgree b)%I ≡ (a = b : uPred M)%I.
+Proof. split. by case. by destruct 1. Qed.
+Lemma dec_agree_validI {M} (x y : dec_agreeRA) : ✓ (x ⋅ y) ⊑ (x = y : uPred M).
+Proof. intros r n _ ?. by apply: dec_agree_op_inv. Qed.
+
+End dec_agree.
-- 
GitLab