Merge pull request #308 from math-comp/remove_typeclasses_opaque

remove typeclasses opaque fmap
math-comp · Dec 21, 2020 · 7f1e7db · 7f1e7db
2 parents b96bf5a + f111cfe
commit 7f1e7db
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 43 deletions.
diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -1039,13 +1039,9 @@ Lemma continuous_cvg_dist {R : numFieldType}
   (V W : normedModType R) (f : V -> W) x l :
   continuous f -> x --> l -> forall e : {posnum R}, `|f l - f x| < e%:num.
 Proof.
-move=> cf xl e.
-move/cvg_dist: (cf l) => /(_ _ (posnum_gt0 e)).
-rewrite nearE /= => /nbhs_ballP [i i0]; apply.
-have /@cvg_dist : Filter [filter of x] by apply: filter_on_Filter.
-move/(_ _ xl _ i0).
-rewrite nearE /= => /nbhs_ballP [j j0].
-by move/(_ _ (ballxx _ j0)); rewrite -ball_normE.
+move=> + + e => /(_ l)/cvg_dist/(_ _ (posnum_gt0 e)).
+rewrite near_map => /nbhs_ballP[_/posnumP[a]] + xl; apply.
+move/cvg_ball : xl => /(_ _ a)/nbhs_ballP[_/posnumP[b]]; apply; exact: ballxx.
 Qed.
 
 Module BigmaxBigminr.
@@ -1603,9 +1599,9 @@ Qed.
 
 Lemma norm_continuous : continuous ((@normr _ V) : V -> K^o).
 Proof.
-move=> x; apply/(@cvg_distP _ [normedModType K of K^o]) => _/posnumP[e] /=.
-rewrite !near_simpl; apply/nbhs_normP; exists e%:num => // y Hy.
-by rewrite -ball_normE in Hy; apply/(le_lt_trans (ler_dist_dist _ _)).
+move=> x; apply/cvg_distP => _/posnumP[e].
+rewrite near_map; apply/nbhs_normP; exists e%:num => // y.
+by rewrite -ball_normE; apply/(le_lt_trans (ler_dist_dist _ _)).
 Qed.
 
 End NVS_continuity_normedModType.
@@ -2165,8 +2161,7 @@ suff [a_ anx] : exists a_, forall n, a_ n != x /\ (U n `&` A) (a_ n).
   exists a_; split.
   - by move=> a [n _ <-]; have [? []] := anx n.
   - by move=> n; have [] := anx n.
-  - apply/cvg_distP; first by exact: fmap_filter.
-    move=> _/posnumP[e]; rewrite near_map; near=> n.
+  - apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> n.
     have [? [] xann Aan] := anx n.
     by rewrite (lt_le_trans xann) // ltW //; near: n; exact: near_infty_natSinv_lt.
 have @a_ : nat -> T^o.
@@ -2270,8 +2265,7 @@ rewrite /mkset le_eqVlt => /orP[/eqP <-{v}|]; last first.
 apply/subset_limit_point/limit_pointP; exists (fun n => z + n.+1%:R^-1); split.
 - by move=> u [] m _ <-; rewrite ltr_addl.
 - by move=> n; rewrite -subr_eq0 addrAC subrr add0r.
-- apply/cvg_distP; first exact: fmap_filter.
-  move=> _/posnumP[e]; rewrite near_map; near=> n.
+- apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> n.
   rewrite opprD addrA subrr add0r normrN ger0_norm //.
   by near: n; exact: near_infty_natSinv_lt.
 Grab Existential Variables. all: end_near. Qed.
@@ -2285,8 +2279,7 @@ rewrite /mkset le_eqVlt => /orP[/eqP <-{z}|]; last first.
 apply/subset_limit_point/limit_pointP; exists (fun n => v - n.+1%:R^-1); split.
 - by move=> u [] m _ <-; rewrite ltr_subl_addl ltr_addr.
 - by move=> n; rewrite -subr_eq0 addrAC subrr add0r oppr_eq0.
-- apply/cvg_distP; first exact: fmap_filter.
-  move=> _/posnumP[e]; rewrite near_map; near=> n.
+- apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> n.
   rewrite opprD addrA subrr add0r opprK ger0_norm //.
   by near: n; exact: near_infty_natSinv_lt.
 Grab Existential Variables. all: end_near. Qed.
@@ -3079,9 +3072,7 @@ Lemma continuous_withinNx (R : numFieldType) {U V : pseudoMetricType R}
 Proof.
 split=> - cfx P /= fxP.
   rewrite /nbhs' !near_simpl near_withinE.
-  by rewrite /nbhs'; apply: cvg_within; apply/cfx.
- (* :BUG: ssr apply: does not work,
-    because the type of the filter is not inferred *)
+  by apply: cvg_within; apply: cfx.
 rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP.
 rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].

diff --git a/theories/sequences.v b/theories/sequences.v
@@ -413,8 +413,7 @@ move=> u_nd u_M; set S := _ @` _; set M0 := sup S.
 have supS : has_sup S.
   split; first by exists (u_ 0%N), 0%N.
   by exists M; apply/ubP => x -[n _ <-{x}].
-apply: cvg_distW; first exact: fmap_filter.
-move=> _/posnumP[e]; rewrite near_map.
+apply: cvg_distW => _/posnumP[e]; rewrite near_map.
 have [p /andP[M0u_p u_pM0]] : exists p, M0 - e%:num <= u_ p <= M0.
   have [x] := sup_adherent supS (posnum_gt0 e).
   move=> -[p _] <-{x} => /ltW M0u_p.
@@ -496,8 +495,7 @@ Proof. exact/ltW/harmonic_gt0. Qed.
 
 Lemma cvg_harmonic {R : archiFieldType} : harmonic --> (0 : R^o).
 Proof.
-apply: cvg_distW; first exact: fmap_filter.
-move=> _/posnumP[e]; rewrite near_map; near=> i.
+apply: cvg_distW => _/posnumP[e]; rewrite near_map; near=> i.
 rewrite distrC subr0 ger0_norm//= -lef_pinv ?qualifE// invrK.
 rewrite (le_trans (ltW (archi_boundP _)))// ler_nat -add1n -leq_subLR.
 by near: i; apply: nbhs_infty_ge.
@@ -529,8 +527,7 @@ move=> u0_cvg; have ssplit v_ m n : (m <= n)%N -> `|n%:R^-1 * series v_ n| <=
     n%:R^-1 * `|series v_ m| + n%:R^-1 * `|\sum_(m <= i < n) v_ i|.
   move=> /subnK<-; rewrite series_addn mulrDr (le_trans (ler_norm_add _ _))//.
   by rewrite !normrM ger0_norm ?invr_ge0 ?ler0n.
-apply/cvg_distP; first exact: fmap_filter.
-move=> _/posnumP[e]; rewrite near_simpl; near \oo => m; near=> n.
+apply/cvg_distP=> _/posnumP[e]; rewrite near_simpl; near \oo => m; near=> n.
 have {}/ssplit -/(_ _ [sequence l - u_ n]_n) : (m.+1 <= n.+1)%nat by near: n; exists m.
 rewrite /series /= big_split/= sumrN mulrBr sumr_const card_ord -(mulr_natl l) mulKf//.
 move=> /le_lt_trans->//; rewrite [e%:num]splitr ltr_add//.
@@ -559,8 +556,7 @@ Let cesaro_converse_off_by_one (u_ : R^o ^nat) :
   [sequence n.+1%:R^-1 * series u_ n.+1]_ n --> (0 : R^o) ->
   [sequence n.+1%:R^-1 * series u_ n]_ n --> (0 : R^o).
 Proof.
-move=> H; apply/cvg_distP; first exact: fmap_filter.
-move=> _/posnumP[e]; rewrite near_map.
+move=> H; apply/cvg_distP => _/posnumP[e]; rewrite near_map.
 move/cvg_distP : H => /(_ e%:num (posnum_gt0 e)); rewrite near_map => -[m _ mu].
 near=> n; rewrite sub0r normrN /=.
 have /andP[n0] : ((0 < n) && (m <= n.-1))%N.
@@ -772,8 +768,7 @@ Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) :
   cvg [normed series u_] -> cvg (series u_).
 Proof.
 move=> /cauchy_cvgP/cauchy_seriesP u_ncvg.
-apply/cauchy_cvgP; first exact: fmap_proper_filter.
-apply/cauchy_seriesP => e /u_ncvg.
+apply/cauchy_cvgP/cauchy_seriesP => e /u_ncvg.
 apply: filterS => n /=; rewrite ger0_norm ?sumr_ge0//.
 by apply: le_lt_trans; apply: ler_norm_sum.
 Qed.
@@ -828,8 +823,7 @@ Qed.
 Lemma dvg_ereal_cvg (R : realFieldType) (u_ : (R^o) ^nat) :
   u_ --> +oo -> (fun n => (u_ n)%:E) --> +oo%E.
 Proof.
-move/cvgPpinfty_lt => uoo; apply/cvg_ballP; first exact: fmap_filter.
-move=> _/posnumP[e]; rewrite near_map.
+move/cvgPpinfty_lt => uoo; apply/cvg_ballP => _/posnumP[e]; rewrite near_map.
 have [e1|e1] := lerP 1 e%:num.
   case: (uoo _ ltr01) => k _ k1un; near=> n.
   rewrite /ball /= /ereal_ball [contract +oo]/= ger0_norm ?subr_ge0; last first.
@@ -900,8 +894,7 @@ have [/eqP|lnoo] := boolP (l == -oo%E).
   move/ereal_sup_ninfty => loo.
   suff : u_ = (fun=> -oo%E) by [].
   by rewrite funeqE => m; apply (loo (u_ m)); exists m.
-apply/cvg_ballP; first exact: fmap_filter.
-move=> _/posnumP[e].
+apply/cvg_ballP => _/posnumP[e].
 have [/eqP {lnoo}loo|lpoo] := boolP (l == +oo%E).
   rewrite near_map; near=> n; rewrite /ball /= /ereal_ball.
   have unoo : u_ n != -oo%E.

diff --git a/theories/topology.v b/theories/topology.v
@@ -942,7 +942,7 @@ Proof. by move=> FF FP; apply: filterS filterT. Qed.
 
 Lemma filterE {T : Type} {F : set (set T)} :
   Filter F -> forall P : set T, (forall x, P x) -> F P.
-Proof. by move=> ???; near=> x => //. Unshelve. end_near. Qed.
+Proof. by move=> [FT _ +] P fP => /(_ setT); apply. Qed.
 
 Lemma filter_app (T : Type) (F : set (set T)) :
   Filter F -> forall P Q : set T, F (fun x => P x -> Q x) -> F P -> F Q.
@@ -1096,7 +1096,7 @@ move=> FF; constructor => [|P Q|P Q PQ]; rewrite ?fmapE ?filter_ofE //=.
 - exact: filterI.
 - by apply: filterS=> ?/PQ.
 Qed.
-Typeclasses Opaque fmap.
+(*Typeclasses Opaque fmap.*)
 
 Global Instance fmap_proper_filter T U (f : T -> U) (F : set (set T)) :
   ProperFilter F -> ProperFilter (f @ F).
@@ -1121,7 +1121,7 @@ Proof. by []. Qed.
 Global Instance fmapi_filter T U (f : T -> set U) (F : set (set T)) :
   infer {near F, is_totalfun f} -> Filter F -> Filter (f `@ F).
 Proof.
-move=> f_totalfun FF; rewrite /fmapi; apply: Build_Filter. (* bug *)
+move=> f_totalfun FF; rewrite /fmapi; apply: Build_Filter.
 - by apply: filterS f_totalfun => x [[y Hy] H]; exists y.
 - move=> /= P Q FP FQ; near=> x.
     have [//|y [fxy Py]] := near FP x.
@@ -1323,9 +1323,8 @@ Lemma filter_pair_near_of (T T' : Type) (F : set (set T)) (F' : set (set T')) :
    filter_prod F F' Q.
 Proof.
 move=> FF FF' [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ.
-near=> x; have := PQ x.1 x.2; rewrite -surjective_pairing; apply; near: x;
-by [apply: cvg_fst|apply: cvg_snd].
-Grab Existential Variables. all: end_near. Qed.
+by exists (P, P') => //= -[t t'] [] /=; exact: PQ.
+Qed.
 
 Tactic Notation "near=>" ident(x) ident(y) :=
   (apply: filter_pair_near_of => x y ? ?).
@@ -1524,7 +1523,7 @@ rewrite nbhsE propeqE; split=> [[? ?]|[? [B [[? ?] BA]]]]; split => //;
   [by exists A; split | exact: BA].
 Qed.
 
-Definition interior (A : set T) := (@nbhs _ [filteredType T of T])^~ A.
+Definition interior (A : set T) := (@nbhs _ T)^~ A.
 
 Local Notation "A ^°" := (interior A).
 
@@ -3238,9 +3237,7 @@ Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x :
 Proof.
 split=> - cfx P /= fxP.
   rewrite /nbhs' !near_simpl near_withinE.
-  by rewrite /nbhs'; apply: cvg_within; apply/cfx.
- (* :BUG: ssr apply: does not work,
-    because the type of the filter is not inferred *)
+  by rewrite /nbhs'; apply: cvg_within; apply: cfx.
 rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP.
 rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].