From f70294b1e7ffc813143247656454def490d1b259 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2016 23:36:52 +0200
Subject: [PATCH] Prove equivalent more useful def of valid on auth A when A is
 discrete.

---
 algebra/auth.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/algebra/auth.v b/algebra/auth.v
index 4ae474849..366e85231 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -100,6 +100,17 @@ Proof. by destruct x as [[[]|]]. Qed.
 Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x.
 Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
 
+Lemma auth_valid_discrete `{CMRADiscrete A} x :
+  ✓ x ↔ match authoritative x with
+        | Excl' a => own x ≼ a ∧ ✓ a
+        | None => ✓ own x
+        | ExclBot' => False
+        end.
+Proof.
+  destruct x as [[[?|]|] ?]; simpl; try done.
+  setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
+Qed.
+
 Lemma auth_cmra_mixin : CMRAMixin (auth A).
 Proof.
   apply cmra_total_mixin.
-- 
GitLab