From 39a5e48f3dc7185ae7b9f2c26f02d45fb76ff7db Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Jun 2017 14:05:56 +0200
Subject: [PATCH] More frac_auth stuff.

---
 theories/algebra/frac_auth.v | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 5d05d246e..7f7b195a1 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -84,6 +84,11 @@ Section frac_auth.
   Lemma frag_auth_op q1 q2 a1 a2 : ◯!{q1+q2} (a1 ⋅ a2) ≡ ◯!{q1} a1 ⋅ ◯!{q2} a2.
   Proof. done. Qed.
 
+  Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯!{1} a ⋅ ◯!{q} b) → False.
+  Proof. rewrite -frag_auth_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
+  Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯!{1} a ⋅ ◯!{q} b) → False.
+  Proof. rewrite -frag_auth_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
+
   Global Instance into_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
     IntoOp q q1 q2 → IntoOp a a1 a2 → IntoOp (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
   Proof. by rewrite /IntoOp=> /leibniz_equiv_iff -> ->. Qed.
@@ -92,15 +97,15 @@ Section frac_auth.
   Proof. by rewrite /FromOp=> /leibniz_equiv_iff <- <-. Qed.
 
   Global Instance into_op_frac_auth_persistent (q q1 q2 : frac) (a  : A) :
-    IntoOp q q1 q2 → Persistent a → IntoOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
+    Persistent a → IntoOp q q1 q2 → IntoOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
   Proof.
-    rewrite /IntoOp=> /leibniz_equiv_iff -> ?.
+    rewrite /IntoOp=> ? /leibniz_equiv_iff ->.
     by rewrite -frag_auth_op -persistent_dup.
   Qed.
   Global Instance from_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
-    FromOp q q1 q2 → Persistent a → FromOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
+    Persistent a → FromOp q q1 q2 → FromOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
   Proof.
-    rewrite /FromOp=> /leibniz_equiv_iff <- ?.
+    rewrite /FromOp=> ? /leibniz_equiv_iff <-.
     by rewrite -frag_auth_op -persistent_dup.
   Qed.
 
-- 
GitLab