rm warnings mathcomp-2.1.0 (#1223)

CHANGELOG_UNRELEASED.md

@@ -73,6 +73,26 @@
 - in `classical_sets.v`:
   + `notin_set` -> `notin_setE`
 
+- in `signed.v`:
+  + `num_le_maxr` -> `num_le_max`
+  + `num_le_maxl` -> `num_ge_max`
+  + `num_le_minr` -> `num_le_min`
+  + `num_le_minl` -> `num_ge_min`
+  + `num_lt_maxr` -> `num_lt_max`
+  + `num_lt_maxl` -> `num_gt_max`
+  + `num_lt_minr` -> `num_lt_min`
+  + `num_lt_minl` -> `num_gt_min`
+
+- in `constructive_ereal.v`:
+  + `num_lee_maxr` -> `num_lee_max`
+  + `num_lee_maxl` -> `num_gee_max`
+  + `num_lee_minr` -> `num_lee_min`
+  + `num_lee_minl` -> `num_gee_min`
+  + `num_lte_maxr` -> `num_lte_max`
+  + `num_lte_maxl` -> `num_gte_max`
+  + `num_lte_minr` -> `num_lte_min`
+  + `num_lte_minl` -> `num_gte_min`
+
 ### Generalized
 
 - in `constructive_ereal.v`:

classical/mathcomp_extra.v

@@ -155,8 +155,8 @@ Lemma le_bigmax_seq F :
   i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O.
 Proof.
 move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons.
-move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_maxr// lexx.
-by case: ifPn => Ph; [rewrite le_maxr ih// orbT|rewrite ih].
+move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_max// lexx.
+by case: ifPn => Ph; [rewrite le_max ih// orbT|rewrite ih].
 Qed.
 
 (* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat *)

classical/set_interval.v

@@ -341,8 +341,8 @@ move: a => [b r|[|]] _ //.
   suff: ~ has_lbound `]-oo, r[%classic.
     by case: b => //; apply/contra_not/subset_has_lbound => x /ltW.
   apply/has_lbPn => x; exists (minr (r - 1) (x - 1)).
-    by rewrite !set_itvE/= lt_minl ltrBlDr ltrDl ltr01.
-  by rewrite lt_minl orbC ltrBlDr ltrDl ltr01.
+    by rewrite !set_itvE/= gt_min ltrBlDr ltrDl ltr01.
+  by rewrite gt_min orbC ltrBlDr ltrDl ltr01.
 case=> r /(_ (r - 1)) /=; rewrite in_itv /= => /(_ erefl).
 by apply/negP; rewrite -ltNge ltrBlDr ltrDl.
 Qed.
@@ -355,7 +355,7 @@ move: a => [b r|[|]] _ //.
     case: b => //; apply/contra_not/subset_has_ubound => x.
     by rewrite !set_itvE => /ltW.
   apply/has_ubPn => x; rewrite !set_itvE; exists (maxr (r + 1) (x + 1));
-  by rewrite ?in_itv /= ?andbT lt_maxr ltrDl ltr01 // orbT.
+  by rewrite ?in_itv /= ?andbT lt_max ltrDl ltr01 // orbT.
 case=> r /(_ (r + 1)) /=; rewrite in_itv /= => /(_ erefl).
 by apply/negP; rewrite -ltNge ltrDl.
 Qed.

theories/Rstruct.v

@@ -532,9 +532,9 @@ Lemma bigmaxr_ler (x0 : R) s i :
   (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
 Proof.
 rewrite /bigmaxr; elim: s i => // h t IH [_|i] /=.
-  by rewrite big_cons /= le_maxr lexx.
+  by rewrite big_cons /= le_max lexx.
 rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
-by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
+by rewrite big_cons bigrmax_dflt le_max orbC IH.
 Qed.
 
 (* Compatibilité avec l'addition *)
@@ -553,8 +553,8 @@ Proof.
 rewrite /bigmaxr; case: lr => // h t _.
 elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE maxxx.
 rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
-- by rewrite le_maxr lexx.
-- by rewrite lt_maxr ltxx => ?; rewrite max_r ?IH // ltW.
+- by rewrite le_max lexx.
+- by rewrite lt_max ltxx => ?; rewrite max_r ?IH // ltW.
 Qed.
 
 (* TODO: bigmaxr_morph? *)

theories/altreals/distr.v

@@ -81,10 +81,10 @@ Definition clamp (x : R) :=
   Num.max (Num.min x 1) 0.
 
 Lemma ge0_clamp x : 0 <= clamp x.
-Proof. by rewrite le_maxr lexx orbT. Qed.
+Proof. by rewrite le_max lexx orbT. Qed.
 
 Lemma le1_clamp x : clamp x <= 1.
-Proof. by rewrite le_maxl le_minl lexx ler01 orbT. Qed.
+Proof. by rewrite ge_max ge_min lexx ler01 orbT. Qed.
 
 Definition cp01_clamp := (ge0_clamp, le1_clamp).
 
@@ -1171,7 +1171,7 @@ Lemma has_esp_bounded f mu :
   (exists M, forall x, `|f x| < M) -> \E?_[mu] f.
 Proof.                          (* TO BE REMOVED *)
 case=> M ltM; rewrite /has_esp; apply/summable_seqP.
-exists (Num.max M 0); first by rewrite le_maxr lexx orbT.
+exists (Num.max M 0); first by rewrite le_max lexx orbT.
 move=> J uqJ; apply/(@le_trans _ _ (\sum_(j <- J) M * mu j)).
   apply/ler_sum=> j _; rewrite normrM [X in _*X]ger0_norm //.
   by apply/ler_wpM2r=> //; apply/ltW.

theories/altreals/realseq.v

@@ -209,20 +209,20 @@ Lemma ncvg_nbounded u x : ncvg u x%:E -> nbounded u.
 Proof.                   (* FIXME: factor out `sup` of a finite set *)
 case/(_ (B x 1)) => K cu; pose S := [seq `|u n| | n <- iota 0 K].
 pose M : R := sup [set x : R | x \in S]; pose e := Num.max (`|x| + 1) (M + 1).
-apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_maxr ltr_wpDl.
+apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_max ltr_wpDl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
-  rewrite lt_maxr; apply/orP; left; rewrite -[u n](addrK x) addrAC.
+  rewrite lt_max; apply/orP; left; rewrite -[u n](addrK x) addrAC.
   by apply/(le_lt_trans (ler_normD _ _)); rewrite addrC ltrD2l.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
-move=> un_S; rewrite lt_maxr; apply/orP; right.
+move=> un_S; rewrite lt_max; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_pwDr; first apply/ltr01.
 suff : has_sup (fun x : R => x \in S) by move/sup_upper_bound/ubP => ->.
 split; first by exists `|u 0%N|; rewrite /S E inE eqxx.
 elim: {+}S => [|v s [ux /ubP hux]]; first by exists 0; apply/ubP.
 exists (Num.max v ux); apply/ubP=> y; rewrite inE => /orP[/eqP->|].
-  by rewrite le_maxr lexx.
-by move/hux=> le_yux; rewrite le_maxr le_yux orbT.
+  by rewrite le_max lexx.
+by move/hux=> le_yux; rewrite le_max le_yux orbT.
 Qed.
 
 Lemma nboundedC c : nbounded c%:S.

theories/altreals/realsum.v

@@ -107,14 +107,14 @@ Proof. by apply/normr_ge0. Qed.
 
 Lemma le_fpos_norm f x : fpos f x <= `|f x|.
 Proof.
-rewrite /fpos ger0_norm ?(le_maxr, lexx) //.
-by rewrite le_maxl normr_ge0 ler_norm.
+rewrite /fpos ger0_norm ?(le_max, lexx) //.
+by rewrite ge_max normr_ge0 ler_norm.
 Qed.
 
 Lemma le_fpos f1 f2 : f1 <=1 f2 -> fpos f1 <=1 fpos f2.
 Proof.
-move=> le_f x; rewrite /fpos !ger0_norm ?le_maxr ?lexx //.
-by rewrite le_maxl lexx /=; case: ltP => //=; rewrite le_f.
+move=> le_f x; rewrite /fpos !ger0_norm ?le_max ?lexx //.
+by rewrite ge_max lexx /=; case: ltP => //=; rewrite le_f.
 Qed.
 
 Lemma fposBfneg f x : fpos f x - fneg f x = f x.

theories/charge.v

@@ -623,7 +623,7 @@ Let nuA_g_ x : nu (A_ x) >= mine (g_ x * 2^-1%:E) 1.
 Proof. by move: x => [[[? ?] ?]] []. Qed.
 
 Let nuA_ge0 x : 0 <= nu (A_ x).
-Proof. by rewrite (le_trans _ (nuA_g_ _))// le_minr lee01 andbT mule_ge0. Qed.
+Proof. by rewrite (le_trans _ (nuA_g_ _))// le_min lee01 andbT mule_ge0. Qed.
 
 Let subDD A := [set nu E | E in [set E | measurable E /\ E `<=` D `\` A] ].
 
@@ -645,7 +645,7 @@ have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A.
   rewrite /m; have [->|dn1oo] := eqVneq (d_ A) +oo.
     by rewrite min_r ?ltey ?gt0_mulye ?leey.
   rewrite -(@fineK _ (d_ A)); last by rewrite gt0_fin_numE// ltey.
-  rewrite -EFinM -fine_min// lte_fin lt_minl; apply/orP; left.
+  rewrite -EFinM -fine_min// lte_fin gt_min; apply/orP; left.
   by rewrite ltr_pdivrMr// ltr_pMr ?ltr1n// fine_gt0// d_gt0/= ltey.
 by exists B; split => //; rewrite (le_trans _ (ltW mnuB)).
 Qed.
@@ -699,7 +699,7 @@ have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
 have mine_cvg_0 : (mine (g_ (v n) * 2^-1%:E) 1) @[n --> \oo] --> 0.
   apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n))));
     [|exact: cvg_cst|by []].
-  by apply: nearW => n /=; rewrite nuA_g_ andbT le_minr lee01 andbT mule_ge0.
+  by apply: nearW => n /=; rewrite nuA_g_ andbT le_min lee01 andbT mule_ge0.
 have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => //=.
 have nuDAoo : nu D >= nu (D `\` Aoo).
   rewrite -[in leRHS](@setDUK _ Aoo D); last first.
@@ -780,7 +780,7 @@ have /ereal_inf_lt/cid2[_ [B/= [mB BU] <-] nuBm] : s_ U < m.
   rewrite /m; have [->|s0oo] := eqVneq (s_ U) -oo.
     by rewrite max_r ?ltNye// gt0_mulNye// leNye.
   rewrite -(@fineK _ (s_ U)); last by rewrite lt0_fin_numE// ltNye.
-  rewrite -EFinM -fine_max// lte_fin lt_maxr; apply/orP; left.
+  rewrite -EFinM -fine_max// lte_fin lt_max; apply/orP; left.
   by rewrite ltr_pdivlMr// gtr_nMr ?ltr1n// fine_lt0// s_lt0/= ltNye andbT.
 have [C [CB nsC nuCB]] := hahn_decomposition_lemma nu mB.
 exists C; split => //; first exact: (subset_trans CB).
@@ -818,7 +818,7 @@ have znuD n : z_ (v n) <= nu D.
   apply: (subset_trans DP); apply: subsetC; rewrite Ubig.
   exact: bigsetU_bigcup.
 have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0.
-  by rewrite le_maxl leeN10 andbT pmule_lle0.
+  by rewrite ge_max leeN10 andbT pmule_lle0.
 have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo]  --> 0.
   move/fine_cvgP => -[zfin] /cvgrPdist_lt.
   have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R.
@@ -849,7 +849,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n -->
   rewrite (_ : _ \o _ = (fun n =>
     \sum_(0 <= k < n) fine (maxe (z_ (v k) * 2^-1%:E)%E (- 1%E)%E))%R) //.
   apply/funext => n/=; rewrite sum_fine// => m _.
-  rewrite le0_fin_numE; first by rewrite lt_maxr ltNyr orbT.
+  rewrite le0_fin_numE; first by rewrite lt_max ltNyr orbT.
   by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0.
 move/cvg_series_cvg_0 => maxe_cvg_0.
 apply: not_s_cvg_0.
@@ -864,13 +864,13 @@ apply/fine_cvgP; split.
     by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx.
   by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0.
 apply/cvgrPdist_lt => _ /posnumP[e].
-have : (0 < minr e%:num 1)%R by rewrite lt_minr// ltr01 andbT.
+have : (0 < minr e%:num 1)%R by rewrite lt_min// ltr01 andbT.
 move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.
 have /hM : (M <= n)%N by near: n; exists M.
 rewrite sub0r normrN /maxe/=; case: ifPn => [_|].
-  by rewrite normrN normr1 lt_minr ltxx andbF.
-by rewrite -leNgt => ? /lt_le_trans; apply; rewrite le_minl lexx.
+  by rewrite normrN normr1 lt_min ltxx andbF.
+by rewrite -leNgt => ? /lt_le_trans; apply; rewrite ge_min lexx.
 Unshelve. all: by end_near. Qed.
 
 Lemma Hahn_decomposition_uniq P1 N1 P2 N2 :

theories/constructive_ereal.v

@@ -61,7 +61,7 @@ Require Import signed.
 (*             x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E   *)
 (* ```                                                                        *)
 (*                                                                            *)
-(* ## Topology of extended real numbers                                        *)
+(* ## Topology of extended real numbers                                       *)
 (* ```                                                                        *)
 (*                       contract == order-preserving bijective function      *)
 (*                                   from extended real numbers to [-1; 1]    *)
@@ -1526,8 +1526,8 @@ split=> [-> // A A0|Ax]; first by rewrite leey.
 apply/eqP; rewrite eq_le leey /= leNgt; apply/negP.
 case: x Ax => [x Ax _|//|/(_ _ ltr01)//].
 suff: ~ x%:E < (Order.max 0 x + 1)%:E.
-  by apply; rewrite lte_fin ltr_pwDr// le_maxr lexx orbT.
-by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_maxr lexx.
+  by apply; rewrite lte_fin ltr_pwDr// le_max lexx orbT.
+by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_max lexx.
 Qed.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `eqyP`")]
@@ -3534,39 +3534,55 @@ Local Notation nR := {compare (0 : \bar R) & nz & r}.
 Implicit Type x y : nR.
 Local Notation num := (@num _ _ (0 : R) nz r).
 
-Lemma num_lee_maxr a x y :
+Lemma num_lee_max a x y :
   a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num).
-Proof. by rewrite -comparable_le_maxr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_le_max// ereal_comparable. Qed.
 
-Lemma num_lee_maxl a x y :
+Lemma num_gee_max a x y :
   maxe x%:num  y%:num <= a = (x%:num <= a) && (y%:num <= a).
-Proof. by rewrite -comparable_le_maxl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_ge_max// ereal_comparable. Qed.
 
-Lemma num_lee_minr a x y :
+Lemma num_lee_min a x y :
   a <= mine x%:num y%:num = (a <= x%:num) && (a <= y%:num).
-Proof. by rewrite -comparable_le_minr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_le_min// ereal_comparable. Qed.
 
-Lemma num_lee_minl a x y :
+Lemma num_gee_min a x y :
   mine x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).
-Proof. by rewrite -comparable_le_minl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_ge_min// ereal_comparable. Qed.
 
-Lemma num_lte_maxr a x y :
+Lemma num_lte_max a x y :
   a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).
-Proof. by rewrite -comparable_lt_maxr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_lt_max// ereal_comparable. Qed.
 
-Lemma num_lte_maxl a x y :
+Lemma num_gte_max a x y :
   maxe x%:num  y%:num < a = (x%:num < a) && (y%:num < a).
-Proof. by rewrite -comparable_lt_maxl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_gt_max// ereal_comparable. Qed.
 
-Lemma num_lte_minr a x y :
+Lemma num_lte_min a x y :
   a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).
-Proof. by rewrite -comparable_lt_minr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_lt_min// ereal_comparable. Qed.
 
-Lemma num_lte_minl a x y :
+Lemma num_gte_min a x y :
   mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).
-Proof. by rewrite -comparable_lt_minl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_gt_min// ereal_comparable. Qed.
 
 End MorphReal.
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_max`")]
+Notation num_lee_maxr := num_lee_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_max`")]
+Notation num_lee_maxl := num_gee_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_min`")]
+Notation num_lee_minr := num_lee_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_min`")]
+Notation num_lee_minl := num_gee_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_max`")]
+Notation num_lte_maxr := num_lte_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_max`")]
+Notation num_lte_maxl := num_gte_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_min`")]
+Notation num_lte_minr := num_lte_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_min`")]
+Notation num_lte_minl := num_gte_min (only parsing).
 
 Section MorphGe0.
 Context {R : numDomainType} {nz : KnownSign.nullity}.
@@ -3796,8 +3812,8 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
 - move: a b ltax ltxb; abstract: wlog. (*BUG*)
   move=> {}a {}b ltxa ltxb.
   have m_gt0 : (Num.min ((r - a) / 2) ((b - r) / 2) > 0)%R.
-    by rewrite lt_minr !divr_gt0 // ?subr_gt0.
-  exists (PosNum m_gt0) => y //=; rewrite lt_minr !ltr_distl.
+    by rewrite lt_min !divr_gt0 // ?subr_gt0.
+  exists (PosNum m_gt0) => y //=; rewrite lt_min !ltr_distl.
   move=> /andP[/andP[ay _] /andP[_ yb]].
   rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.
     rewrite -subr_gt0 opprD addrA {1}[(b - r)%R]splitr addrK.

theories/derive.v

@@ -783,9 +783,9 @@ Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
 Proof.
 move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
 apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
-rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_maxr /= lexx orbT.
+rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT.
 rewrite -ler_pdivlMl //.
-suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_maxr /= lexx.
+suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_max /= lexx.
 near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
 by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
 Unshelve. all: by end_near. Qed.
@@ -849,7 +849,7 @@ Lemma eqo_pair (U V' W' : normedModType R) (F : filter_on U)
   (f : U -> V') (g : U -> W') :
   (fun t => ([o_F id of f] t, [o_F id of g] t)) =o_F id.
 Proof.
-apply/eqoP => _/posnumP[e]; near=> x; rewrite num_le_maxl /=.
+apply/eqoP => _/posnumP[e]; near=> x; rewrite num_ge_max /=.
 by apply/andP; split; near: x; apply: littleoP.
 Unshelve. all: by end_near. Qed.