diff --git a/CHANGELOG.md b/CHANGELOG.md
index 73255a411bffab5cbc150482251201c8764ed16d..68d579c4d39b805956dc21340011a5c7ad836513 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`:**
@@ -110,6 +121,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:
diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index da52b48cc41ad090b81ba08c6bb4b6ab363ff217..f947a7cb8e51582000df0d3c532e0c5628ce5ddb 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -59,9 +59,14 @@ Section excl_auth.
Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (â—E a â‹… â—¯E b) → a = b.
Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
- Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
+ Lemma excl_auth_auth_op_validN n a b : ✓{n} (â—E a â‹… â—E b) ↔ False.
+ Proof. apply auth_auth_op_validN. Qed.
+ Lemma excl_auth_auth_op_valid a b : ✓ (â—E a â‹… â—E b) ↔ False.
+ Proof. apply auth_auth_op_valid. Qed.
+
+ Lemma excl_auth_frag_op_validN n a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
- Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
+ Lemma excl_auth_frag_op_valid a b : ✓ (◯E a ⋅ ◯E b) ↔ False.
Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
Lemma excl_auth_update a b a' : â—E a â‹… â—¯E b ~~> â—E a' â‹… â—¯E a'.
diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 412ada8e4ba9fe1f3bc714f33d8ad3eb8112009c..4ea484de6a034860b08f3ae07ba3feca4f009143 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -92,10 +92,12 @@ Section frac_auth.
Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
Proof. done. Qed.
- Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False.
- Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/Qp_not_add_le_l []]. Qed.
- Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False.
- Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/Qp_not_add_le_l []]. Qed.
+ Lemma frac_auth_frag_op_validN n q1 q2 a b :
+ ✓{n} (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓{n} (a ⋅ b).
+ Proof. by rewrite -frac_auth_frag_op frac_auth_frag_validN. Qed.
+ Lemma frac_auth_frag_op_valid q1 q2 a b :
+ ✓ (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓ (a ⋅ b).
+ Proof. by rewrite -frac_auth_frag_op frac_auth_frag_valid. Qed.
Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index d577614c7d5312097cfb22edeef643551556c338..f967c538718ea555b419f206db2f83d6a0551850 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -13,8 +13,8 @@ difference:
✓ (a â‹… b) → â—U_p a ~~> â—U_(p + q) (a â‹… b) â‹… â—¯U_q b
>>
-- We no longer have the [â—¯U{1} a] is the exclusive fragmental element (cf.
- [frac_auth_frag_validN_op_1_l]).
+- We no longer have the [â—¯U_1 a] is an exclusive fragmental element. That is,
+ while [â—¯F{1} a â‹… â—¯F{q} b] is vacuously false, [â—¯U_1 a â‹… â—¯U_q2 b] is not.
*)
From iris.algebra Require Export auth frac updates local_updates.
From iris.algebra Require Import ufrac proofmode_classes.
@@ -118,6 +118,13 @@ Section ufrac_auth.
Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U_(q1+q2) (a1 ⋅ a2) ≡ ◯U_q1 a1 ⋅ ◯U_q2 a2.
Proof. done. Qed.
+ Lemma ufrac_auth_frag_op_validN n q1 q2 a b :
+ ✓{n} (◯U_q1 a ⋅ ◯U_q2 b) ↔ ✓{n} (a ⋅ b).
+ Proof. by rewrite -ufrac_auth_frag_op ufrac_auth_frag_validN. Qed.
+ Lemma ufrac_auth_frag_op_valid q1 q2 a b :
+ ✓ (◯U_q1 a ⋅ ◯U_q2 b) ↔ ✓ (a ⋅ b).
+ Proof. by rewrite -ufrac_auth_frag_op ufrac_auth_frag_valid. Qed.
+
Global Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U_q a) (◯U_q1 a1) (◯U_q2 a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index d467e21f5d564c77fc34db7291216b41c7f33b04..c7ec1a2dd42dc035cab04b6e9f67da0bdee5ed3d 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -100,7 +100,7 @@ Section lifting.
Qed.
Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
Proof.
- rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_valid_op_1_l).
+ rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_op_valid).
Qed.
Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
Proof. rewrite /ownP; apply _. Qed.