Merge branch 'robbert/laterN_add' into 'master'

Rename `_plus` into `_add`.

Closes #472

See merge request !821

CHANGELOG.md

@@ -33,6 +33,7 @@ lemma.
 * Remove `mono_list_lb_is_op` instance for `IsOp' (◯ML l) (◯ML l) (◯ML l)`; we
   don't usually have such instances for duplicable resources and it was added by
   accident.
+* Rename `pos_op_plus` into `pos_op_add`.
 
 **Changes in `bi`:**
 
@@ -53,6 +54,7 @@ lemma.
   `least_fixpoint_affine`, `least_fixpoint_absorbing`,
   `least_fixpoint_persistent_affine`, `least_fixpoint_persistent_absorbing`,
   `greatest_fixpoint_absorbing`.
+* Rename `laterN_plus` into `laterN_add`.
 
 **Changes in `proofmode`:**
 
@@ -151,6 +153,9 @@ s/\bexcl_auth_frag_validN_op_1_l\b/excl_auth_frag_op_validN/g
 s/\bexcl_auth_frag_valid_op_1_l\b/excl_auth_frag_op_valid/g
 # staging → unstable
 s/\biris\.staging\b/iris.unstable/g
+# plus → add
+s/\blaterN_plus\b/laterN_add/g
+s/\bpos_op_plus\b/pos_op_add/g
 EOF
 ```
 

iris/algebra/numbers.v

@@ -163,7 +163,7 @@ Section positive.
   Local Instance pos_validN_instance : ValidN positive := λ n x, True.
   Local Instance pos_pcore_instance : PCore positive := λ x, None.
   Local Instance pos_op_instance : Op positive := Pos.add.
-  Definition pos_op_plus x y : x ⋅ y = (x + y)%positive := eq_refl.
+  Definition pos_op_add x y : x ⋅ y = (x + y)%positive := eq_refl.
   Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
   Proof. by rewrite Plt_sum. Qed.
   Lemma pos_ra_mixin : RAMixin positive.

iris/bi/derived_laws_later.v

@@ -183,7 +183,7 @@ Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
 Proof. done. Qed.
 Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
 Proof. induction n; f_equiv/=; auto. Qed.
-Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
+Lemma laterN_add n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
 Proof. induction n1; f_equiv/=; auto. Qed.
 Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
 Proof. induction 1; simpl; by rewrite -?later_intro. Qed.

iris/proofmode/class_instances_later.v

@@ -288,7 +288,7 @@ Global Instance into_laterN_later only_head n n' m' P Q lQ :
 Proof.
   rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
   move=> Hn [_ ->|->] <-;
-    by rewrite -later_laterN -laterN_plus -Hn Nat.add_comm.
+    by rewrite -later_laterN -laterN_add -Hn Nat.add_comm.
 Qed.
 Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
   NatCancel n m n' m' →
@@ -297,7 +297,7 @@ Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
   IntoLaterN only_head n (▷^m P) lQ | 1.
 Proof.
   rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
-  move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
+  move=> Hn [_ ->|->] <-; by rewrite -!laterN_add -Hn Nat.add_comm.
 Qed.
 
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :