From ad579807ceb232c4f04e9d7e7df49ac0e13c5559 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 14 Jan 2022 19:24:10 -0500
Subject: [PATCH] remove _frac_ lemmas, the corresponding _dfrac_ lemmas are
 sufficient

---
 iris/algebra/lib/mono_list.v        | 12 ------------
 iris_staging/base_logic/mono_list.v |  4 ++--
 2 files changed, 2 insertions(+), 14 deletions(-)

diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index dedbe3942..60679ecfe 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -58,9 +58,6 @@ Section mono_list_props.
     rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (â—¯ _)).
   Qed.
-  Lemma mono_list_auth_frac_op q1 q2 l :
-    ●ML{#(q1 + q2)} l ≡ ●ML{#q1} l ⋅ ●ML{#q2} l.
-  Proof. by rewrite -mono_list_auth_dfrac_op dfrac_op_own. Qed.
 
   Lemma mono_list_lb_op_l l1 l2 : l1 `prefix_of` l2 → ◯ML l1 ⋅ ◯ML l2 ≡ ◯ML l2.
   Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.
@@ -101,9 +98,6 @@ Section mono_list_props.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
       naive_solver apply to_max_prefix_list_validN.
   Qed.
-  Lemma mono_list_auth_frac_op_validN n q1 q2 l1 l2 :
-    ✓{n} (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 ≡{n}≡ l2.
-  Proof. by apply mono_list_auth_dfrac_op_validN. Qed.
   Lemma mono_list_auth_op_validN n l1 l2 : ✓{n} (●ML l1 ⋅ ●ML l2) ↔ False.
   Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.
 
@@ -113,18 +107,12 @@ Section mono_list_props.
     rewrite cmra_valid_validN equiv_dist.
     setoid_rewrite mono_list_auth_dfrac_op_validN. naive_solver eauto using O.
   Qed.
-  Lemma mono_list_auth_frac_op_valid q1 q2 l1 l2 :
-    ✓ (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 ≡ l2.
-  Proof. by apply mono_list_auth_dfrac_op_valid. Qed.
   Lemma mono_list_auth_op_valid l1 l2 : ✓ (●ML l1 ⋅ ●ML l2) ↔ False.
   Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
 
   Lemma mono_list_auth_dfrac_op_valid_L `{!LeibnizEquiv A} dq1 dq2 l1 l2 :
     ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 = l2.
   Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.
-  Lemma mono_list_auth_frac_op_valid_L `{!LeibnizEquiv A} q1 q2 l1 l2 :
-    ✓ (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 = l2.
-  Proof. unfold_leibniz. apply mono_list_auth_frac_op_valid. Qed.
 
   Lemma mono_list_both_dfrac_validN n dq l1 l2 :
     ✓{n} (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡{n}≡ l2 ++ l.
diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v
index f410dd857..ec4ffa575 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -73,7 +73,7 @@ Section mono_list_own.
 
   Global Instance mono_list_auth_own_fractional γ l :
     Fractional (λ q, mono_list_auth_own γ q l).
-  Proof. unseal. intros p q. by rewrite -own_op mono_list_auth_frac_op. Qed.
+  Proof. unseal. intros p q. by rewrite -own_op -mono_list_auth_dfrac_op. Qed.
   Global Instance mono_list_auth_own_as_fractional γ q l :
     AsFractional (mono_list_auth_own γ q l) (λ q, mono_list_auth_own γ q l) q.
   Proof. split; [auto|apply _]. Qed.
@@ -84,7 +84,7 @@ Section mono_list_own.
     ⌜(q1 + q2 ≤ 1)%Qp ∧ l1 = l2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_frac_op_valid_L.
+    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_dfrac_op_valid_L.
   Qed.
   Lemma mono_list_auth_own_exclusive γ l1 l2 :
     mono_list_auth_own γ 1 l1 -∗ mono_list_auth_own γ 1 l2 -∗ False.
-- 
GitLab