From 7caec2efdb0c70647ec04b2edd54bfc75308ba36 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Sep 2016 22:32:16 +0200
Subject: [PATCH] More validity lemmas for auth.

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

diff --git a/algebra/auth.v b/algebra/auth.v
index 5e7a7633c..e8d25bfd6 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -95,9 +95,10 @@ Proof.
   split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
   intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
 Qed.
-Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x.
+
+Lemma authoritative_validN n x : ✓{n} x → ✓{n} authoritative x.
 Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_validN n (x : auth A) : ✓{n} x → ✓{n} auth_own x.
+Lemma auth_own_validN n x : ✓{n} x → ✓{n} auth_own x.
 Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
 
 Lemma auth_valid_discrete `{CMRADiscrete A} x :
@@ -111,6 +112,14 @@ Proof.
   setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
 Qed.
 
+Lemma authoritative_valid  x : ✓ x → ✓ authoritative x.
+Proof. by destruct x as [[[]|]]. Qed.
+Lemma auth_own_valid `{CMRADiscrete A} x : ✓ x → ✓ auth_own x.
+Proof.
+  rewrite auth_valid_discrete.
+  destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
+Qed.
+
 Lemma auth_cmra_mixin : CMRAMixin (auth A).
 Proof.
   apply cmra_total_mixin.
-- 
GitLab