From 9814fac11e48700c117a78decc25de62191d9750 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 27 Sep 2020 10:03:40 +0200
Subject: [PATCH] Fix direction of `auth_auth_validN` to make it consistent
 with other lemmas.

For example, `auth_auth_valid`.
---
 CHANGELOG.md            | 2 ++
 theories/algebra/auth.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1c7314b97..a6567f7ae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,8 @@ With this release, we dropped support for Coq 8.9.
   (`iso_cmra_mixin_restrict`) and through an isomorphism (`iso_cmra_mixin`).
 * Add a `frac_agree` library which encapsulates `frac * agree A` for some OFE
   `A`, and provides some useful lemmas.
+* Fix direction of `auth_auth_validN` to make it consistent with similar lemmas,
+  e.g., `auth_auth_valid`. The direction is now `✓{n} (● a) ↔ ✓{n} a`.
 
 **Changes in `proofmode`:**
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 647bf0116..a29d6068a 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -162,7 +162,7 @@ Proof.
   - by intros [?[->%(inj to_agree) []]].
   - naive_solver eauto using ucmra_unit_leastN.
 Qed.
-Lemma auth_auth_validN n a : ✓{n} a ↔ ✓{n} (● a).
+Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
 Proof.
   rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
 Qed.
-- 
GitLab