From 8e9c3db765c01a7394f667c0a15fd95babbecf26 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Oct 2020 16:48:04 +0200
Subject: [PATCH] Add all versions of `auth_frag_frag_valid`.

---
 theories/algebra/auth.v | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 8786d7f07..8e323595a 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -106,10 +106,14 @@ Section auth.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
   Lemma auth_frag_validN n b : ✓{n} (◯ b) ↔ ✓{n} b.
   Proof. by rewrite view_frag_validN auth_view_rel_exists. Qed.
-  (** Stated as an implication (instead of a bi-implication) to force [apply] to
-  use the lemma in the right direction. *)
-  Lemma auth_frag_frag_validN_1 n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) → ✓{n} (b1 ⋅ b2).
+  (** Also stated as implications, which can be used to force [apply] to use the
+  lemma in the right direction. *)
+  Lemma auth_frag_frag_validN n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) ↔ ✓{n} (b1 ⋅ b2).
   Proof. apply auth_frag_validN. Qed.
+  Lemma auth_frag_frag_validN_1 n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) → ✓{n} (b1 ⋅ b2).
+  Proof. apply auth_frag_frag_validN. Qed.
+  Lemma auth_frag_frag_validN_2 n b1 b2 : ✓{n} (b1 ⋅ b2) → ✓{n} (◯ b1 ⋅ ◯ b2).
+  Proof. apply auth_frag_frag_validN. Qed.
 
   Lemma auth_both_frac_validN n q a b :
     ✓{n} (●{q} a ⋅ ◯ b) ↔ ✓{n} q ∧ b ≼{n} a ∧ ✓{n} a.
@@ -132,10 +136,14 @@ Section auth.
     rewrite view_frag_valid cmra_valid_validN.
     by setoid_rewrite auth_view_rel_exists.
   Qed.
-  (** Stated as an implication (instead of a bi-implication) to force [apply] to
-  use the lemma in the right direction. *)
-  Lemma auth_frag_frag_valid_1 b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) → ✓ (b1 ⋅ b2).
+  (** Also stated as implications, which can be used to force [apply] to use the
+  lemma in the right direction. *)
+  Lemma auth_frag_frag_valid b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) ↔ ✓ (b1 ⋅ b2).
   Proof. apply auth_frag_valid. Qed.
+  Lemma auth_frag_frag_valid_1 b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) → ✓ (b1 ⋅ b2).
+  Proof. apply auth_frag_frag_valid. Qed.
+  Lemma auth_frag_frag_valid_2 b1 b2 : ✓ (b1 ⋅ b2) → ✓ (◯ b1 ⋅ ◯ b2).
+  Proof. apply auth_frag_frag_valid. Qed.
 
   (** These lemma statements are a bit awkward as we cannot possibly extract a
   single witness for [b ≼ a] from validity, we have to make do with one witness
-- 
GitLab