iris/algebra/cmra_big_op.v

@@ -3,34 +3,36 @@ From iris.algebra Require Export big_op cmra.
 From iris.prelude Require Import options.
 
 (** Option *)
-Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
+Lemma big_opL_None {M : cmra} {A} (f : nat → A → option M) l :
   ([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
 Proof.
   revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
   - intros [??] [|k] y ?; naive_solver.
   - intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
 Qed.
-Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K → A → option M) m :
+Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
 Proof.
-  induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
-  rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
+  induction m as [|i x m ? IH] using map_ind=> /=.
+  { by rewrite big_opM_empty. }
+  rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
   { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
   intros Hm; split.
   - apply (Hm i). by simplify_map_eq.
   - intros k y ?. apply (Hm k). by simplify_map_eq.
 Qed.
-Lemma big_opS_None {M : cmraT} `{Countable A} (f : A → option M) X :
+Lemma big_opS_None {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
-  induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
-  rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
+  induction X as [|x X ? IH] using set_ind_L.
+  { by rewrite big_opS_empty. }
+  rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
 Qed.
-Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A → option M) X :
+Lemma big_opMS_None {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X IH] using gmultiset_ind.
-  { rewrite big_opMS_empty. set_solver. }
-  rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
-  set_solver.
+  { rewrite big_opMS_empty. multiset_solver. }
+  rewrite -None_equiv_eq big_opMS_disj_union big_opMS_singleton None_equiv_eq op_None IH.
+  multiset_solver.
 Qed.

iris/algebra/frac.v

@@ -15,41 +15,43 @@ Notation frac := Qp (only parsing).
 Section frac.
   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.
+  Local Instance frac_valid_instance : Valid frac := λ x, (x ≤ 1)%Qp.
+  Local Instance frac_pcore_instance : PCore frac := λ _, None.
+  Local Instance frac_op_instance : Op frac := λ x y, (x + y)%Qp.
 
-  Lemma frac_valid' p : ✓ p ↔ (p ≤ 1)%Qp.
+  Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
-  Lemma frac_op' p q : p ⋅ q = (p + q)%Qp.
+  Lemma frac_valid_1 : ✓ 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.
+  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.
+  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.
+    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.
+  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.
+  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.
+  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.
+  Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
 End frac.