From 7ff76b3c55b23ecbdb82e3681dc265ff11870bbc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Jun 2022 08:46:51 +0200
Subject: [PATCH] CHANGELOG entry.
---
CHANGELOG.md | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index c9c805bb5..6d18df9ce 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,17 @@ lemma.
* Add some missing algebra functors: `dfrac_agreeRF`, `excl_authURF`, `excl_authRF`,
`frac_authURF`, `frac_authRF`, `ufrac_authURF`, `ufrac_authRF`, `max_prefix_listURF`,
`max_prefix_listRF`, `mono_listURF`, and `mono_listRF`.
+* Make validy lemmas for `excl_auth` more consistent with `auth`.
+ - Rename `excl_auth_frag_validN_op_1_l` into `excl_auth_frag_op_validN` and
+ `excl_auth_frag_valid_op_1_l` into `excl_auth_frag_op_valid` (similar to
+ `auth_auth_op_valid`), and make them bi-implications.
+ - Add `excl_auth_auth_op_validN` and `excl_auth_auth_op_valid`.
+* Make validy lemmas for `(u)frac_auth` more consistent with `auth`.
+ - Remove unidirectional lemmas with `1` fraction `frac_auth_frag_validN_op_1_l`
+ and `frac_auth_frag_valid_op_1_l`
+ - Add `frac_auth_frag_op_validN` and `frac_auth_frag_op_valid`, which are
+ bi-implications with arbitrary fractions.
+ - Add `ufrac_auth_frag_op_validN` and `ufrac_auth_frag_op_valid`.
**Changes in `bi`:**
@@ -101,6 +112,17 @@ lemma.
+ `heap_total` provides the additional assumption `HasNoLc`, which needs to be
introduced by clients and needs to be kept around to use the laws in `BiFUpdPlainly`.
+The following `sed` script helps adjust your code to the renaming (on macOS,
+replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# excl_auth
+s/\bexcl_auth_frag_validN_op_1_l\b/excl_auth_frag_op_validN/g
+s/\bexcl_auth_frag_valid_op_1_l\b/excl_auth_frag_op_valid/g
+EOF
+```
+
## Iris 3.6.0 (2022-01-22)
The highlights and most notable changes of this release are:
--
GitLab