From 3e206cd015cc7151d51a7c441a0ef3cf37c30072 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Tue, 23 Feb 2021 12:06:23 +0100
Subject: [PATCH] Make changes related to dfrac generalization

---
 CHANGELOG.md                   | 18 +++++++++---------
 iris/algebra/lib/gmap_view.v   | 34 +++++++++++++++++-----------------
 iris/algebra/lib/mono_nat.v    |  6 +++---
 iris/algebra/view.v            |  2 +-
 iris/base_logic/lib/mono_nat.v |  4 ++--
 5 files changed, 32 insertions(+), 32 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8e2afeee4..c9e945414 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,11 +7,11 @@ lemma.
 
 **Changes in `algebra`:**
 
-* Authorative elements of the `view`, `auth` and `gset_bij` cameras are
-  parameterized by a [discardable fraction](iris/algebra/dfrac.v) instead of a
-  fraction. Normal fractions are now denoted `●{#q} a` and `●V{#q} a`. Lemmas
-  affected by this have been renamed such that the "frac" in their name has been
-  changed into "dfrac".
+* Generalize the authorative elements of the `view`, `auth` and `gset_bij`
+  cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v)
+  (`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted
+  `●{#q} a` and `●V{#q} a`. Lemmas affected by this have been renamed such that
+  the "frac" in their name has been changed into "dfrac".
 
 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`).
@@ -19,10 +19,10 @@ Note that the script is not idempotent, do not run it twice.
 ```
 sed -i -E -f- $(find theories -name "*.v") <<EOF
 # auth and view renames from frac to dfrac
-/\b(auth|view)_auth_frac_op\b/! s/\b(auth|view)_(auth|both)_frac_(\w*)\b/\1_\2_dfrac_\3/g
-/\bgset_bij_auth_frac/gset_bij_auth_dfrac/g
-/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
-/\bgbij_both_frac_valid\b/bij_both_dfrac_valid/g
+s/\b(auth|view)_(auth|both)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
+s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
+s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
+s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
 EOF
 ```
 
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 3dfd8fd59..7d4030207 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -176,43 +176,43 @@ Section lemmas.
   Qed.
 
   (** Composition and validity *)
-  Lemma gmap_view_auth_dfrac_op p q m :
+  Lemma gmap_view_auth_frac_op p q m :
     gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
   Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_dfrac_op. Qed.
-  Global Instance gmap_view_auth_dfrac_is_op q q1 q2 m :
+  Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
     IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
 
-  Lemma gmap_view_auth_dfrac_op_invN n p m1 q m2 :
+  Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
     ✓{n} (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡{n}≡ m2.
   Proof. apply view_auth_dfrac_op_invN. Qed.
-  Lemma gmap_view_auth_dfrac_op_inv p m1 q m2 :
+  Lemma gmap_view_auth_frac_op_inv p m1 q m2 :
     ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡ m2.
   Proof. apply view_auth_dfrac_op_inv. Qed.
-  Lemma gmap_view_auth_dfrac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
+  Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
     ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
   Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
 
-  Lemma gmap_view_auth_dfrac_valid m q : ✓ gmap_view_auth q m ↔ (q ≤ 1)%Qp.
+  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ (q ≤ 1)%Qp.
   Proof.
     rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
   Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
-  Proof. rewrite gmap_view_auth_dfrac_valid. done. Qed.
+  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
 
-  Lemma gmap_view_auth_dfrac_op_validN n q1 q2 m1 m2 :
+  Lemma gmap_view_auth_frac_op_validN n q1 q2 m1 m2 :
     ✓{n} (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡{n}≡ m2.
   Proof.
     rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_dfrac_op_valid q1 q2 m1 m2 :
+  Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
     ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ (q1 + q2 ≤ 1)%Qp ∧ m1 ≡ m2.
   Proof.
     rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_dfrac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
+  Lemma gmap_view_auth_frac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
     ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 = m2.
-  Proof. unfold_leibniz. apply gmap_view_auth_dfrac_op_valid. Qed.
+  Proof. unfold_leibniz. apply gmap_view_auth_frac_op_valid. Qed.
 
   Lemma gmap_view_auth_op_validN n m1 m2 :
     ✓{n} (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
@@ -260,7 +260,7 @@ Section lemmas.
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
   Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
 
-  Lemma gmap_view_both_dfrac_validN n q m k dq v :
+  Lemma gmap_view_both_frac_validN n q m k dq v :
     ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
       (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof.
@@ -271,8 +271,8 @@ Section lemmas.
   Lemma gmap_view_both_validN n m k dq v :
     ✓{n} (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
       ✓ dq ∧ m !! k ≡{n}≡ Some v.
-  Proof. rewrite gmap_view_both_dfrac_validN. naive_solver done. Qed.
-  Lemma gmap_view_both_dfrac_valid q m k dq v :
+  Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
+  Lemma gmap_view_both_frac_valid q m k dq v :
     ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
     (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡ Some v.
   Proof.
@@ -286,14 +286,14 @@ Section lemmas.
       + apply Hm.
       + revert n. apply equiv_dist. apply Hm.
   Qed.
-  Lemma gmap_view_both_dfrac_valid_L `{!LeibnizEquiv V} q m k dq v :
+  Lemma gmap_view_both_frac_valid_L `{!LeibnizEquiv V} q m k dq v :
     ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
     ✓ q ∧ ✓ dq ∧ m !! k = Some v.
-  Proof. unfold_leibniz. apply gmap_view_both_dfrac_valid. Qed.
+  Proof. unfold_leibniz. apply gmap_view_both_frac_valid. Qed.
   Lemma gmap_view_both_valid m k dq v :
     ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k ≡ Some v.
-  Proof. rewrite gmap_view_both_dfrac_valid. naive_solver done. Qed.
+  Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
   (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
      have [inv_L] lemmas instead that just have an equality on the RHS. *)
   Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 60d147f8a..7c5fe7e4f 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -23,7 +23,7 @@ Section mono_nat.
   Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb n).
   Proof. apply _. Qed.
 
-  Lemma mono_nat_auth_dfrac_op q1 q2 n :
+  Lemma mono_nat_auth_frac_op q1 q2 n :
     mono_nat_auth q1 n ⋅ mono_nat_auth q2 n ≡ mono_nat_auth (q1 + q2) n.
   Proof.
     rewrite /mono_nat_auth -dfrac_op_own auth_auth_dfrac_op.
@@ -57,7 +57,7 @@ Section mono_nat.
   Lemma mono_nat_auth_valid n : ✓ mono_nat_auth 1 n.
   Proof. by apply auth_both_valid. Qed.
 
-  Lemma mono_nat_auth_dfrac_op_valid q1 q2 n1 n2 :
+  Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
     ✓ (mono_nat_auth q1 n1 ⋅ mono_nat_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
   Proof.
     rewrite /mono_nat_auth (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
@@ -68,7 +68,7 @@ Section mono_nat.
   Qed.
   Lemma mono_nat_auth_op_valid n1 n2 :
     ✓ (mono_nat_auth 1 n1 ⋅ mono_nat_auth 1 n2) ↔ False.
-  Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
+  Proof. rewrite mono_nat_auth_frac_op_valid. naive_solver. Qed.
 
   Lemma mono_nat_both_frac_valid q n m :
     ✓ (mono_nat_auth q n ⋅ mono_nat_lb m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 77c636d2a..672aa04da 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -394,7 +394,7 @@ Section cmra.
     split.
     - intros [[[[dqf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [left; apply (cmra_included_l dq1)|]. apply to_agree_includedN. by exists agf.
+      + split; [left; apply: cmra_included_l|]. apply to_agree_includedN. by exists agf.
       + split; [right; done|]. by apply (inj to_agree).
     - intros [[[? ->]| ->] ->].
       + rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 46d5d9523..ba3d1cef3 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -53,7 +53,7 @@ Section mono_nat.
 
   Global Instance mono_nat_auth_own_fractional γ n :
     Fractional (λ q, mono_nat_auth_own γ q n).
-  Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_dfrac_op //. Qed.
+  Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_frac_op //. Qed.
   Global Instance mono_nat_auth_own_as_fractional γ q n :
     AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
   Proof. split; [auto|apply _]. Qed.
@@ -64,7 +64,7 @@ Section mono_nat.
     ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_dfrac_op_valid; done.
+    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_frac_op_valid; done.
   Qed.
   Lemma mono_nat_auth_own_exclusive γ n1 n2 :
     mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
-- 
GitLab