Bump std++ (Qp changes).

coq-iris.opam

@@ -10,7 +10,7 @@ synopsis: "Iris is a Higher-Order Concurrent Separation Logic Framework with sup
 
 depends: [
   "coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2020-10-15.0.c6e5d0be") | (= "dev") }
+  "coq-stdpp" { (= "dev.2020-10-30.0.402f2d6a") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/algebra/auth.v

@@ -262,10 +262,10 @@ Section auth.
 
   (** Inclusion *)
   Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
-    ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
+    ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2.
   Proof. apply view_auth_frac_includedN. Qed.
   Lemma auth_auth_frac_included p1 p2 a1 a2 b :
-    ●{p1} a1 ≼ ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2.
+    ●{p1} a1 ≼ ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2.
   Proof. apply view_auth_frac_included. Qed.
   Lemma auth_auth_includedN n a1 a2 b :
     ● a1 ≼{n} ● a2 ⋅ ◯ b ↔ a1 ≡{n}≡ a2.
@@ -284,10 +284,10 @@ Section auth.
   (** The weaker [auth_both_included] lemmas below are a consequence of the
   [auth_auth_included] and [auth_frag_included] lemmas above. *)
   Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
-    ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+    ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof. apply view_both_frac_includedN. Qed.
   Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
-    ●{p1} a1 ⋅ ◯ b1 ≼ ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2 ∧ b1 ≼ b2.
+    ●{p1} a1 ⋅ ◯ b1 ≼ ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof. apply view_both_frac_included. Qed.
   Lemma auth_both_includedN n a1 a2 b1 b2 :
     ● a1 ⋅ ◯ b1 ≼{n} ● a2 ⋅ ◯ b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.

theories/algebra/dfrac.v

@@ -18,7 +18,6 @@
     discarded. Conversely, knowing that a fraction has been discarded implies
     that no one can own 1. And, since discarding is an irreversible operation,
     it also implies that no one can own 1 in the future *)
-From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes updates frac.
 From iris Require Import options.
@@ -32,27 +31,24 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
-Global Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
-Proof. by injection 1. Qed.
-
-Global Instance DfracBoth_inj : Inj (=) (=) DfracBoth.
-Proof. by injection 1. Qed.
-
 Section dfrac.
-
   Canonical Structure dfracO := leibnizO dfrac.
 
   Implicit Types p q : Qp.
-
   Implicit Types x y : dfrac.
 
+  Global Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
+  Proof. by injection 1. Qed.
+  Global Instance DfracBoth_inj : Inj (=) (=) DfracBoth.
+  Proof. by injection 1. Qed.
+
   (** An element is valid as long as the sum of its content is less than one. *)
   Instance dfrac_valid : Valid dfrac := λ x,
     match x with
-    | DfracOwn q => q ≤ 1%Qp
+    | DfracOwn q => q ≤ 1
     | DfracDiscarded => True
-    | DfracBoth q => q < 1%Qp
-    end%Qc.
+    | DfracBoth q => q < 1
+    end%Qp.
 
   (** As in the fractional camera the core is undefined for elements denoting
      ownership of a fraction. For elements denoting the knowledge that a fraction has
@@ -86,7 +82,7 @@ Section dfrac.
     DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded.
   Proof. done. Qed.
 
-  Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qc.
+  Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
   Proof.
     rewrite Qp_lt_sum. split.
     - rewrite /included /op /dfrac_op. intros [[o| |?] [= ->]]. by exists o.
@@ -103,20 +99,20 @@ Section dfrac.
     split; try apply _.
     - intros [?| |?] y cx <-; intros [= <-]; eexists _; done.
     - intros [?| |?] [?| |?] [?| |?];
-        rewrite /op /dfrac_op 1?assoc 1?assoc; done.
+        rewrite /op /dfrac_op 1?assoc_L 1?assoc_L; done.
     - intros [?| |?] [?| |?];
-        rewrite /op /dfrac_op 1?(comm Qp_plus); done.
+        rewrite /op /dfrac_op 1?(comm_L Qp_add); done.
     - intros [?| |?] cx; rewrite /pcore /dfrac_pcore; intros [= <-];
         rewrite /op /dfrac_op; done.
     - intros [?| |?] ? [= <-]; done.
     - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
         apply dfrac_discarded_included.
-    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op /valid /dfrac_valid; try done.
-      * apply (Qp_plus_weak_r _ _ 1).
-      * apply Qclt_le_weak.
-      * move=> /Qclt_le_weak. apply Qcle_trans. etrans; last apply Qp_le_plus_l. done.
-      * apply Qclt_trans. apply Qp_lt_sum. eauto.
-      * apply Qclt_trans. apply Qp_lt_sum. eauto.
+    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op /valid /dfrac_valid //.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp_le_add_l.
+      + apply Qp_lt_le_incl.
+      + intros. trans (q + q')%Qp; [|by apply Qp_lt_le_incl]. apply Qp_le_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
   Qed.
   Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
 
@@ -126,41 +122,31 @@ Section dfrac.
   Global Instance dfrac_full_exclusive : Exclusive (DfracOwn 1).
   Proof.
     intros [q| |q];
-      rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
-    - apply (Qp_not_plus_ge 1 q).
-    - intros []%(irreflexivity _).
-    - move=> /Qclt_le_weak. apply (Qp_not_plus_ge 1 q).
+      rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
+    - apply Qp_not_add_le_l.
+    - move=> /Qp_lt_le_incl. apply Qp_not_add_le_l.
   Qed.
 
   Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
   Proof.
     apply: discrete_cancelable.
-    intros [q1| |q1] [q2| |q2] _; rewrite /op /cmra_op; simpl;
-      try by intros [= ->].
-    - by intros ->%(inj _)%(inj _).
-    - done.
-    - intros Hq%(inj _). symmetry in Hq. apply Qp_plus_id_free in Hq. done.
-    - by intros Hq%(inj _)%Qp_plus_id_free.
-    - by intros ->%(inj _)%(inj _).
+    intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
+    - by destruct (Qp_add_id_free q q2).
+    - by destruct (Qp_add_id_free q q1).
   Qed.
-
   Global Instance frac_id_free q : IdFree (DfracOwn q).
-  Proof.
-    intros [q'| |q'] _; rewrite /op /cmra_op; simpl; try by intros [=].
-    by intros [= ?%Qp_plus_id_free].
-  Qed.
-
+  Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
   Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.
 
-  Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1%Qp)%Qc.
+  Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
 
   Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_valid_own_discarded q :
-    ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1%Qp)%Qc.
+    ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1)%Qp.
   Proof. done. Qed.
 
   Global Instance dfrac_is_op q q1 q2 :
@@ -172,16 +158,9 @@ Section dfrac.
   Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded.
   Proof.
     intros n [[q'| |q']|];
-      rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid /=.
-    - intros [Hq|Hq]%Qcle_lt_or_eq.
-      + etrans; last eassumption. change (q' < (q + q')%Qp)%Qc. apply Qp_lt_sum.
-        rewrite {1}comm. eauto.
-      + change (q' < 1%Qp)%Qc. apply Qp_lt_sum. exists q.
-        rewrite (comm Qp_plus). apply Qp_eq. simpl. rewrite Hq. done.
-    - done.
-    - apply Qclt_trans. change (q' < (q + q')%Qp)%Qc. apply Qp_lt_sum.
-      rewrite {1}comm. eauto.
-    - done.
+      rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid //=.
+    - intros. apply Qp_lt_le_trans with (q + q')%Qp; [|done]. apply Qp_lt_add_r.
+    - intros. apply Qp_le_lt_trans with (q + q')%Qp; [|done]. apply Qp_le_add_r.
   Qed.
 
 End dfrac.

theories/algebra/frac.v

@@ -3,7 +3,6 @@ in the internal (0,1] of the rational numbers.
 
 Notice that this camera could in principle be obtained by restricting the
 validity of the unbounded fractional camera [ufrac]. *)
-From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes.
 From iris Require Import options.
@@ -14,51 +13,43 @@ From iris Require Import options.
 Notation frac := Qp (only parsing).
 
 Section frac.
-Canonical Structure fracO := leibnizO frac.
-
-Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
-Instance frac_pcore : PCore frac := λ _, None.
-Instance frac_op : Op frac := λ x y, (x + y)%Qp.
-
-Lemma frac_included (x y : frac) : x ≼ y ↔ (x < y)%Qc.
-Proof. by rewrite Qp_lt_sum. Qed.
-
-Corollary frac_included_weak (x y : frac) : x ≼ y → (x ≤ y)%Qc.
-Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
-
-Definition frac_ra_mixin : RAMixin frac.
-Proof.
-  split; try apply _; try done.
-  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
-  rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
-Qed.
-Canonical Structure fracR := discreteR frac frac_ra_mixin.
-
-Global Instance frac_cmra_discrete : CmraDiscrete fracR.
-Proof. apply discrete_cmra_discrete. Qed.
+  Canonical Structure fracO := leibnizO frac.
+
+  Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qp.
+  Instance frac_pcore : PCore frac := λ _, None.
+  Instance frac_op : Op frac := λ x y, (x + y)%Qp.
+
+  Lemma frac_valid' p : ✓ p ↔ (p ≤ 1)%Qp.
+  Proof. done. Qed.
+  Lemma frac_op' p q : p ⋅ q = (p + q)%Qp.
+  Proof. done. Qed.
+  Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
+  Proof. by rewrite Qp_lt_sum. Qed.
+
+  Corollary frac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
+  Proof. rewrite frac_included. apply Qp_lt_le_incl. Qed.
+
+  Definition frac_ra_mixin : RAMixin frac.
+  Proof.
+    split; try apply _; try done.
+    intros p q. rewrite !frac_valid' frac_op'=> ?.
+    trans (p + q)%Qp; last done. apply Qp_le_add_l.
+  Qed.
+  Canonical Structure fracR := discreteR frac frac_ra_mixin.
+
+  Global Instance frac_cmra_discrete : CmraDiscrete fracR.
+  Proof. apply discrete_cmra_discrete. Qed.
+  Global Instance frac_full_exclusive : Exclusive 1%Qp.
+  Proof. intros p. apply Qp_not_add_le_l. Qed.
+  Global Instance frac_cancelable (q : frac) : Cancelable q.
+  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Global Instance frac_id_free (q : frac) : IdFree q.
+  Proof. intros p _. apply Qp_add_id_free. Qed.
+
+  (* This one has a higher precendence than [is_op_op] so we get a [+] instead
+     of an [⋅]. *)
+  Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
+  Proof. done. Qed.
+  Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
+  Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
 End frac.
-
-Global Instance frac_full_exclusive : Exclusive 1%Qp.
-Proof.
-  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
-Qed.
-
-Global Instance frac_cancelable (q : frac) : Cancelable q.
-Proof. intros n y z ??. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
-
-Global Instance frac_id_free (q : frac) : IdFree q.
-Proof. intros p _. apply Qp_plus_id_free. Qed.
-
-Lemma frac_op' (q p : Qp) : (p ⋅ q) = (p + q)%Qp.
-Proof. done. Qed.
-
-Lemma frac_valid' (p : Qp) : ✓ p ↔ (p ≤ 1%Qp)%Qc.
-Proof. done. Qed.
-
-Global Instance frac_is_op_half q : IsOp' q (q/2)%Qp (q/2)%Qp.
-Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
-
-(* This one has a higher precendence than [is_op_op] so we get a [+] instead
-   of an [⋅]. *)
-Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
-Proof. done. Qed.

theories/algebra/lib/ufrac_auth.v

@@ -16,7 +16,6 @@ difference:
 - We no longer have the [◯U{1} a] is the exclusive fragmental element (cf.
   [frac_auth_frag_validN_op_1_l]).
 *)
-From Coq Require Import QArith Qcanon.
 From iris.algebra Require Export auth frac updates local_updates.
 From iris.algebra Require Import ufrac proofmode_classes.
 From iris Require Import options.
@@ -71,10 +70,9 @@ Section ufrac_auth.
 
   Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U{p} a ⋅ ◯U{p} b) → a ≡{n}≡ b.
   Proof.
-    rewrite auth_both_validN=> -[Hincl Hvalid].
-    move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
-    rewrite -discrete_iff leibniz_equiv_iff. rewrite ufrac_op'=> [/Qp_eq/=].
-    rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
+    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.
   Proof.

theories/algebra/ufrac.v

 (** This file provides an "unbounded" version of the fractional camera whose
 elements are in the interval (0,..) instead of (0,1]. *)
-From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes.
 From iris Require Import options.
@@ -11,37 +10,34 @@ infers the [frac] camera by default when using the [Qp] type. *)
 Definition ufrac := Qp.
 
 Section ufrac.
-Canonical Structure ufracO := leibnizO ufrac.
+  Implicit Types p q : ufrac.
 
-Instance ufrac_valid : Valid ufrac := λ x, True.
-Instance ufrac_pcore : PCore ufrac := λ _, None.
-Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
+  Canonical Structure ufracO := leibnizO ufrac.
 
-Lemma ufrac_included (x y : ufrac) : x ≼ y ↔ (x < y)%Qc.
-Proof. by rewrite Qp_lt_sum. Qed.
+  Instance ufrac_valid : Valid ufrac := λ x, True.
+  Instance ufrac_pcore : PCore ufrac := λ _, None.
+  Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
 
-Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc.
-Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
+  Lemma ufrac_op' p q : p ⋅ q = (p + q)%Qp.
+  Proof. done. Qed.
+  Lemma ufrac_included p q : p ≼ q ↔ (p < q)%Qp.
+  Proof. by rewrite Qp_lt_sum. Qed.
 
-Definition ufrac_ra_mixin : RAMixin ufrac.
-Proof. split; try apply _; try done. Qed.
-Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
+  Corollary ufrac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
+  Proof. rewrite ufrac_included. apply Qp_lt_le_incl. Qed.
 
-Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
-Proof. apply discrete_cmra_discrete. Qed.
-End ufrac.
-
-Global Instance ufrac_cancelable (q : ufrac) : Cancelable q.
-Proof. intros n y z ??. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+  Definition ufrac_ra_mixin : RAMixin ufrac.
+  Proof. split; try apply _; try done. Qed.
+  Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
 
-Global Instance ufrac_id_free (q : ufrac) : IdFree q.
-Proof.
-  intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
-  eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
-Qed.
+  Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
+  Proof. apply discrete_cmra_discrete. Qed.
 
-Lemma ufrac_op' (q p : ufrac) : (p ⋅ q) = (p + q)%Qp.
-Proof. done. Qed.
+  Global Instance ufrac_cancelable q : Cancelable q.
+  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Global Instance ufrac_id_free q : IdFree q.
+  Proof. intros p _. apply Qp_add_id_free. Qed.
 
-Global Instance ufrac_is_op (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
-Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
+  Global Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
+  Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
+End ufrac.

theories/algebra/view.v

@@ -384,26 +384,26 @@ Section cmra.
 
   (** Inclusion *)
   Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :
-    ●V{p1} a1 ≼{n} ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
+    ●V{p1} a1 ≼{n} ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2.
   Proof.
     split.
     - intros [[[[qf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [apply Qp_le_plus_l|]. apply to_agree_includedN. by exists agf.
+      + split; [apply Qp_le_add_l|]. apply to_agree_includedN. by exists agf.
       + split; [done|]. by apply (inj to_agree).
-    - intros [[[q ->]%frac_included| ->%Qp_eq]%Qcanon.Qcle_lt_or_eq ->].
+    - intros [[[q ->]%frac_included| ->]%Qp_le_lteq ->].
       + rewrite view_auth_frac_op -assoc. apply cmra_includedN_l.
       + apply cmra_includedN_l.
   Qed.
   Lemma view_auth_frac_included p1 p2 a1 a2 b :
-    ●V{p1} a1 ≼ ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2.
+    ●V{p1} a1 ≼ ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2.
   Proof.
     intros. split.
     - split.
       + by eapply (view_auth_frac_includedN 0), cmra_included_includedN.
       + apply equiv_dist=> n.
         by eapply view_auth_frac_includedN, cmra_included_includedN.
-    - intros [[[q ->]%frac_included| ->%Qp_eq]%Qcanon.Qcle_lt_or_eq ->].
+    - intros [[[q ->]%frac_included| ->]%Qp_le_lteq ->].
       + rewrite view_auth_frac_op -assoc. apply cmra_included_l.
       + apply cmra_included_l.
   Qed.
@@ -434,7 +434,7 @@ Section cmra.
   (** The weaker [view_both_included] lemmas below are a consequence of the
   [view_auth_included] and [view_frag_included] lemmas above. *)
   Lemma view_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
-    ●V{p1} a1 ⋅ ◯V b1 ≼{n} ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+    ●V{p1} a1 ⋅ ◯V b1 ≼{n} ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof.
     split.
     - intros. rewrite assoc. split.
@@ -444,7 +444,7 @@ Section cmra.
       by apply cmra_monoN_r, view_auth_frac_includedN.
   Qed.
   Lemma view_both_frac_included p1 p2 a1 a2 b1 b2 :
-    ●V{p1} a1 ⋅ ◯V b1 ≼ ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2 ∧ b1 ≼ b2.
+    ●V{p1} a1 ⋅ ◯V b1 ≼ ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof.
     split.
     - intros. rewrite assoc. split.
@@ -522,7 +522,7 @@ Section cmra.
     rewrite !local_update_unital.
     move=> Hup Hrel n [[[q ag]|] bf] /view_both_validN Hrel' [/=].
     - rewrite right_id -Some_op -pair_op frac_op'=> /Some_dist_inj [/= H1q _].
-      exfalso. apply (Qp_not_plus_ge 1 q). by rewrite -H1q.
+      by destruct (Qp_add_id_free 1 q).
     - rewrite !left_id=> _ Hb0.
       destruct (Hup n bf) as [? Hb0']; [by eauto using view_rel_validN..|].
       split; [apply view_both_validN; by auto|]. by rewrite -assoc Hb0'.

theories/bi/lib/fractional.v

@@ -98,15 +98,15 @@ Section fractional.
 
   (** Mult instances *)
 
-  Global Instance mult_fractional_l Φ Ψ p :
+  Global Instance mul_fractional_l Φ Ψ p :
     (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ.
   Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_l. by apply H.
+    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_r. by apply H.
   Qed.
-  Global Instance mult_fractional_r Φ Ψ p :
+  Global Instance mul_fractional_r Φ Ψ p :
     (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ.
   Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_r. by apply H.
+    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_l. by apply H.
   Qed.
 
   (* REMARK: These two instances do not work in either direction of the
@@ -114,16 +114,16 @@ Section fractional.
        - In the forward direction, they make the search not terminate
        - In the backward direction, the higher order unification of Φ
          with the goal does not work. *)
-  Instance mult_as_fractional_l P Φ p q :
+  Instance mul_as_fractional_l P Φ p q :
     AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q.
   Proof.
-    intros H. split. apply H. eapply (mult_fractional_l _ Φ p).
+    intros H. split. apply H. eapply (mul_fractional_l _ Φ p).
     split. done. apply H.
   Qed.
-  Instance mult_as_fractional_r P Φ p q :
+  Instance mul_as_fractional_r P Φ p q :
     AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q.
   Proof.
-    intros H. split. apply H. eapply (mult_fractional_r _ Φ p).
+    intros H. split. apply H. eapply (mul_fractional_r _ Φ p).
     split. done. apply H.
   Qed.