in_setE/in_fsetE -> inE

theories/classical_sets.v

@@ -1,5 +1,4 @@
-From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
-From mathcomp Require Import fintype bigop ssralg matrix.
+From mathcomp Require Import all_ssreflect ssralg matrix finmap.
 Require Import boolp.
 
 (******************************************************************************)
@@ -162,12 +161,16 @@ Canonical Prop_eqType := EqType Prop gen_eqMixin.
 Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin.
 
 Definition set A := A -> Prop.
-Definition in_set T (P : set T) : pred T := [pred x | `[<P x>]].
+(* we use fun x => instead of pred to prevent inE from working *)
+(* we will then extend inE with in_setE to make this work      *)
+Definition in_set T (P : set T) : pred T := (fun x => `[<P x>]).
 Canonical set_predType T := @PredType T (set T) (@in_set T).
 
 Lemma in_setE T (P : set T) x : x \in P = P x :> Prop.
 Proof. by rewrite propeqE; split => [] /asboolP. Qed.
 
+Definition inE := (inE, in_setE).
+
 Bind Scope classical_set_scope with set.
 Local Open Scope classical_set_scope.
 Delimit Scope classical_set_scope with classic.
@@ -463,8 +466,8 @@ Lemma setUDr T : right_distributive (@setU T) (@setI T).
 Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUDl. Qed.
 
 Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
-Definition is_fun {A B} (f : A -> B -> Prop) := all (is_subset1 \o f).
-Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).
+Definition is_fun {A B} (f : A -> B -> Prop) := Logic.all (is_subset1 \o f).
+Definition is_total {A B} (f : A -> B -> Prop) := Logic.all (nonempty \o f).
 Definition is_totalfun {A B} (f : A -> B -> Prop) :=
   forall x, nonempty (f x) /\ is_subset1 (f x).
 

theories/derive.v

@@ -1313,33 +1313,32 @@ Proof.
 move=> leab fcont; set imf := [pred t | t \in f @` [set x | x \in `[a, b]]].
 have imf_sup : has_sup imf.
   apply/has_supP; split.
-    by exists (f a); rewrite !inE; apply/asboolP/imageP; rewrite inE/= lexx.
+    by exists (f a); rewrite !inE; apply/imageP; rewrite inE/= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` [set x | x \in `[a, b]] : set R^o).
     apply/compact_bounded/continuous_compact; last exact: segment_compact.
-    by move=> ?; rewrite inE => /asboolP /fcont.
-  exists (M + 1); apply/ubP => y; rewrite !inE => /asboolP /imfltM yleM.
+    by move=> ?; rewrite inE => /fcont.
+  exists (M + 1); apply/ubP => y; rewrite !inE => /imfltM yleM.
   apply: le_trans (yleM _ _); last by rewrite ltr_addl.
   by rewrite ler_norm.
 case: (pselect (exists2 c, c \in `[a, b] & f c = sup imf)) => [|imf_ltsup].
   move=> [c cab fceqsup]; exists c => // t tab.
-  rewrite fceqsup; apply: sup_upper_bound=> //; rewrite !inE; apply/asboolP.
-  exact: imageP.
+  by rewrite fceqsup; apply: sup_upper_bound=> //; rewrite !inE; apply: imageP.
 have {imf_ltsup} imf_ltsup : forall t, t \in `[a, b] -> f t < sup imf.
   move=> t tab; case: (ltrP (f t) (sup imf))=> // supleft.
   rewrite falseE; apply: imf_ltsup; exists t => //.
   apply/eqP; rewrite eq_le supleft sup_upper_bound => //.
-  by rewrite !inE; apply/asboolP/imageP.
+  by rewrite !inE; apply/imageP.
 have invf_continuous : {in `[a, b], continuous (fun t => (sup imf - f t)^-1 : R^o)}.
   move=> t tab; apply: cvgV.
     by rewrite neq_lt subr_gt0 orbC imf_ltsup.
   by apply: cvgD; [apply: continuous_cst|apply: cvgN; apply:fcont].
 have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] :
    bounded_set ((fun t => (sup imf - f t)^-1) @` [set x | x \in `[a, b]] : set R^o).
   apply/compact_bounded/continuous_compact; last exact: segment_compact.
-  by move=> ?; rewrite inE => /asboolP /invf_continuous.
+  by move=> ?; rewrite inE => /invf_continuous.
 have : exists2 y, y \in imf & sup imf - k^-1 < y.
   by apply: sup_adherent => //; rewrite invr_gt0.
-move=> [y]; rewrite !inE => /asboolP [t tab <-] {y}.
+move=> [y]; rewrite !inE => -[t tab <-] {y}.
 rewrite ltr_subl_addr -ltr_subl_addl.
 suff : sup imf - f t > k^-1 by move=> /ltW; rewrite leNgt => /negbTE ->.
 rewrite -[X in _ < X]invrK ltf_pinv ?qualifE ?invr_gt0 ?subr_gt0 ?imf_ltsup//.

theories/normedtype.v

@@ -2399,25 +2399,25 @@ move=> FF F_cauchy; apply/cvg_ex.
 pose D := \bigcap_(A in F) (down (mem A)).
 have /cauchyP /(_ 1) [//|x0 x01] := F_cauchy.
 have D_has_sup : has_sup (mem D); first split.
-- exists (x0 - 1); rewrite in_setE => A FA.
+- exists (x0 - 1); rewrite inE => A FA.
   apply/existsbP; near F => x; first exists x.
-    by rewrite ler_distW 1?distrC 1?ltW ?andbT ?in_setE //; near: x.
-- exists (x0 + 1); apply/forallbP => x; apply/implyP; rewrite in_setE.
-  move=> /(_ _ x01) /existsbP [y /andP[]]; rewrite in_setE.
+    by rewrite ler_distW 1?distrC 1?ltW ?andbT ?inE //; near: x.
+- exists (x0 + 1); apply/forallbP => x; apply/implyP; rewrite inE.
+  move=> /(_ _ x01) /existsbP [y /andP[]]; rewrite inE.
   rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltW].
   by move=> /(le_trans _) yx01 _ /yx01.
 exists (sup (mem D)).
 apply: (cvg_distW (_ : R^o)) => /= _ /posnumP[eps]; near=> x.
 rewrite ler_distl sup_upper_bound //=.
   apply: sup_le_ub => //; first by case: D_has_sup.
-  apply/forallbP => y; apply/implyP; rewrite in_setE.
+  apply/forallbP => y; apply/implyP; rewrite inE.
   move=> /(_ (ball_ (fun x => `| x |) x eps%:num) _) /existsbP [].
     by near: x; apply: nearP_dep; apply: F_cauchy.
-  move=> z /andP[]; rewrite in_setE /ball_ ltr_distl ltr_subl_addr.
+  move=> z /andP[]; rewrite inE /ball_ ltr_distl ltr_subl_addr.
   by move=> /andP [/ltW /(le_trans _) le_xeps _ /le_xeps].
-rewrite in_setE /D /= => A FA; near F => y.
+rewrite inE /D /= => A FA; near F => y.
 apply/existsbP; exists y; apply/andP; split.
-  by rewrite in_setE; near: y.
+  by rewrite inE; near: y.
 rewrite ler_subl_addl -ler_subl_addr ltW //.
 suff: `|x - y| < eps%:num by rewrite ltr_norml => /andP[_].
 by near: y; near: x; apply: nearP_dep; apply: F_cauchy.
@@ -2591,26 +2591,26 @@ have sAab : A `<=` [set x | x \in `[a, b]] by rewrite AeabB => ? [].
 move=> /asboolPn; rewrite asbool_and => /nandP [/asboolPn /(_ (sAab _))|] //.
 move=> /imply_asboolPn [abx nAx] [C Cop AeabC].
 set Altx := fun y => y \in A `&` [set y | y < x].
-have Altxn0 : reals.nonempty Altx by exists y; rewrite in_setE.
+have Altxn0 : reals.nonempty Altx by exists y; rewrite inE.
 have xub_Altx : x \in ub Altx.
-  by apply/ubP => ?; rewrite in_setE => - [_ /ltW].
+  by apply/ubP => ?; rewrite inE => - [_ /ltW].
 have Altxsup : has_sup Altx by apply/has_supP; split=> //; exists x.
 set z := sup Altx.
 have yxz : z \in `[y, x].
   rewrite inE; apply/andP; split; last exact: sup_le_ub.
-  by apply/sup_upper_bound => //; rewrite in_setE.
+  by apply/sup_upper_bound => //; rewrite inE.
 have Az : A z.
   rewrite AeabB; split.
     suff : {subset `[y, x] <= `[a, b]} by apply.
     by apply/subitvP; rewrite /= (itvP abx); have /sAab/itvP-> := Ay.
   apply: Bcl => D [_ /posnumP[e] ze_D].
   have [t] := sup_adherent Altxsup [gt0 of e%:num].
-  rewrite in_setE => - [At lttx] ltzet.
+  rewrite inE => - [At lttx] ltzet.
   exists t; split; first by move: At; rewrite AeabB => - [].
   apply/ze_D; rewrite /= ltr_distl.
   apply/andP; split; last by rewrite -ltr_subl_addr.
   rewrite ltr_subl_addr; apply: ltr_spaddr => //.
-  by apply/sup_upper_bound => //; rewrite in_setE.
+  by apply/sup_upper_bound => //; rewrite inE.
 have ltzx : 0 < x - z.
   have : z <= x by rewrite (itvP yxz).
   by rewrite subr_gt0 le_eqVlt => /orP [/eqP zex|] //; move: nAx; rewrite -zex.
@@ -2619,7 +2619,7 @@ suff [t Altxt] : exists2 t, Altx t & z < t.
   by rewrite ltNge => /negP; apply; apply/sup_upper_bound.
 exists (z + (minr (e%:num / 2) ((PosNum ltzx)%:num / 2))); last first.
   by rewrite ltr_addl.
-rewrite in_setE; split; last first.
+rewrite inE; split; last first.
   rewrite -[_ < _]ltr_subr_addl ltIx; apply/orP; right.
   by rewrite ltr_pdivr_mulr // mulrDr mulr1 ltr_addl.
 rewrite AeabC; split; last first.
@@ -2656,12 +2656,12 @@ suff Aeab : A = [set x | x \in `[a, b]].
 apply: segment_connected.
 - have aba : a \in `[a, b] by rewrite inE/=; apply/andP.
   exists a; split=> //; have /sabUf [i Di fia] := aba.
-  exists [fset i]%fset; first by move=> ?; rewrite inE in_setE => /eqP->.
+  exists [fset i]%fset; first by move=> ?; rewrite inE inE => /eqP->.
   split; last by exists i => //; rewrite inE.
   move=> x aex; exists i; [by rewrite inE|suff /eqP-> : x == a by []].
   by rewrite eq_le !(itvP aex).
 - exists B => //; rewrite openE => x [D' sD [saxUf [i Di fx]]].
-  have : open (f i) by have /sD := Di; rewrite in_setE => /fop.
+  have : open (f i) by have /sD := Di; rewrite inE => /fop.
   rewrite openE => /(_ _ fx) [e egt0 xe_fi]; exists e => // y xe_y.
   exists D' => //; split; last by exists i => //; apply/xe_fi.
   move=> z ayz; case: (lerP z x) => [lezx|ltxz].
@@ -2677,7 +2677,7 @@ move=> x clAx; have abx : x \in `[a, b].
 split=> //; have /sabUf [i Di fx] := abx.
 have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi].
 have /clAx [y [[aby [D' sD [sayUf _]]] xe_y]] := locally_ball x e.
-exists (i |` D')%fset; first by move=> j /fset1UP[->|/sD] //; rewrite in_setE.
+exists (i |` D')%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE.
 split=> [z axz|]; last first.
   exists i; first by rewrite !inE eq_refl.
   by apply/xe_fi; rewrite /ball_ subrr normr0.
@@ -3014,7 +3014,7 @@ move=> C D FC f_D; have {f_D} f_D :
   move=> _ [_ _ <-]; set s := [seq (@^~ j) @^-1` (get (Pj j)) | j : 'I_n.+1].
   exists [fset x in s]%fset.
     move=> B'; rewrite in_fset => /mapP [j _ ->]; rewrite inE.
-    apply/asboolP; exists j => //; exists (get (Pj j)) => //.
+    exists j => //; exists (get (Pj j)) => //.
     by have /getPex [[]] := exPj j.
   rewrite predeqE => g; split=> [Ig j|Ig B'].
     apply: (Ig ((@^~ j) @^-1` (get (Pj j)))).

theories/topology.v

@@ -1478,7 +1478,7 @@ Lemma open_comp  {T U : topologicalType} (f : T -> U) (D : set U) :
   {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D).
 Proof.
 rewrite !openE => fcont Dop x /= Dfx.
-by apply: fcont; [rewrite in_setE|apply: Dop].
+by apply: fcont; [rewrite inE|apply: Dop].
 Qed.
 
 Lemma cvg_fmap {T: topologicalType} {U : topologicalType}
@@ -1708,9 +1708,9 @@ Lemma finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i :
   D i -> finI_from D f (f i).
 Proof.
 move=> Di; exists [fset i]%fset.
-  by move=> ?; rewrite in_fsetE in_setE => /eqP->.
-rewrite predeqE => t; split=> [|fit]; first by apply; rewrite in_fsetE.
-by move=> ?; rewrite in_fsetE => /eqP->.
+  by move=> ?; rewrite !inE => /eqP->.
+rewrite predeqE => t; split=> [|fit]; first by apply; rewrite inE.
+by move=> ?; rewrite inE => /eqP->.
 Qed.
 
 Section TopologyOfSubbase.
@@ -1724,8 +1724,8 @@ move: i j t H H0 H1 H2 => A B t [DA sDAD AeIbA] [DB sDBD BeIbB] At Bt.
 exists (A `&` B); split; last by split.
 exists (DA `|` DB)%fset; first by move=> i /fsetUP [/sDAD|/sDBD].
 rewrite predeqE => s; split=> [Ifs|[As Bs] i /fsetUP].
-  split; first by rewrite -AeIbA => i DAi; apply: Ifs; rewrite in_fsetE DAi.
-  by rewrite -BeIbB => i DBi; apply: Ifs; rewrite in_fsetE DBi orbC.
+  split; first by rewrite -AeIbA => i DAi; apply: Ifs; rewrite inE DAi.
+  by rewrite -BeIbB => i DBi; apply: Ifs; rewrite inE DBi orbC.
 by move=> [DAi|DBi];
   [have := As; rewrite -AeIbA; apply|have := Bs; rewrite -BeIbB; apply].
 Qed.
@@ -1956,14 +1956,14 @@ move=> Ffilt; split=> cvFt.
   apply: cvFt; exists B; split=> //; exists [set B]; last first.
     by rewrite predeqE => ?; split=> [[_ ->]|] //; exists B.
   move=> _ ->; exists [fset B]%fset.
-    by move=> ?; rewrite in_fsetE in_setE => /eqP->; exists i.
-  by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite in_fsetE // =>/eqP->.
+    by move=> ?; rewrite inE inE => /eqP->; exists i.
+  by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite inE // =>/eqP->.
 move=> A /=; rewrite (@locallyE sup_topologicalType).
 move=> [_ [[[B sB <-] [C BC Ct]] sUBA]].
 rewrite locally_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C).
   by move=> ??; exists C.
 have /sB [D sD IDeC] := BC; rewrite -IDeC; apply: filter_bigI => E DE.
-have /sD := DE; rewrite in_setE => - [i _]; rewrite openE => Eop.
+have /sD := DE; rewrite inE => - [i _]; rewrite openE => Eop.
 by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE).
 Qed.
 
@@ -2095,7 +2095,7 @@ Proof.
 rewrite !closedE=> f_continuous D_cl x /= xDf; apply: D_cl; apply: contrap xDf => fxD.
 have NDfx : ~ D (f x).
   by move: fxD; rewrite -locally_nearE locallyE => - [A [[??]]]; apply.
-by apply: f_continuous fxD; rewrite in_setE.
+by apply: f_continuous fxD; rewrite inE.
 Qed.
 
 Lemma closed_cvg_loc {T} {U : topologicalType} {F} {FF : ProperFilter F}
@@ -2197,7 +2197,7 @@ have GF : ProperFilter G.
   by move=> C /(filterI FfA) /filter_ex [_ [[p ? <-]]]; eexists p.
 case: (Aco G); first by exists (f @` A) => // ? [].
 move=> p [Ap clsGp]; exists (f p); split; first exact/imageP.
-move=> B C FB /fcont; rewrite in_setE /= locally_filterE => /(_ Ap) p_Cf.
+move=> B C FB /fcont; rewrite inE /= locally_filterE => /(_ Ap) p_Cf.
 have : G (A `&` f @^-1` B) by exists B.
 by move=> /clsGp /(_ p_Cf) [q [[]]]; exists (f q).
 Qed.
@@ -2371,10 +2371,10 @@ move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)).
 - by exists setT; exists fset0 => //; rewrite predeqE.
 - move=> A B [DA sDA IfA] [DB sDB IfB]; exists (A `&` B) => //.
   exists (DA `|` DB)%fset.
-    by move=> ?; rewrite in_fsetE => /orP [/sDA|/sDB].
+    by move=> ?; rewrite inE => /orP [/sDA|/sDB].
   rewrite -IfA -IfB predeqE => p; split=> [Ifp|[IfAp IfBp] i].
-    by split=> i Di; apply: Ifp; rewrite in_fsetE Di // orbC.
-  by rewrite in_fsetE => /orP []; [apply: IfAp|apply: IfBp].
+    by split=> i Di; apply: Ifp; rewrite inE Di // orbC.
+  by rewrite inE => /orP []; [apply: IfAp|apply: IfBp].
 - by move=> _ [?? <-]; apply: finIf.
 Qed.
 
@@ -2383,7 +2383,7 @@ Lemma filter_finI (T : pointedType) (F : set (set T)) (D : set (set T))
   ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f.
 Proof.
 move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI.
-by move=> A /sD; rewrite in_setE => /sDFf.
+by move=> A /sD; rewrite inE => /sDFf.
 Qed.
 
 Section Covers.
@@ -2412,7 +2412,7 @@ rewrite predeqE => A; split=> [Aco I D f [g gop feAg] fcov|Aco I D f fop fcov].
     by move=> p /fcov [i Di]; rewrite feAg // => - []; exists i.
   have [D' sD sgcov] := Aco _ _ _ gop gcov.
   exists D' => // p Ap; have /sgcov [i D'i gip] := Ap.
-  by exists i => //; rewrite feAg //; have /sD := D'i; rewrite in_setE.
+  by exists i => //; rewrite feAg //; have /sD := D'i; rewrite inE.
 have Afcov : A `<=` \bigcup_(i in D) (A `&` f i).
   by move=> p Ap; have /fcov [i ??] := Ap; exists i.
 have Afop : open_fam_of A D (fun i => A `&` f i) by exists f.
@@ -2486,11 +2486,11 @@ have Anfop : open_fam_of A D (fun i => A `\` f i).
 have [D' sD sAnfcov] := Aco _ _ _ Anfop Anfcov.
 wlog [k D'k] : D' sD sAnfcov / exists i, i \in D'.
   move=> /(_ (D' `|` [fset j])%fset); apply.
-  - by move=> k; rewrite !in_fsetE => /orP [/sD|/eqP->] //; rewrite in_setE.
-  - by move=> p /sAnfcov [i D'i Anfip]; exists i => //; rewrite !in_fsetE D'i.
-  - by exists j; rewrite !in_fsetE orbC eq_refl.
+  - by move=> k; rewrite !inE => /orP [/sD|/eqP->] //; rewrite inE.
+  - by move=> p /sAnfcov [i D'i Anfip]; exists i => //; rewrite !inE D'i.
+  - by exists j; rewrite !inE orbC eq_refl.
 exists D' => /(_ sD) [p Ifp].
-have /Ifp := D'k; rewrite feAg; last by have /sD := D'k; rewrite in_setE.
+have /Ifp := D'k; rewrite feAg; last by have /sD := D'k; rewrite inE.
 by move=> [/sAnfcov [i D'i [_ nfip]] _]; have /Ifp := D'i.
 Qed.
 
@@ -2563,9 +2563,9 @@ rewrite propeqE; split => [T_filterT2|T_openT2] x y.
   move=> /asboolPn; rewrite -set0P => /negP; rewrite negbK => /eqP AIB_eq0.
   move: xA yB; rewrite !locallyE.
   move=> - [oA [[oA_open oAx] oAA]] [oB [[oB_open oBx] oBB]].
-  by exists (oA, oB); rewrite ?in_setE; split => //; apply: subsetI_eq0 AIB_eq0.
+  by exists (oA, oB); rewrite ?inE; split => //; apply: subsetI_eq0 AIB_eq0.
 apply: contrapTT => /eqP /T_openT2[[/=A B]].
-rewrite !in_setE => - [xA yB] [Aopen Bopen /eqP AIB_eq0].
+rewrite !inE => - [xA yB] [Aopen Bopen /eqP AIB_eq0].
 move=> /(_ A B (neigh_locally _) (neigh_locally _)).
 by rewrite -set0P => /(_ _ _)/negP; apply.
 Qed.
@@ -2918,12 +2918,12 @@ Lemma ball_hausdorff : hausdorff T =
   exists r : {posnum R} * {posnum R}, ball a r.1%:num `&` ball b r.2%:num == set0.
 Proof.
 rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]].
-  move=> A B; rewrite 2!in_setE => [[aA bB] [oA oB /eqP ABeq0]].
+  move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]].
   have /locallyP[_/posnumP[r] rA]: locally a A by apply: neigh_locally.
   have /locallyP[_/posnumP[s] rB]: locally b B by apply: neigh_locally.
   by exists (r, s) => /=; rewrite (subsetI_eq0 _ _ ABeq0).
 move=> r s /eqP brs_eq0; exists ((ball a r%:num)^°, (ball b s%:num)^°) => /=.
-  split; by rewrite in_setE; apply: locally_singleton; apply: locally_interior;
+  split; by rewrite inE; apply: locally_singleton; apply: locally_interior;
             apply/locallyP; apply: in_filter_from.
 split; do ?by apply: open_interior.
 by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset.