fixes #1051 (rename lim_sup -> limn_sup) (#1068)

* fixes #1051

* add only parsing

CHANGELOG_UNRELEASED.md

@@ -69,6 +69,35 @@
 - in `ereal.v`:
   + `le_er_map` -> `le_er_map_in`
 
+- in `sequences.v`:
+  + `lim_sup` -> `limn_sup`
+  + `lim_inf` -> `limn_inf`
+  + `lim_infN` -> `limn_infN`
+  + `lim_supE` -> `limn_supE`
+  + `lim_infE` -> `limn_infE`
+  + `lim_inf_le_lim_sup` -> `limn_inf_sup`
+  + `cvg_lim_inf_sup` -> `cvg_limn_inf_sup`
+  + `cvg_lim_supE` -> `cvg_limn_supE`
+  + `le_lim_supD` -> `le_limn_supD`
+  + `le_lim_infD` -> `le_limn_infD`
+  + `lim_supD` -> `limn_supD`
+  + `lim_infD` -> `limn_infD`
+  + `LimSup.lim_esup` -> `limn_esup`
+  + `LimSup.lim_einf` -> `limn_einf`
+  + `lim_einf_shift` -> `limn_einf_shift`
+  + `lim_esup_le_cvg` -> `limn_esup_le_cvg`
+  + `lim_einfN` -> `limn_einfN`
+  + `lim_esupN` -> `limn_esupN`
+  + `lim_einf_sup` -> `limn_einf_sup`
+  + `cvgNy_lim_einf_sup` -> `cvgNy_limn_einf_sup`
+  + `cvg_lim_einf_sup` -> `cvg_limn_einf_sup`
+  + `is_cvg_lim_einfE` -> `is_cvg_limn_einfE`
+  + `is_cvg_lim_esupE` -> `is_cvg_limn_esupE`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_lim_sup` -> `measurable_fun_limn_sup`
+  + `measurable_fun_lim_esup` -> `measurable_fun_limn_esup`
+
 ### Generalized
 
 - in `topology.v`:
@@ -80,6 +109,26 @@
 
 - `lebesgue_measure_unique` (generalized to `lebesgue_stieltjes_measure_unique`)
 
+- in `sequences.v`:
+  + notations `elim_sup`, `elim_inf`
+  + `LimSup.lim_esup`, `LimSup.lim_einf`
+  + `elim_inf_shift`
+  + `elim_sup_le_cvg`
+  + `elim_infN`
+  + `elim_supN`
+  + `elim_inf_sup`
+  + `cvg_ninfty_elim_inf_sup`
+  + `cvg_ninfty_einfs`
+  + `cvg_ninfty_esups`
+  + `cvg_pinfty_einfs`
+  + `cvg_pinfty_esups`
+  + `cvg_elim_inf_sup`
+  + `is_cvg_elim_infE`
+  + `is_cvg_elim_supE`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_elim_sup`
+
 ### Infrastructure
 
 ### Misc

CONTRIBUTING.md

@@ -44,6 +44,24 @@ Landau notations can be written in four shapes:
 
 The outcome is an expression with the normal Leibniz equality `=` and term `'o_F` which is not parsable. See [this paper](https://doi.org/10.6092/issn.1972-5787/8124) for more explanation and the header of the file [landau.v](https://github.com/math-comp/analysis/blob/master/theories/landau.v).
 
+## Deprecation
+
+Deprecations are introduced for breaking changes. For a simple renaming, the pattern is:
+```
+#[deprecated(since="analysis X.Y.Z", note="Use new_definition instead.")]
+Notation old_definition := new_definition (only parsing).
+```
+Note that this needs to be at the top-level (i.e., not inside a section).
+
+When a lemma `lem` is scheduled for deletion, it ought better be renamed `__deprecated__lem`
+(so that it can be blacklisted). The deprecation command then becomes:
+```
+#[deprecated(since="analysis X.Y.Z", note="Use another_lemma instead.")]
+Notation lem := __deprecated__lem (only parsing).
+```
+The `(only parsing)` format is needed so that Coq does not print back the deprecated name
+(for example when displaying error messages, that would be confusing).
+
 ## Naming convention
 
 ### homo and mono notations

classical/cardinality.v

@@ -909,7 +909,7 @@ Lemma __deprecated__bigcup_fset_set T (I : choiceType) (A : set I) (F : I -> set
   finite_set A -> \bigcup_(i in A) F i = \big[setU/set0]_(i <- fset_set A) F i.
 Proof. by move=> /bigsetU_fset_set->. Qed.
 #[deprecated(note="Use -bigsetU_fset_set instead")]
-Notation bigcup_fset_set := __deprecated__bigcup_fset_set.
+Notation bigcup_fset_set := __deprecated__bigcup_fset_set (only parsing).
 
 Lemma bigsetU_fset_set_cond T (I : choiceType) (A : set I) (F : I -> set T)
     (P : pred I) : finite_set A ->
@@ -923,7 +923,7 @@ Lemma __deprecated__bigcup_fset_set_cond T (I : choiceType) (A : set I) (F : I -
   \bigcup_(i in A `&` P) F i = \big[setU/set0]_(i <- fset_set A | P i) F i.
 Proof. by move=> /bigsetU_fset_set_cond->. Qed.
 #[deprecated(note="Use -bigsetU_fset_set_cond instead")]
-Notation bigcup_fset_set_cond := __deprecated__bigcup_fset_set_cond.
+Notation bigcup_fset_set_cond := __deprecated__bigcup_fset_set_cond (only parsing).
 
 Lemma bigsetI_fset_set T (I : choiceType) (A : set I) (F : I -> set T) :
   finite_set A -> \big[setI/setT]_(i <- fset_set A) F i =\bigcap_(i in A) F i.
@@ -935,7 +935,7 @@ Lemma __deprecated__bigcap_fset_set T (I : choiceType) (A : set I) (F : I -> set
   finite_set A -> \bigcap_(i in A) F i = \big[setI/setT]_(i <- fset_set A) F i.
 Proof. by move=> /bigsetI_fset_set->. Qed.
 #[deprecated(note="Use -bigsetI_fset_set instead")]
-Notation bigcap_fset_set := __deprecated__bigcap_fset_set.
+Notation bigcap_fset_set := __deprecated__bigcap_fset_set (only parsing).
 
 Lemma bigsetI_fset_set_cond T (I : choiceType) (A : set I) (F : I -> set T)
     (P : pred I) : finite_set A ->
@@ -1064,7 +1064,7 @@ by under eq_imagel do rewrite /= gE ?inE//; rewrite image_eq.
 Qed.
 
 #[deprecated(note="use countable0 instead")]
-Notation countable_set0 := countable0.
+Notation countable_set0 := countable0 (only parsing).
 
 Lemma countable1 T (x : T) : countable [set x].
 Proof. exact: finite_set_countable. Qed.

classical/classical_sets.v

@@ -466,7 +466,7 @@ apply: contra_notP => /forallNP h.
 by apply/eqP; rewrite predeqE => t; split => // _; apply: contrapT.
 Qed.
 #[deprecated(note="Use setTPn instead")]
-Notation setTP := setTPn.
+Notation setTP := setTPn (only parsing).
 
 Lemma in_set0 (x : T) : (x \in set0) = false. Proof. by rewrite memNset. Qed.
 Lemma in_setT (x : T) : x \in setT. Proof. by rewrite mem_set. Qed.
@@ -1033,9 +1033,9 @@ End basic_lemmas.
 #[global]
 Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.
 #[deprecated(since="mathcomp-analysis 0.6", note="Use setICl instead.")]
-Notation setvI := setICl.
+Notation setvI := setICl (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6", note="Use setICr instead.")]
-Notation setIv := setICr.
+Notation setIv := setICr (only parsing).
 Arguments setU_id2r {T} C {A B}.
 
 Section set_order.
@@ -1981,13 +1981,13 @@ Proof. by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed.
 
 End bigcup_seq.
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcup_seq instead")]
-Notation bigcup_set := bigcup_seq.
+Notation bigcup_set := bigcup_seq (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcup_seq_cond instead")]
-Notation bigcup_set_cond := bigcup_seq_cond.
+Notation bigcup_set_cond := bigcup_seq_cond (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcap_seq instead")]
-Notation bigcap_set := bigcap_seq.
+Notation bigcap_set := bigcap_seq (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcap_seq_cond instead")]
-Notation bigcap_set_cond := bigcap_seq_cond.
+Notation bigcap_set_cond := bigcap_seq_cond (only parsing).
 
 Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) :
   \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t.
@@ -2628,7 +2628,7 @@ Qed.
 End partitions.
 
 #[deprecated(note="Use trivIset_setIl instead")]
-Notation trivIset_setI := trivIset_setIl.
+Notation trivIset_setI := trivIset_setIl (only parsing).
 
 Definition total_on T (A : set T) (R : T -> T -> Prop) :=
   forall s t, A s -> A t -> R s t \/ R t s.

classical/fsbigop.v

@@ -276,7 +276,7 @@ Proof. by move=> Afin; apply: __deprecated__full_fsbigID; apply: finite_setIl. Q
 Arguments fsbigID {R idx op I} B.
 
 #[deprecated(note="Use fsbigID instead")]
-Notation full_fsbigID := __deprecated__full_fsbigID.
+Notation full_fsbigID := __deprecated__full_fsbigID (only parsing).
 
 Lemma fsbigU (R : Type) (idx : R) (op : Monoid.com_law idx)
     (I : choiceType) (A B : set I) (F : I -> R) :
@@ -422,9 +422,9 @@ Arguments fsbig_image {R idx op I J} _ _.
 Arguments __deprecated__reindex_inside {R idx op I J} _ _.
 Arguments reindex_fsbigT {R idx op I J} _ _.
 #[deprecated(note="use reindex_fsbig, fsbig_image or reindex_fsbigT instead")]
-Notation reindex_inside := __deprecated__reindex_inside.
+Notation reindex_inside := __deprecated__reindex_inside (only parsing).
 #[deprecated(note="use reindex_fsbigT instead")]
-Notation reindex_inside_setT := reindex_fsbigT.
+Notation reindex_inside_setT := reindex_fsbigT (only parsing).
 
 Lemma fsbigN1 (R : eqType) (idx : R) (op : Monoid.com_law idx)
     (T1 T2 : choiceType) (Q : set T2) (f : T1 -> T2 -> R) (x : T1) :

theories/charge.v

@@ -1078,9 +1078,11 @@ Definition fRN := fun x => lim (F ^~ x).
 
 Lemma measurable_fun_fRN : measurable_fun [set: T] fRN.
 Proof.
-rewrite (_ : fRN = fun x => lim_esup (F ^~ x)).
-  by apply: measurable_fun_lim_esup => // n; exact: measurable_max_approxRN_seq.
-by apply/funext=> n; rewrite is_cvg_lim_esupE//; exact: is_cvg_max_approxRN_seq.
+rewrite (_ : fRN = fun x => limn_esup (F ^~ x)).
+  apply: measurable_fun_limn_esup => // n.
+  exact: measurable_max_approxRN_seq.
+apply/funext=> n; rewrite is_cvg_limn_esupE//.
+exact: is_cvg_max_approxRN_seq.
 Qed.
 
 Lemma fRN_ge0 x : 0 <= fRN x.

theories/constructive_ereal.v

@@ -1020,13 +1020,13 @@ by apply/eqP/esum_eqyP => //; exists i.
 Qed.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNyP`")]
-Notation esum_ninftyP := esum_eqNyP.
+Notation esum_ninftyP := esum_eqNyP (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNy`")]
-Notation esum_ninfty := esum_eqNy.
+Notation esum_ninfty := esum_eqNy (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqyP`")]
-Notation esum_pinftyP := esum_eqyP.
+Notation esum_pinftyP := esum_eqyP (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqy`")]
-Notation esum_pinfty := esum_eqy.
+Notation esum_pinfty := esum_eqy (only parsing).
 
 Lemma adde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
 Proof. by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed.
@@ -1398,13 +1398,13 @@ by under eq_existsb => i do rewrite eqe_oppLR.
 Qed.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNyP`")]
-Notation desum_ninftyP := desum_eqNyP.
+Notation desum_ninftyP := desum_eqNyP (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNy`")]
-Notation desum_ninfty := desum_eqNy.
+Notation desum_ninfty := desum_eqNy (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqyP`")]
-Notation desum_pinftyP := desum_eqyP.
+Notation desum_pinftyP := desum_eqyP (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqy`")]
-Notation desum_pinfty := desum_eqy.
+Notation desum_pinfty := desum_eqy (only parsing).
 
 Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
 Proof. rewrite dual_addeE oppe_ge0 -!oppe_le0; exact: adde_le0. Qed.
@@ -1498,7 +1498,7 @@ by apply/negP; rewrite -leNgt; apply/Ax/ltr_spaddr; rewrite // le_maxr lexx.
 Qed.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `eqyP`")]
-Notation eq_pinftyP := eqyP.
+Notation eq_pinftyP := eqyP (only parsing).
 
 Lemma seq_psume_eq0 (I : choiceType) (r : seq I)
     (P : pred I) (F : I -> \bar R) : (forall i, P i -> 0 <= F i)%E ->
@@ -2597,11 +2597,11 @@ Arguments lee_sum_npos_natl {R}.
 #[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core.
 
 #[deprecated(since="mathcomp-analysis 0.6", note="Use lte_spaddre instead.")]
-Notation lte_spaddr := lte_spaddre.
+Notation lte_spaddr := lte_spaddre (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.5", note="Use leeN2 instead.")]
-Notation lee_opp := leeN2.
+Notation lee_opp := leeN2 (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.5", note="Use lteN2 instead.")]
-Notation lte_opp := lteN2.
+Notation lte_opp := lteN2 (only parsing).
 
 Module DualAddTheoryRealDomain.
 

theories/derive.v

@@ -1376,15 +1376,15 @@ Lemma __deprecated__le0r_cvg_map (R : realFieldType) (T : topologicalType) (F :
 Proof. by move=> ? ?; rewrite limr_ge. Qed.
 #[deprecated(since="mathcomp-analysis 0.6.0",
   note="generalized by `limr_ge`")]
-Notation le0r_cvg_map := __deprecated__le0r_cvg_map.
+Notation le0r_cvg_map := __deprecated__le0r_cvg_map (only parsing).
 
 Lemma __deprecated__ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
   (FF : ProperFilter F) (f : T -> R) :
   (\forall x \near F, f x <= 0) -> cvg (f @ F) -> lim (f @ F) <= 0.
 Proof. by move=> ? ?; rewrite limr_le. Qed.
 #[deprecated(since="mathcomp-analysis 0.6.0",
   note="generalized by `limr_le`")]
-Notation ler0_cvg_map := __deprecated__ler0_cvg_map.
+Notation ler0_cvg_map := __deprecated__ler0_cvg_map (only parsing).
 
 Lemma __deprecated__ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
     (FF : ProperFilter F) (f g : T -> R) :
@@ -1393,7 +1393,7 @@ Lemma __deprecated__ler_cvg_map (R : realFieldType) (T : topologicalType) (F : s
 Proof. by move=> ? ? ?; rewrite ler_lim. Qed.
 #[deprecated(since="mathcomp-analysis 0.6.0",
   note="subsumed by `ler_lim`")]
-Notation ler_cvg_map := __deprecated__ler_cvg_map.
+Notation ler_cvg_map := __deprecated__ler_cvg_map (only parsing).
 
 Lemma derive1_at_max (R : realFieldType) (f : R -> R) (a b c : R) :
   a <= b -> (forall t, t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R ->

theories/kernel.v

@@ -516,10 +516,10 @@ Lemma measurable_fun_xsection_integral
 Proof.
 move=> h.
 rewrite (_ : (fun x => _) =
-    (fun x => lim_esup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first.
+    (fun x => limn_esup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first.
   apply/funext => x.
   transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first.
-    rewrite is_cvg_lim_esupE//.
+    rewrite is_cvg_limn_esupE//.
     apply: ereal_nondecreasing_is_cvg => m n mn.
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
@@ -532,7 +532,7 @@ rewrite (_ : (fun x => _) =
   - by move=> n; exact/EFin_measurable_fun/measurableT_comp.
   - by move=> n y _; rewrite lee_fin.
   - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_.
-apply: measurable_fun_lim_esup => n.
+apply: measurable_fun_limn_esup => n.
 rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y
     (\sum_(r \in range (k_ n))
       r * \1_(k_ n @^-1` [set r]) (x, y))%:E)); last first.