From 64825c1c467dd9f15e5e55295ccf19976a5ee6af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 14 Jan 2022 19:16:11 -0500
Subject: [PATCH] remove auth_frac_op lemmas

---
 CHANGELOG.md                    | 3 +++
 iris/algebra/auth.v             | 2 --
 iris/algebra/lib/gmap_view.v    | 4 ----
 iris/algebra/view.v             | 2 --
 iris/base_logic/lib/ghost_map.v | 2 +-
 5 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 57a15c2fb..efce12646 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,9 @@ lemma.
   The old `to_frac_agree` and its lemmas still exist, except that the
   `frac_agree_op_valid` lemmas are made bi-directional.
 * Rename typeclass instance `Later_inj` -> `Next_inj`.
+* Remove `view_auth_frac_op`, `auth_auth_frac_op`, `gmap_view_auth_frac_op`; the
+  corresponding `dfrac` lemmas can be used instead (together with `dfrac_op_own`
+  if needed).
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 5a0aca789..00f829c2f 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -120,8 +120,6 @@ Section auth.
   (** Operation *)
   Lemma auth_auth_dfrac_op dq1 dq2 a : ●{dq1 ⋅ dq2} a ≡ ●{dq1} a ⋅ ●{dq2} a.
   Proof. apply view_auth_dfrac_op. Qed.
-  Lemma auth_auth_frac_op q1 q2 a : ●{#(q1 + q2)} a ≡ ●{#q1} a ⋅ ●{#q2} a.
-  Proof. apply view_auth_frac_op. Qed.
   Global Instance auth_auth_dfrac_is_op dq dq1 dq2 a :
     IsOp dq dq1 dq2 → IsOp' (●{dq} a) (●{dq1} a) (●{dq2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 6ebf62a34..3109af96a 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -180,10 +180,6 @@ Section lemmas.
     gmap_view_auth (dp ⋅ dq) m ≡
     gmap_view_auth dp m â‹… gmap_view_auth dq m.
   Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.
-  Lemma gmap_view_auth_frac_op p q m :
-    gmap_view_auth (DfracOwn (p + q)) m ≡
-    gmap_view_auth (DfracOwn p) m â‹… gmap_view_auth (DfracOwn q) m.
-  Proof. by rewrite /gmap_view_auth view_auth_frac_op. Qed.
   Global Instance gmap_view_auth_dfrac_is_op dq dq1 dq2 m :
     IsOp dq dq1 dq2 → IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 0d7106419..ce5b96b9c 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -275,8 +275,6 @@ Section cmra.
     intros; split; simpl; last by rewrite left_id.
     by rewrite -Some_op -pair_op agree_idemp.
   Qed.
-  Lemma view_auth_frac_op q1 q2 a : ●V{#(q1 + q2)} a ≡ ●V{#q1} a ⋅ ●V{#q2} a.
-  Proof. rewrite -dfrac_op_own. apply view_auth_dfrac_op. Qed.
   Global Instance view_auth_dfrac_is_op dq dq1 dq2 a :
     IsOp dq dq1 dq2 → IsOp' (●V{dq} a) (●V{dq1} a) (●V{dq2} a).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_dfrac_op. Qed.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index e59bb2412..ac9a1dc0f 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -157,7 +157,7 @@ Section lemmas.
   Global Instance ghost_map_auth_timeless γ q m : Timeless (ghost_map_auth γ q m).
   Proof. unseal. apply _. Qed.
   Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ q m)%I.
-  Proof. intros p q. unseal. rewrite -own_op gmap_view_auth_frac_op //. Qed.
+  Proof. intros p q. unseal. rewrite -own_op -gmap_view_auth_dfrac_op //. Qed.
   Global Instance ghost_map_auth_as_fractional γ q m :
     AsFractional (ghost_map_auth γ q m) (λ q, ghost_map_auth γ q m)%I q.
   Proof. split; first done. apply _. Qed.
-- 
GitLab