Merge branch 'ralf/ufrac' into 'master'

ufrac_auth: don't use curly braces for fractions since these are different

See merge request iris/iris!758

CHANGELOG.md

@@ -13,6 +13,9 @@ lemma.
   [discardable fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction
   (`frac`). Lemmas affected by this have been renamed such that the "frac" in
   their name has been changed into "dfrac". (by Simon Friis Vindum)
+* Change `ufrac_auth` notation to not use curly braces, since these fractions do
+  not behave like regular fractions (and cannot be made `dfrac`).
+  Old: `●U{q} a`, `◯U{q} b`; new: `●U_q a`, `◯U_q b`.
 
 **Changes in `bi`:**
 

iris/algebra/lib/ufrac_auth.v

@@ -10,7 +10,7 @@ difference:
   and allocate a new fragment.
 
   <<<
-  ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b
+  ✓ (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.
@@ -42,8 +42,8 @@ Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
 Global Instance: Params (@ufrac_auth_auth) 2 := {}.
 Global Instance: Params (@ufrac_auth_frag) 2 := {}.
 
-Notation "●U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●U{ q }  a").
-Notation "◯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯U{ q }  a").
+Notation "●U_ q a" := (ufrac_auth_auth q a) (at level 10, q at level 9, format "●U_ q  a").
+Notation "◯U_ q a" := (ufrac_auth_frag q a) (at level 10, q at level 9, format "◯U_ q  a").
 
 Section ufrac_auth.
   Context {A : cmra}.
@@ -58,86 +58,86 @@ Section ufrac_auth.
   Global Instance ufrac_auth_frag_proper q : Proper ((≡) ==> (≡)) (@ufrac_auth_frag A q).
   Proof. solve_proper. Qed.
 
-  Global Instance ufrac_auth_auth_discrete q a : Discrete a → Discrete (●U{q} a).
+  Global Instance ufrac_auth_auth_discrete q a : Discrete a → Discrete (●U_q a).
   Proof. intros. apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
-  Global Instance ufrac_auth_frag_discrete q a : Discrete a → Discrete (◯U{q} a).
+  Global Instance ufrac_auth_frag_discrete q a : Discrete a → Discrete (◯U_q a).
   Proof. intros. apply auth_frag_discrete; apply Some_discrete; apply _. Qed.
 
-  Lemma ufrac_auth_validN n a p : ✓{n} a → ✓{n} (●U{p} a ⋅ ◯U{p} a).
+  Lemma ufrac_auth_validN n a p : ✓{n} a → ✓{n} (●U_p a ⋅ ◯U_p a).
   Proof. by rewrite auth_both_validN. Qed.
-  Lemma ufrac_auth_valid p a : ✓ a → ✓ (●U{p} a ⋅ ◯U{p} a).
+  Lemma ufrac_auth_valid p a : ✓ a → ✓ (●U_p a ⋅ ◯U_p a).
   Proof. intros. by apply auth_both_valid_2. Qed.
 
-  Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U{p} a ⋅ ◯U{p} b) → a ≡{n}≡ b.
+  Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U_p a ⋅ ◯U_p b) → a ≡{n}≡ b.
   Proof.
     rewrite auth_both_validN=> -[/Some_includedN [[_ ? //]|Hincl] _].
     move: Hincl=> /pair_includedN=> -[/ufrac_included Hincl _].
     by destruct (irreflexivity (<)%Qp p).
   Qed.
-  Lemma ufrac_auth_agree p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a ≡ b.
+  Lemma ufrac_auth_agree p a b : ✓ (●U_p a ⋅ ◯U_p b) → a ≡ b.
   Proof.
     intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
   Qed.
-  Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a = b.
+  Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U_p a ⋅ ◯U_p b) → a = b.
   Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
 
-  Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U{p} a ⋅ ◯U{q} b) → Some b ≼{n} Some a.
+  Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U_p a ⋅ ◯U_q b) → Some b ≼{n} Some a.
   Proof. by rewrite auth_both_validN=> -[/Some_pair_includedN [_ ?] _]. Qed.
   Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
-    ✓ (●U{p} a ⋅ ◯U{q} b) → Some b ≼ Some a.
+    ✓ (●U_p a ⋅ ◯U_q b) → Some b ≼ Some a.
   Proof. rewrite auth_both_valid_discrete=> -[/Some_pair_included [_ ?] _] //. Qed.
   Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
-    ✓{n} (●U{p} a ⋅ ◯U{q} b) → b ≼{n} a.
+    ✓{n} (●U_p a ⋅ ◯U_q b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
   Lemma ufrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
-    ✓ (●U{p} a ⋅ ◯U{q} b) → b ≼ a.
+    ✓ (●U_p a ⋅ ◯U_q b) → b ≼ a.
   Proof. intros. by eapply Some_included_total, ufrac_auth_included. Qed.
 
-  Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U{q} a) ↔ ✓{n} a.
+  Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U_q a) ↔ ✓{n} a.
   Proof.
     rewrite auth_auth_dfrac_validN Some_validN. split.
     - by intros [?[]].
     - intros. by split.
   Qed.
-  Lemma ufrac_auth_auth_valid q a : ✓ (●U{q} a) ↔ ✓ a.
+  Lemma ufrac_auth_auth_valid q a : ✓ (●U_q a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
 
-  Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U{q} a) ↔ ✓{n} a.
+  Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U_q a) ↔ ✓{n} a.
   Proof.
     rewrite auth_frag_validN. split.
     - by intros [??].
     - by split.
   Qed.
-  Lemma ufrac_auth_frag_valid q a : ✓ (◯U{q} a) ↔ ✓ a.
+  Lemma ufrac_auth_frag_valid q a : ✓ (◯U_q a) ↔ ✓ a.
   Proof.
     rewrite auth_frag_valid. split.
     - by intros [??].
     - by split.
   Qed.
 
-  Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2.
+  Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U_(q1+q2) (a1 ⋅ a2) ≡ ◯U_q1 a1 ⋅ ◯U_q2 a2.
   Proof. done. Qed.
 
   Global Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
-    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U{q} a) (◯U{q1} a1) (◯U{q2} a2).
+    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U_q a) (◯U_q1 a1) (◯U_q2 a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
   Global Instance ufrac_auth_is_op_core_id q q1 q2 a :
-    CoreId a → IsOp q q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a).
+    CoreId a → IsOp q q1 q2 → IsOp' (◯U_q a) (◯U_q1 a) (◯U_q2 a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
     by rewrite -ufrac_auth_frag_op -core_id_dup.
   Qed.
 
   Lemma ufrac_auth_update p q a b a' b' :
-    (a,b) ~l~> (a',b') → ●U{p} a ⋅ ◯U{q} b ~~> ●U{p} a' ⋅ ◯U{q} b'.
+    (a,b) ~l~> (a',b') → ●U_p a ⋅ ◯U_q b ~~> ●U_p a' ⋅ ◯U_q b'.
   Proof.
     intros. apply: auth_update.
     apply: option_local_update. by apply: prod_local_update_2.
   Qed.
 
   Lemma ufrac_auth_update_surplus p q a b :
-   ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b.
+   ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b.
   Proof.
     intros Hconsistent. apply: auth_update_alloc.
     intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.