trying to control the unfolding of ub

- replace `case`s of `pselect` with `have`s of `pselect`
- replace expressions such as `(forall y, X y -> (x <= y)%O)`
  by `ub X` (resp. `lb`)
- avoid implicit unfolding of `ub`, `lb`, `down` by enforcing
  usage of `ubP`, `lbP`, `downP`
  + in particular, change the definition of supremum to
    `ub E `&` lb (ub E)`
- replace usage of `nonempty` by `!=set0`
- removed redundant `has_inP`, `has_supP`, `has_ubP`, `has_lbP`,
  `nonemptyPn`

theories/Rstruct.v

@@ -380,8 +380,8 @@ Section ssreal_struct_contd.
 
 Lemma is_upper_boundE (E : set R) x : is_upper_bound E x = ((ub E) x).
 Proof.
-apply/eq_forall=> y.
-by rewrite propeqE; split => h Ey; [apply/RleP/h|apply/RleP/h].
+rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h].
+by apply/ubP => y Ey; apply/RleP/h.
 Qed.
 
 Lemma boundE (E : set R) : bound E = has_ub E.
@@ -411,7 +411,7 @@ Lemma real_sup_adherent (E : set R) (eps : R) :
 Proof.
 move=> supE eps_gt0; set m := _ - eps; apply: contrapT=> mNsmall.
 have: (ub E) m.
-  move=> y Ey.
+  apply/ubP => y Ey.
   have /negP := mNsmall (ex_intro2 _ _ y Ey _).
   by rewrite -leNgt.
 have [_ /(_ m)] := real_sup_is_lub supE.

theories/altreals/distr.v

@@ -5,7 +5,7 @@
 
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
-Require Import xfinmap boolp ereal reals discrete.
+Require Import xfinmap boolp classical_sets ereal reals discrete.
 Require Import realseq realsum.
 
 Set Implicit Arguments.

theories/altreals/realseq.v

@@ -223,8 +223,8 @@ case: (ltnP n K); last first.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
 move=> un_S; rewrite ltxU; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_spaddr; first apply/ltr01.
-apply/sup_upper_bound; last by apply/map_f; rewrite mem_iota E.
-apply/has_supP; split; first by exists `|u 0%N|; rewrite /S E inE eqxx.
+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 lexU lexx.
@@ -540,13 +540,13 @@ Proof.
 move=> mn_u cv_ul; set S := (X in sup X); suff: ncvg u (sup S)%:E.
   by move/nlimE; move/nlimE: cv_ul => -> [->].
 elim/nbh_finW=> /= e gt0_e; have sS: has_sup S.
-  apply/has_supP; split; first exists (u 0%N).
+  split; first exists (u 0%N).
     by exists 0%N.
   exists l; apply/ubP => _ [n ->].
   by rewrite -lee_fin; apply/ncvg_homo_le.
 have /sup_adherent := sS => /(_ _ gt0_e) [r] [N ->] lt_uN.
 exists N => n le_Nn; rewrite !inE distrC ger0_norm ?subr_ge0.
-  by apply/sup_upper_bound => //; exists n.
+  by move/ubP : (sup_upper_bound sS) => -> //; exists n.
 by rewrite ltr_subl_addr -ltr_subl_addl (lt_le_trans lt_uN) ?mn_u.
 Qed.
 

theories/altreals/realsum.v

@@ -182,7 +182,7 @@ move=> supE; exists (sup E)%:E => //; first exact: lte_ninfty.
 elim/nbh_finW=>e /= gt0_e.
 case: (sup_adherent supE gt0_e)=> x [K ->] lt_uK.
 exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.
-  by apply/sup_upper_bound=> //; exists n.
+  by move/ubP: (sup_upper_bound supE); apply; exists n.
 rewrite ltr_subl_addr addrC -ltr_subl_addr.
 by rewrite (lt_le_trans lt_uK) //; apply/mono_u.
 Qed.
@@ -209,7 +209,7 @@ Implicit Type S : T -> R.
 Lemma summable_sup (S : T -> R) : summable S -> has_sup
   [set x | exists J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic.
 Proof.
-case/summableP=> M _ hbd; apply/has_supP; split.
+case/summableP=> M _ hbd; split.
   by exists 0, fset0; rewrite big_fset0.
 by exists M; apply/ubP=> y [J ->].
 Qed.
@@ -219,8 +219,8 @@ Lemma psum_sup S : psum S =
 Proof.
 rewrite /psum; case: ifPn => // /asboolPn h.
 rewrite sup_out //; set X := [set r | _]%classic => hs.
-apply: h; exists (sup X) => J; apply/sup_upper_bound => //.
-by exists J.
+apply: h; exists (sup X) => J.
+by move/ubP : (sup_upper_bound hs); apply; exists J.
 Qed.
 
 Lemma psum_sup_seq S : psum S =
@@ -316,8 +316,8 @@ Qed.
 Lemma gerfin_psum S (J : {fset T}) :
   summable S -> \sum_(j : J) `|S (val j)| <= psum S.
 Proof.
-move=> smS; rewrite /psum (asboolT smS); apply/sup_upper_bound.
-  by apply/summable_sup. by exists J.
+move=> smS; rewrite /psum (asboolT smS).
+by move/ubP : (sup_upper_bound (summable_sup smS)); apply; exists J.
 Qed.
 
 Lemma gerfinseq_psum S (r : seq T) :
@@ -352,8 +352,9 @@ Lemma max_sup {R : realType} x (E : set R) :
   (E `&` ub E)%classic x -> sup E = x.
 Proof.
 case=> /= xE xubE; have nzE: nonempty E by exists x.
-apply/eqP; rewrite eq_le sup_le_ub ?sup_upper_bound //.
-by apply/has_supP; split; exists x.
+apply/eqP; rewrite eq_le sup_le_ub //=.
+have : has_sup E by split; exists x.
+by move/sup_upper_bound/ubP; apply.
 Qed.
 
 (* -------------------------------------------------------------------- *)
@@ -395,9 +396,11 @@ Variable (S : T -> R).
 Lemma ger_big_psum r : uniq r -> summable S ->
   \sum_(x <- r) `|S x| <= psum S.
 Proof.
-move=> uq_r smS; rewrite /psum (asboolT smS) sup_upper_bound //.
-  by apply/summable_sup. exists [fset x in r].
-by rewrite (big_seq_fset (fun i => `|S i|)).
+move=> uq_r smS; rewrite /psum (asboolT smS).
+set E := (X in sup X).
+have : has_sup E by apply/summable_sup.
+move/sup_upper_bound/ubP; apply.
+by exists [fset x in r]; rewrite (big_seq_fset (fun i => `|S i|)).
 Qed.
 
 Lemma ger1_psum x : summable S -> `|S x| <= psum S.

theories/boolp.v

@@ -554,28 +554,35 @@ apply: (asbool_equiv_eqP existsp_asboolPn);
   by split=> -[x h]; exists x; apply/negP.
 Qed.
 
-Lemma existsp_Pn (T : Type) (P : T -> Prop) :
+Lemma existsNP (T : Type) (P : T -> Prop) :
   (exists x : T, ~ P x) <-> (~ forall x : T, P x).
 Proof.
 split => [[x Px h]|/asboolP]; [exact: Px|].
 by rewrite asbool_neg => /existsp_asboolPn.
 Qed.
 
-Lemma existsp_P (T : Type) (P : T -> Prop) :
+Lemma existsP (T : Type) (P : T -> Prop) :
   (exists x : T, P x) <-> (~ forall x : T, ~ P x).
 Proof.
 split => [[x Px h]|/asboolP]; [exact: (h x)|].
-by move/asboolP/existsp_Pn => [x /contrapT Px]; exists x.
+by move/asboolP/existsNP => [x /contrapT Px]; exists x.
 Qed.
 
-Lemma forallp_Pn (T : Type) (P : T -> Prop) :
+Lemma forallNP (T : Type) (P : T -> Prop) :
   (forall x : T, ~ P x) <-> (~ exists x : T, P x).
 Proof.
 split => [h [x Px]|/asboolP]; [exact: (h x)|].
 by rewrite asbool_neg => /forallp_asboolPn.
 Qed.
 
-Lemma imply_Pn (P Q : Prop) : (P /\ ~ Q) <-> ~ (P -> Q).
+Lemma forallP (T : Type) (P : T -> Prop) :
+  (forall x : T, P x) <-> (~ exists x : T, ~ P x).
+Proof.
+split => [h [x px]|]; [exact/px/h|move=> /forallNP h x].
+by move/contrapT : (h x).
+Qed.
+
+Lemma imply_classic (P Q : Prop) : (P /\ ~ Q) <-> ~ (P -> Q).
 Proof.
 split => [[p nq pq]|/asboolP]; [exact/nq/pq|].
 by rewrite asbool_neg => /imply_asboolPn.

theories/classical_sets.v

@@ -479,7 +479,7 @@ 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) := 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).
+  forall x, f x !=set0 /\ is_subset1 (f x).
 
 Definition xget {T : choiceType} x0 (P : set T) : T :=
   if pselect (exists x : T, `[<P x>]) isn't left exP then x0
@@ -519,7 +519,7 @@ Definition fun_of_rel {A} {B : choiceType} (f0 : A -> B) (f : A -> B -> Prop) :=
   fun x => xget (f0 x) (f x).
 
 Lemma fun_of_relP {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a :
-  nonempty (f a) ->  f a (fun_of_rel f0 f a).
+  f a !=set0 -> f a (fun_of_rel f0 f a).
 Proof. by move=> [b fab]; rewrite /fun_of_rel; apply: xgetI fab. Qed.
 
 Lemma fun_of_rel_uniq {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a :
@@ -695,18 +695,18 @@ suff Twtot : total_on tower R.
   have [R_S] := RS (lub (exist _ tower Twtot)); apply.
   by apply/Rantisym => //; apply/lub_ub/Succ/Lub.
 move=> s t Tws; elim: Tws t => {s} [A sATw ihA|s Tws ihs] t Twt.
-  case: (pselect (forall s, sval A s -> R s t)).
-    by move=> ?; left; apply: lub_lub.
-  move/asboolP; rewrite asbool_neg => /existsp_asboolPn [s /asboolP].
+  have [?|/asboolP] := pselect (forall s, sval A s -> R s t).
+    by left; apply: lub_lub.
+  rewrite asbool_neg => /existsp_asboolPn [s /asboolP].
   rewrite asbool_neg => /imply_asboolPn [As nRst]; right.
   by have /lub_ub := As; apply: Rtrans; have [] := ihA _ As _ Twt.
 suff /(_ _ Twt) [Rts|RSst] : forall r, tower r -> R r s \/ R (succ s) r.
     by right; apply: Rtrans Rts _; have [] := RS s.
   by left.
 move=> r; elim=> {r} [A sATw ihA|r Twr ihr].
-  case: (pselect (forall r, sval A r -> R r s)).
-    by move=> ?; left; apply: lub_lub.
-  move/asboolP; rewrite asbool_neg => /existsp_asboolPn [r /asboolP].
+  have [?|/asboolP] := pselect (forall r, sval A r -> R r s).
+    by left; apply: lub_lub.
+  rewrite asbool_neg => /existsp_asboolPn [r /asboolP].
   rewrite asbool_neg => /imply_asboolPn [Ar nRrs]; right.
   by have /lub_ub := Ar; apply: Rtrans; have /ihA [] := Ar.
 have [Rrs|RSsr] := ihr; last by right; apply: Rtrans RSsr _; have [] := RS r.
@@ -761,9 +761,9 @@ have Astot : total_on (sval A `|` [set s]) R.
   by apply: Rtrans Rts; apply: tub.
 exists (exist _ (sval A `|` [set s]) Astot); split; first by move=> ??; left.
 split=> [AeAs|[B Btot] sAB sBAs].
-  case: (pselect (sval A s)); first by move=> /tub Rst; apply/snet/Rantisym.
+  have [/tub Rst|] := (pselect (sval A s)); first exact/snet/Rantisym.
   by rewrite AeAs /=; apply; right.
-case: (pselect (B s)) => [Bs|nBs].
+have [Bs|nBs] := pselect (B s).
   by right; apply: exist_congr; rewrite predeqE => r; split=> [/sBAs|[/sAB|->]].
 left; case: A tub Astot sBAs sAB => A Atot /= tub Astot sBAs sAB.
 apply: exist_congr; rewrite predeqE => r; split=> [Br|/sAB] //.
@@ -821,43 +821,69 @@ have /Amax <- : R' A (lift t).
 by have [] := repr_liftE t.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Section ArchiBound.
-
+Section UpperLowerTheory.
+Import Order.TTheory.
 Variables (d : unit) (T : porderType d).
 Implicit Types E : set T.
 
 (* upper bound and lower bound sets. *)
-Definition ub E : set T := [set z | forall y, E y -> (y <= z)%O].
-Definition lb E : set T := [set z | forall y, E y -> (z <= y)%O].
+Definition ub E : set T := locked [set z | forall y, E y -> (y <= z)%O].
+Definition lb E : set T := locked [set z | forall y, E y -> (z <= y)%O].
+
+Lemma ubP E x : (forall y, E y -> (y <= x)%O) <-> ub E x.
+Proof. by rewrite /ub; unlock. Qed.
+
+Lemma lbP E x : (forall y, E y -> (x <= y)%O) <-> lb E x.
+Proof. by rewrite /lb; unlock. Qed.
+
+Lemma ub_set1 x y : ub [set x] y = (x <= y)%O.
+Proof.
+by rewrite propeqE; split => [/ubP/(_ x erefl)//|xy]; apply/ubP => z ->.
+Qed.
+
+Lemma lb_ub_set1 x y : lb (ub [set x]) y -> (y <= x)%O.
+Proof. by move/lbP => /(_ x); apply; rewrite ub_set1. Qed.
+
+Lemma lb_ub_refl x : lb (ub [set x]) x.
+Proof. by apply/lbP => y /ubP; apply. Qed.
+
+Lemma ub_lb_ub E x y : ub E y -> lb (ub E) x -> (x <= y)%O.
+Proof. by move=> Ey /lbP; apply. Qed.
 
 (* down set (i.e., generated order ideal) *)
 (* i.e. down E := { x | exists y, y \in E /\ x <= y} *)
-Definition down E : set T := [set x | exists y, E y /\ (x <= y)%O].
+Definition down E : set T := locked [set x | exists y, E y /\ (x <= y)%O].
 
 (* Real set supremum and infimum existence condition. *)
-Definition has_ub  E := nonempty (ub E).
-Definition has_sup E := nonempty E /\ has_ub E.
-Definition has_lb  E := nonempty (lb E).
-Definition has_inf E := nonempty E /\ has_lb E.
+Definition has_ub  E := ub E !=set0.
+Definition has_sup E := E !=set0 /\ has_ub E.
+Definition has_lb  E := lb E !=set0.
+Definition has_inf E := E !=set0 /\ has_lb E.
+
+Lemma has_ub_set1 x : has_ub [set x]. Proof. by exists x; rewrite ub_set1. Qed.
+
+Lemma downP E x : (exists2 y, E y & (x <= y)%O) <-> down E x.
+Proof.
+by rewrite /down; unlock; split => [[y Ey xy]|[y [Ey xy]]]; [exists y| exists y].
+Qed.
 
-Definition supremums E := [set x | ub E x /\ (forall y, ub E y -> (x <= y)%O)].
+Definition supremums E := ub E `&` lb (ub E).
 
 Lemma supremums_set1 x : supremums [set x] = [set x].
 Proof.
-rewrite predeqE => y; split => [[]/(_ x erefl) xy /(_ x) yx|->{y}].
-  by apply/eqP; rewrite Order.POrderTheory.eq_le xy andbT yx // => z ->.
-by split=> [y -> //|y]; exact.
+rewrite /supremums predeqE => y; split => [[]|].
+  rewrite ub_set1 => xy /lb_ub_set1 => yx.
+  by apply/eqP; rewrite eq_le xy andbT yx // => z ->.
+by move=> xy; split; [rewrite -xy ub_set1 | rewrite -xy; apply: lb_ub_refl].
 Qed.
 
 Lemma is_subset1_supremums E : is_subset1 (supremums E).
 Proof.
-move=> x y [Ex xE] [Ey yE].
-move: {xE Ey}(xE _ Ey) {yE Ex}(yE _ Ex) => xy yx.
-by apply/eqP; rewrite Order.POrderTheory.eq_le xy.
+move=> x y [Ex xE] [Ey yE]; have yx := ub_lb_ub Ex yE. have xy := ub_lb_ub Ey xE.
+by apply/eqP; rewrite eq_le xy.
 Qed.
 
 Definition supremum (x0 : T) E :=
   if pselect (E !=set0) then xget x0 (supremums E) else x0.
 
-End ArchiBound.
+End UpperLowerTheory.

theories/derive.v

@@ -1312,7 +1312,7 @@ Lemma EVT_max (R : realType) (f : R^o -> R^o) (a b : R^o) :
 Proof.
 move=> leab fcont; set imf := [set t | (f @` [set x | x \in `[a, b]]) t].
 have imf_sup : has_sup imf.
-  apply/has_supP; split.
+  split.
     by exists (f a) => //; rewrite /imf; 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.
@@ -1321,13 +1321,13 @@ have imf_sup : has_sup imf.
   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.
-  by rewrite fceqsup; apply: sup_upper_bound=> //; apply: imageP.
+  move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup.
+  by move/ubP : (sup_upper_bound imf_sup); apply; exact: 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 apply/imageP.
+  apply/eqP; rewrite eq_le supleft andbT.
+  by move/ubP : (sup_upper_bound imf_sup); apply; exact: 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.
@@ -1531,8 +1531,8 @@ have itvW : {subset `[x, y] <= `[a, b]} by apply/subitvP; rewrite /= leyb leax.
 have fdrv z : z \in `]x, y[ -> is_derive (z : R^o) 1 f (f^`()z).
   rewrite inE => /andP [/ltW lexz /ltW lezy].
   apply: DeriveDef; last by rewrite derive1E.
-  apply: fdrvbl; rewrite inE; apply/andP; split; first exact: le_trans lexz.
-  exact: le_trans leyb.
+  apply: fdrvbl; rewrite inE; apply/andP.
+  by split; [exact: le_trans lexz | exact: le_trans leyb].
 have [] := @MVT _ f (f^`()) x y lexy fdrv.
   by move=> ? /itvW /fdrvbl /derivable1_diffP /differentiable_continuous.
 move=> t /itvW /dfle0 dft dftxy; rewrite -oppr_le0 opprB dftxy.