From 98c99c79cfa4bf48ff7388be7ff2b29e200b5a8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Jul 2022 09:59:30 +0200
Subject: [PATCH] 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.

---
 iris/algebra/lib/frac_auth.v  | 16 ++++++----------
 iris/algebra/lib/ufrac_auth.v |  4 ++--
 2 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 882d480fb..4ea484de6 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -92,16 +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.
-    pose proof (Qp_not_add_le_l 1 q); tauto.
-  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.
-    pose proof (Qp_not_add_le_l 1 q); tauto.
-  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 d577614c7..6617975b9 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.
-- 
GitLab