rm \near _, _ notation

CHANGELOG_UNRELEASED.md

@@ -386,6 +386,11 @@
 - in `radon_nikodym.v`:
   + notation `induced` (deprecated since 1.15.0)
 
+- in `filter.v`:
+  + notation `\near x, P x`
+  + notation `\near x & y, P x y`
+  + ltac `near_simpl`
+
 ### Infrastructure
 
 ### Misc

analysis_stdlib/Rstruct_topology.v

@@ -20,7 +20,6 @@ From mathcomp Require exp.
 (* The following line is for RcosE, PIE and RsinE. *)
 From mathcomp Require trigonometry_functions.
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -88,7 +87,7 @@ by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP.
 Qed.
 
 Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) :
-  nbhs (f x) P -> continuity_pt f x -> \near x, P (f x).
+  nbhs (f x) P -> continuity_pt f x -> \forall x0 \near x, P (f x0).
 Proof. by move=> Lf /continuity_pt_cvg; apply. Qed.
 
 End analysis_struct.

classical/filter.v

@@ -147,12 +147,10 @@ From mathcomp Require Import boolp classical_sets functions wochoice
 (*                                     Prefer this notation when the          *)
 (*                                     statement forall x, P x does not stand *)
 (*                                     alone.                                 *)
-(*                     \near x, P x := \forall y \near x, P y.                *)
 (*                  {near F & G, P} == same as {near H, P}, where H is the    *)
 (*                                     product of the filters F and G         *)
 (*   \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y}  *)
 (*     \forall x & y \near F, P x y == same as before, with G = F             *)
-(*               \near x & y, P x y := \forall z \near x & t \near y, P x y   *)
 (*                     x \is_near F == x belongs to a set P : in_filter F     *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -196,9 +194,6 @@ Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near'  x ,  P }").
 Reserved Notation "'\forall' x '\near' x_0 , P"
   (at level 200, x name, P at level 200,
    format "'\forall'  x  '\near'  x_0 ,  P").
-Reserved Notation "'\near' x , P"
-  (at level 200, x at level 99, P at level 200,
-   format "'\near'  x ,  P", only parsing).
 Reserved Notation "{ 'near' x & y , P }"
   (at level 0, format "{ 'near'  x  &  y ,  P }").
 Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P"
@@ -207,9 +202,6 @@ Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P"
 Reserved Notation "'\forall' x & y '\near' z , P"
   (at level 200, x name, y name, P at level 200,
    format "'\forall'  x  &  y  '\near'  z ,  P").
-Reserved Notation "'\near' x & y , P"
-  (at level 200, x, y at level 99, P at level 200,
-   format "'\near'  x  &  y ,  P", only parsing).
 (*Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter'  'of'  x ]").*)
 Reserved Notation "F `=>` G" (at level 70, format "F  `=>`  G").
 Reserved Notation "F --> G" (at level 70, format "F  -->  G").
@@ -289,14 +281,12 @@ End Near.
 
 Notation "{ 'near' x , P }" := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope.
 Notation "'\forall' x '\near' x_0 , P" := {near x_0, forall x, P} : type_scope.
-Notation "'\near' x , P" := (\forall x \near x, P) : type_scope.
 Notation "{ 'near' x & y , P }" :=
   (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope.
 Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" :=
   {near x_0 & y_0, forall x y, P} : type_scope.
 Notation "'\forall' x & y '\near' z , P" :=
   {near z & z, forall x y, P} : type_scope.
-Notation "'\near' x & y , P" := (\forall x \near x & y \near y, P) : type_scope.
 Arguments prop_near1 : simpl never.
 Arguments prop_near2 : simpl never.
 
@@ -401,11 +391,11 @@ Arguments cvgP {T F} l.
 Arguments dvgP {T F}.
 
 Lemma nbhs_nearE {U} {T : filteredType U} (x : T) (P : set U) :
-  nbhs x P = \near x, P x.
+  nbhs x P = \forall x0 \near x, P x0.
 Proof. by []. Qed.
 
 Lemma near_nbhs {U} {T : filteredType U} (x : T) (P : set U) :
-  (\forall x \near nbhs x, P x) = \near x, P x.
+  (\forall x0 \near nbhs x, P x0) = (\forall x0 \near x, P x0).
 Proof. by []. Qed.
 
 Lemma near2_curry {U V} (F : set_system U) (G : set_system V) (P : U -> set V) :
@@ -424,8 +414,7 @@ Lemma filter_of_nearI (X : Type) (fX : filteredType X)
 Proof. by []. Qed.
 
 Module Export NearNbhs.
-Definition near_simpl := (@near_nbhs, @nbhs_nearE, filter_of_nearI).
-Ltac near_simpl := rewrite ?near_simpl.
+Definition near_simpl := (@near_nbhs, filter_of_nearI).
 End NearNbhs.
 
 Lemma near_swap {U V} (F : set_system U) (G : set_system V) (P : U -> set V) :
@@ -525,7 +514,7 @@ Lemma filter_nbhsT {T : Type} (F : set_system T) :
 Proof. by move=> FF; apply: filterT. Qed.
 #[global] Hint Resolve filter_nbhsT : core.
 
-Lemma nearT {T : Type} (F : set_system T) : Filter F -> \near F, True.
+Lemma nearT {T : Type} (F : set_system T) : Filter F -> \forall _ \near F, True.
 Proof. by move=> FF; apply: filterT. Qed.
 #[global] Hint Resolve nearT : core.
 
@@ -693,10 +682,9 @@ Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) :
 Proof. by exists i. Qed.
 
 Lemma in_nearW {T : Type} (F : set_system T) (P : T -> Prop) (S : set T) :
-  Filter F -> F S -> {in S, forall x, P x} -> \near F, P F.
+  Filter F -> F S -> {in S, forall x, P x} -> \forall x \near F, P x.
 Proof.
-move=> FF FS SP; rewrite -nbhs_nearE.
-by apply: (@filterS _ F _ S) => // x /mem_set /SP.
+by move=> FF FS SP; apply: (@filterS _ F _ S) => // x /mem_set /SP.
 Qed.
 
 Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F ->
@@ -809,7 +797,7 @@ by move=> i; rewrite inE/= => _; apply: (fIF i).
 Qed.
 
 Lemma filter_imply [T : Type] [P : Prop] [f : set T] [F : set_system T] :
-  Filter F -> (P -> \near F, f F) -> \near F, P -> f F.
+  Filter F -> (P -> \forall x \near F, f x) -> \forall x \near F, P -> f x.
 Proof.
 move=> ? PF; near do move=> /asboolP.
 by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW].
@@ -990,7 +978,7 @@ HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) :=
 
 Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
     {for x, continuous f} ->
-  (\forall y \near f x, P y) -> (\near x, P (f x)).
+  (\forall y \near f x, P y) -> (\forall x0 \near x, P (f x0)).
 Proof. exact. Qed.
 Arguments near_fun {T T'} f x.
 
@@ -1223,7 +1211,7 @@ split.
 - move=> fFAG; split.
   + exact/(cvg_trans fFAG)/cvg_within.
   + by apply/fFAG; exact: withinT.
-- move=> [+ fA] B => /[apply]; rewrite 2!nbhs_nearE !near_map.
+- move=> [+ fA] B => /[apply]; rewrite nbhs_simpl.
   by apply: filterS2 fA => t ?; exact.
 Unshelve. all: by end_near. Qed.
 

theories/derive.v

@@ -891,7 +891,7 @@ 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_max /= lexx.
-near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
+near: x; apply/nbhs_le_nbhs_norm.
 by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
 Unshelve. all: by end_near. Qed.
 
@@ -2197,7 +2197,7 @@ Qed.
 
 Lemma near_eq_derive {R : numFieldType} {V W : normedModType R}
   (f g : V -> W) (a v : V) :
-  (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
+  (\forall a0 \near a, f a0 = g a0) -> 'D_v f a = 'D_v g a.
 Proof.
 have [-> _|] := eqVneq v 0; first by rewrite !derive0.
 move=> v0 fg; rewrite /derive; congr (lim _).
@@ -2207,7 +2207,7 @@ Unshelve. all: by end_near. Qed.
 
 Lemma near_eq_is_derive {R : numFieldType} {V W : normedModType R}
     (f g : V -> W) (a v : V) (df : W) :
-  (\near a, f a = g a) -> is_derive a v f df -> is_derive a v g df.
+  (\forall a0 \near a, f a0 = g a0) -> is_derive a v f df -> is_derive a v g df.
 Proof.
 move=> fg [fav <-]; rewrite (near_eq_derive _ fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
@@ -2222,7 +2222,7 @@ Lemma near_eq_derive1n_near n f g x:
 Proof.
 move=> fg; elim: n => [//|n IH].
 near do (rewrite 2!derive1nS !derive1E; apply: near_eq_derive).
-by rewrite near_nbhs; exact: near_join.
+exact: (@near_join _ x).
 Unshelve. all: by end_near. Qed.
 
 Lemma near_eq_derive1_near f g x : {near x, f =1 g} -> {near x, f^`() =1 g^`()}.

theories/ereal.v

@@ -1622,15 +1622,16 @@ Qed.
 Section nbhs_ereal.
 Context {R : numFieldType} (P : \bar R -> Prop).
 
-Lemma nbhs_EFin (x : R) : (\forall y \near x%:E, P y) <-> \near x, P x%:E.
-Proof. done. Qed.
+Lemma nbhs_EFin (x : R) :
+  (\forall y \near x%:E, P y) <-> \forall x0 \near x, P x0%:E.
+Proof. by []. Qed.
 
 End nbhs_ereal.
 
 Section cvg_fin.
 Context {R : numFieldType} {F : set_system \bar R} {FF : Filter F}.
 
-Lemma fcvg_is_fine a : F --> a%:E -> \near F, F \is a fin_num.
+Lemma fcvg_is_fine a : F --> a%:E -> \forall x \near F, x \is a fin_num.
 Proof. by apply; apply/nbhs_EFin; near=> x. Unshelve. all: by end_near. Qed.
 
 End cvg_fin.
@@ -1653,7 +1654,8 @@ Section limit.
 Context {R : numFieldType} {I : Type} {F : set_system I} {FF : Filter F}
   (f : I -> \bar R).
 
-Lemma cvg_EFin a : (\near F, f F \is a fin_num) -> fine \o f @ F --> a ->
+Lemma cvg_EFin a :
+    (\forall x \near F, f x \is a fin_num) -> fine \o f @ F --> a ->
   f @ F --> a%:E.
 Proof.
 move=> Ffin Fa P/= /nbhs_EFin /Fa; rewrite !near_simpl.
@@ -1663,11 +1665,12 @@ Qed.
 Lemma fine_cvg a : f @ F --> a%:E -> fine \o f @ F --> a.
 Proof. exact: fine_fcvg. Qed.
 
-Lemma cvg_is_fine a : f @ F --> a%:E -> \near F, f F \is a fin_num.
+Lemma cvg_is_fine a : f @ F --> a%:E -> \forall x \near F, f x \is a fin_num.
 Proof. exact: fcvg_is_fine. Qed.
 
 Lemma fine_cvgP a :
-   f @ F --> a%:E <-> (\near F, f F \is a fin_num) /\ fine \o f @ F --> a.
+   f @ F --> a%:E <->
+   (\forall x \near F, f x \is a fin_num) /\ fine \o f @ F --> a.
 Proof.
 by split;[split;[exact: (@cvg_is_fine a)|exact: fine_cvg]|case; apply: cvg_EFin].
 Qed.

theories/ftc.v

@@ -1743,7 +1743,7 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R).
   apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl/=; near=> z.
   rewrite derive1E deriveN -?derive1E//.
   apply: dF.
-  near: z; rewrite near_nbhs.
+  near: z.
   apply: (@open_in_nearW _ _ `]a, +oo[).
   + exact: interval_open.
   + by move=> ?; rewrite inE.
@@ -1785,9 +1785,7 @@ have mF' : measurable_fun `]a, +oo[ (- F)%R^`().
   apply: near_eq_cvg => /=; rewrite near_simpl; near=> z.
   rewrite !derive1E deriveN ?opprK//.
   apply: dF.
-  near: z.
-  rewrite near_nbhs.
-  exact: near_in_itvoy.
+  by near: z; exact: near_in_itvoy.
 rewrite -!integral_itvob_itvcb.
 - apply/measurable_EFinP; apply: measurable_funM; last exact: measurableT_comp.
   apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)).

theories/landau.v

@@ -1115,7 +1115,8 @@ Lemma linear_for_continuous (f : {linear U -> V | GRing.Scale.Law.sort s}) :
   (f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.
 Proof.
 move=> /eqO_exP [_/posnumP[k0] Of1] x.
-apply/cvgrPdist_lt => _/posnumP[e]; rewrite !near_simpl.
+apply/cvgrPdist_lt => /= _/posnumP[e].
+suff: \forall t \near x, `|f x - f t| < e%:num by [].
 rewrite (near_shift 0) /= subr0; near=> y => /=.
 rewrite -linearB opprD addrC addrNK linearN normrN; near: y.
 suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|.

theories/normedtype_theory/ereal_normedtype.v

@@ -29,7 +29,6 @@ From mathcomp Require Import topology ereal num_normedtype.
 (*                                                                            *)
 (******************************************************************************)
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -432,24 +431,26 @@ End ereal_is_hausdorff.
 Hint Extern 0 (hausdorff_space _) => solve[apply: ereal_hausdorff] : core.
 
 Section ProperFilterERealType.
-Context {T : Type} {a : set_system T} {Fa : ProperFilter a} {R : realFieldType}.
+Context {T : Type} {F : set_system T} {FF : ProperFilter F} {R : realFieldType}.
 Local Open Scope ereal_scope.
 Implicit Types f g h : T -> \bar R.
 
-Lemma cvge_to_ge f b c : f @ a --> c -> (\near a, b <= f a) -> b <= c.
+Lemma cvge_to_ge f b c : f @ F --> c -> (\forall a \near F, b <= f a) -> b <= c.
 Proof.
 by move=> /[swap]/(closed_cvg _ (@closed_ereal_le_ereal _ b)) /[apply].
 Qed.
 
-Lemma cvge_to_le f b c : f @ a --> c -> (\near a, f a <= b) -> c <= b.
+Lemma cvge_to_le f b c : f @ F --> c -> (\forall a \near F, f a <= b) -> c <= b.
 Proof.
 by move=> /[swap]/(closed_cvg _ (@closed_ereal_ge_ereal _ b))/[apply].
 Qed.
 
-Lemma lime_ge x f : cvg (f @ a) -> (\near a, x <= f a) -> x <= lim (f @ a).
+Lemma lime_ge x f :
+  cvg (f @ F) -> (\forall a \near F, x <= f a) -> x <= lim (f @ F).
 Proof. exact: cvge_to_ge. Qed.
 
-Lemma lime_le x f : cvg (f @ a) -> (\near a, x >= f a) -> x >= lim (f @ a).
+Lemma lime_le x f :
+  cvg (f @ F) -> (\forall a \near F, x >= f a) -> x >= lim (f @ F).
 Proof. exact: cvge_to_le. Qed.
 
 End ProperFilterERealType.