Merge branch 'ralf/auth_frac_op' into 'master'

remove auth_frac_op lemmas

See merge request iris/iris!774

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`:**
 

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.

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.

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.

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.