From 8dd160b6ba5ac2b2465c76841aeed7a04881d226 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 12 May 2020 00:05:09 +0900 Subject: [PATCH 1/6] generalize ub, lb, etc. from `reals.v` - replace `pred` with `set` in `reals.v` and propagate - replace `-' E` by `-%R @' E` --- theories/Rstruct.v | 27 ++-- theories/altreals/distr.v | 4 +- theories/altreals/realseq.v | 13 +- theories/altreals/realsum.v | 135 ++++++++-------- theories/boolp.v | 23 +++ theories/derive.v | 14 +- theories/normedtype.v | 39 ++--- theories/reals.v | 307 ++++++++++++++++++------------------ 8 files changed, 297 insertions(+), 265 deletions(-) diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 9b1cd0746a..0631e0a069 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -374,44 +374,45 @@ Canonical R_rcfType := RcfType R Rreal_closed_axiom. End ssreal_struct. Local Open Scope ring_scope. -Require Import reals boolp. +Require Import reals boolp classical_sets. Section ssreal_struct_contd. -Lemma is_upper_boundE (E : pred R) x : is_upper_bound E x = (x \in ub E). +Lemma is_upper_boundE (E : set R) x : is_upper_bound E x = ((ub E) x). Proof. -rewrite /is_upper_bound inE forallbE asboolE /=; apply/eq_forall=> y. -by rewrite -(reflect_eq implyP) (reflect_eq (RleP _ _)). +apply/eq_forall=> y. +by rewrite propeqE; split => h Ey; [apply/RleP/h|apply/RleP/h]. Qed. -Lemma boundE (E : pred R) : bound E = has_ub E. +Lemma boundE (E : set R) : bound E = has_ub E. Proof. by apply/eq_exists=> x; rewrite is_upper_boundE. Qed. -Lemma completeness' (E : pred R) : has_sup E -> {m : R | is_lub E m}. +Lemma completeness' (E : set R) : has_sup E -> {m : R | is_lub E m}. Proof. by move=> [eE bE]; rewrite -boundE in bE; apply: completeness. Qed. -Definition real_sup (E : pred R) : R := +Definition real_sup (E : set R) : R := if pselect (has_sup E) isn't left hsE then 0 else projT1 (completeness' hsE). -Lemma real_sup_is_lub (E : pred R) : has_sup E -> is_lub E (real_sup E). +Lemma real_sup_is_lub (E : set R) : has_sup E -> is_lub E (real_sup E). Proof. by move=> hsE; rewrite /real_sup; case: pselect=> // ?; case: completeness'. Qed. -Lemma real_sup_ub (E : pred R) : has_sup E -> real_sup E \in ub E. +Lemma real_sup_ub (E : set R) : has_sup E -> (ub E) (real_sup E). Proof. by move=> /real_sup_is_lub []; rewrite is_upper_boundE. Qed. -Lemma real_sup_out (E : pred R) : ~ has_sup E -> real_sup E = 0. +Lemma real_sup_out (E : set R) : ~ has_sup E -> real_sup E = 0. Proof. by move=> nosup; rewrite /real_sup; case: pselect. Qed. (* :TODO: rewrite like this using (a fork of?) Coquelicot *) (* Lemma real_sup_adherent (E : pred R) : real_sup E \in closure E. *) -Lemma real_sup_adherent (E : pred R) (eps : R) : +Lemma real_sup_adherent (E : set R) (eps : R) : has_sup E -> 0 < eps -> exists2 e : R, E e & (real_sup E - eps) < e. Proof. move=> supE eps_gt0; set m := _ - eps; apply: contrapT=> mNsmall. -have: m \in ub E. - apply/ubP=> y Ey; have /negP := mNsmall (ex_intro2 _ _ y Ey _). +have: (ub E) m. + move=> y Ey. + have /negP := mNsmall (ex_intro2 _ _ y Ey _). by rewrite -leNgt. have [_ /(_ m)] := real_sup_is_lub supE. rewrite is_upper_boundE => m_big /m_big /RleP. diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v index 2efb45db6f..c7b928cf1e 100644 --- a/theories/altreals/distr.v +++ b/theories/altreals/distr.v @@ -157,8 +157,8 @@ Qed. Local Lemma isd3 : psum mu <= 1. Proof. rewrite psumE; [apply/isd1 | apply/isd2 | apply/sup_le_ub]. - by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. -apply/ubP=> y /imsetbP[x ->]; rewrite big_fset_seq /=. + by exists 0, fset0; rewrite big_fset0. +apply/ubP=> y [x ->]; rewrite big_fset_seq /=. by case: isd => _; apply; case: x => x /= /canonical_uniq. Qed. diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v index 9805b15c75..460fd68fb0 100644 --- a/theories/altreals/realseq.v +++ b/theories/altreals/realseq.v @@ -7,6 +7,7 @@ From mathcomp Require Import all_ssreflect all_algebra. Require Import mathcomp.bigenough.bigenough. Require Import xfinmap boolp ereal reals discrete. +Require Import classical_sets. Set Implicit Arguments. Unset Strict Implicit. @@ -213,7 +214,7 @@ Proof. by move=> le_uv; apply/(@ncvg_le_from 0). Qed. 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 [pred x in S]; pose e := Num.max (`|x| + 1) (M + 1). +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 ltxU ltr_paddl. case: (ltnP n K); last first. move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1. @@ -534,18 +535,18 @@ Qed. Lemma nlim_sup (u : nat -> R) l : (forall n m, (n <= m)%N -> u n <= u m) -> ncvg u l%:E - -> sup [pred r | `[exists n, r == u n]] = l. + -> sup [set r | exists n, r = u n] = l. 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). - by apply/imsetbP; exists 0%N. - exists l; apply/ubP => _ /imsetbP[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 /imsetbP] [N ->] lt_uN. +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 => //; apply/imsetbP; exists n. + by apply/sup_upper_bound => //; exists n. by rewrite ltr_subl_addr -ltr_subl_addl (lt_le_trans lt_uN) ?mn_u. Qed. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 5836c3c9bd..904711d97c 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -6,6 +6,7 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import all_ssreflect all_algebra. Require Import xfinmap boolp ereal reals discrete realseq. +Require Import classical_sets. Set Implicit Arguments. Unset Strict Implicit. @@ -124,7 +125,7 @@ Qed. Definition psum f : R := (* We need some ticked `image` operator *) - let S := [pred x | `[exists J : {fset T}, x == \sum_(x : J) `|f (val x)|]] in + let S := [set x | exists J : {fset T}, x = \sum_(x : J) `|f (val x)| ]%classic in if `[] then sup S else 0. Definition sum f : R := psum (fpos f) - psum (fneg f). @@ -171,17 +172,17 @@ Lemma ncvg_mono (u : nat -> R) : (forall x y, (x <= y)%N -> u x <= u y) -> exists2 l, (-oo < l)%E & ncvg u l. Proof. -move=> mono_u; pose E := [pred x | `[exists n, x == u n]]. -have nzE: nonempty E by exists (u 0%N); apply/imsetbP; exists 0%N. -case/boolP: `[< has_sup E >] => /asboolP; last first. +move=> mono_u; pose E := [set x | exists n, x = u n]%classic. +have nzE: nonempty E by exists (u 0%N); exists 0%N. +case: (pselect (has_sup E)); last first. move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=. - case/(_ M): h=> x /imsetbP[K -> lt_MuK]; exists K=> n le_Kn; rewrite inE. + case/(_ M): h=> x [K -> lt_MuK]; exists K=> n le_Kn; rewrite inE. by apply/(lt_le_trans lt_MuK)/mono_u. move=> supE; exists (sup E)%:E => //; first exact: lte_ninfty. elim/nbh_finW=>e /= gt0_e. -case: (sup_adherent supE gt0_e)=> x /imsetbP[K ->] lt_uK. +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/imsetbP=> //; exists n. + by apply/sup_upper_bound=> //; exists n. rewrite ltr_subl_addr addrC -ltr_subl_addr. by rewrite (lt_le_trans lt_uK) //; apply/mono_u. Qed. @@ -206,31 +207,31 @@ Context {R : realType} (T : choiceType). Implicit Type S : T -> R. Lemma summable_sup (S : T -> R) : summable S -> has_sup - [pred x | `[exists J : {fset T}, x == \sum_(j : J) `|S (val j)|]]. + [set x | exists J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic. Proof. case/summableP=> M _ hbd; apply/has_supP; split. - by exists 0; apply/existsbP; exists fset0; rewrite big_fset0. -by exists M; apply/ubP=> y /existsbP[J /eqP->]. + by exists 0, fset0; rewrite big_fset0. +by exists M; apply/ubP=> y [J ->]. Qed. Lemma psum_sup S : psum S = - sup [pred x | `[exists J : {fset T}, x == \sum_(x : J) `|S (val x)|]]. + sup [set x | exists J : {fset T}, x = \sum_(x : J) `|S (val x)|]%classic. Proof. rewrite /psum; case: ifPn => // /asboolPn h. -rewrite sup_out //; set X := [pred r | _] => hs. +rewrite sup_out //; set X := [set r | _]%classic => hs. apply: h; exists (sup X) => J; apply/sup_upper_bound => //. -by apply/imsetbP; exists J. +by exists J. Qed. Lemma psum_sup_seq S : psum S = - sup [pred x | `[]]. + sup [set x | exists2 J : seq T, + uniq J & x = \sum_(x <- J) `|S x| ]%classic. Proof. -rewrite psum_sup; apply/eq_sup => x; rewrite !inE; apply/imsetbP/idP. - case=> J ->; apply/asboolP; exists (enum_fset J). +rewrite psum_sup; congr sup; rewrite predeqE => x; split. + case=> J ->; exists (enum_fset J). by case: J => /= J /canonical_uniq. by rewrite (big_fset_seq \`|_|) /=. -case/asboolP=> J uqJ /eqP->; exists [fset x in J]. +case=> J uqJ ->; exists [fset x in J]. by rewrite (big_seq_fset \`|_|). Qed. @@ -247,17 +248,18 @@ Lemma eq_summableb (S1 S2 : T -> R) : Proof. by move=> eq_12; apply/asboolP/asboolP; apply/eq_summable. Qed. Lemma eq_ppsum (F1 F2 : {fset T} -> R) : F1 =1 F2 -> - sup [pred x | `[exists J, x == F1 J]] = sup [pred x | `[exists J, x == F2 J]]. + (sup [set x | exists J, x = F1 J] = sup [set x | exists J, x = F2 J])%classic. Proof. -move=> eq_12; apply/eq_sup=> x; rewrite !inE. -by apply/existsbP/existsbP=> -[J /eqP->]; exists J; apply/eqP. +move=> eq_12; congr sup; rewrite predeqE => x. +by split=> -[J ->]; exists J. Qed. Lemma eq_psum (F1 F2 : T -> R) : F1 =1 F2 -> psum F1 = psum F2. Proof. move=> eq_12; rewrite /psum (eq_summableb eq_12). -case: `[< summable F1 >] => //; apply/eq_sup. -move=> x; apply/imsetbP/imsetbP=> -[J ->]; exists J; +case: `[< summable F1 >] => //. +congr sup. +rewrite predeqE => x; split=> -[J ->]; exists J; by apply/eq_bigr=> /= K _; rewrite eq_12. Qed. @@ -281,9 +283,9 @@ Proof. move=> le_F smF2; have smF1: summable F1 by apply/(le_summable le_F). rewrite /psum (asboolT smF1) (asboolT smF2); apply/le_sup; first last. + by apply/summable_sup. -+ by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. -move=> x /imsetbP[J ->]; apply/downP; exists (\sum_(j : J) `|F2 (val j)|). - by apply/imsetbP; exists J. ++ by exists 0, fset0; rewrite big_fset0. +move=> x [J ->]; apply/downP; exists (\sum_(j : J) `|F2 (val j)|). + by exists J. apply/ler_sum=> /= j _; case/andP: (le_F (val j)) => h1 h2. by rewrite !ger0_norm // (le_trans h1 h2). Qed. @@ -292,14 +294,14 @@ Lemma psum_out S : ~ summable S -> psum S = 0. Proof. by move/asboolPn/negbTE=> smN; rewrite /psum smN. Qed. Lemma psumE S : (forall x, 0 <= S x) -> summable S -> psum S = - sup [pred x | `[exists J : {fset T}, x == \sum_(j : J) S (val j)]]. + sup [set x | exists J : {fset T}, x = \sum_(j : J) S (val j)]%classic. Proof. move=> gt0_S smS; rewrite /psum (asboolT smS); apply/eq_ppsum=> /=. by move=> J; apply/eq_bigr=> j _; rewrite ger0_norm. Qed. Lemma psum_absE S : summable S -> psum S = - sup [pred x | `[exists J : {fset T}, x == \sum_(j : J) `|S (val j)|]]. + sup [set x | exists J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic. Proof. by move=> smS; rewrite /psum (asboolT smS). Qed. Lemma summable_seqP S : @@ -315,7 +317,7 @@ 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 apply/imsetbP; exists J. + by apply/summable_sup. by exists J. Qed. Lemma gerfinseq_psum S (r : seq T) : @@ -332,7 +334,7 @@ move=> le_z; have: summable S; first (apply/summable_seqP; exists z). + by apply/(le_trans _ (le_z [::] _)) => //; rewrite big_nil. + by move=> J uqJ; apply/le_z. move/summable_sup=> [neS hsS]; rewrite psum_sup. -apply/sup_le_ub => //; apply/ubP=> r /imsetbP [J ->]. +apply/sup_le_ub => //; apply/ubP=> r [J ->]. by rewrite (big_fset_seq \`|_|) le_z /=; case: J => J /= /canonical_uniq. Qed. @@ -346,10 +348,10 @@ Qed. End SumTh. (* -------------------------------------------------------------------- *) -Lemma max_sup {R : realType} x (E : pred R) : - x \in [predI E & ub E] -> sup E = x. +Lemma max_sup {R : realType} x (E : set R) : + (E `&` ub E)%classic x -> sup E = x. Proof. -case/andP=> /= xE xubE; have nzE: nonempty E by exists x. +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. Qed. @@ -370,9 +372,8 @@ Lemma psum_fin (f : I -> R) : psum f = \sum_i `|f i|. Proof. (* FIXME *) pose S := \sum_(i : [fset i | i : I]) `|f (val i)|. rewrite /psum (asboolT (summable_fin f)) (@max_sup _ S). - rewrite inE/=; apply/andP; split; first apply/imsetbP. - by exists [fset i | i : I]%fset. - apply/ubP=> y /imsetbP[J ->]; apply/(big_fset_subset (F := \`|_|)). + rewrite /=; split; first by exists [fset i | i : I]%fset. + apply/ubP=> y [J ->]; apply/(big_fset_subset (F := \`|_|)). by move=> i; rewrite normr_ge0. by move=> j jJ; apply/in_imfset. rewrite /S -(big_map val xpredT \`|f|); apply/perm_big. @@ -395,7 +396,7 @@ 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. apply/imsetbP; exists [fset x in r]. + by apply/summable_sup. exists [fset x in r]. by rewrite (big_seq_fset (fun i => `|S i|)). Qed. @@ -464,7 +465,7 @@ apply/eqP; case: (x =P _) => // /eqP /lt_total /orP[]; last first. move=> lt_xS; pose e := psum S - x. have ge0_e: 0 < e by rewrite subr_gt0. case: (sup_adherent (summable_sup smS) ge0_e) => y. -case/imsetbP=> /= J ->; rewrite /e /psum (asboolT smS). +case=> /= J ->; rewrite /e /psum (asboolT smS). rewrite opprB addrCA subrr addr0 => lt_xSJ. pose k := \max_(j : J) (val j); have lt_x_uSk: x < u k.+1. apply/(lt_le_trans lt_xSJ); rewrite /u big_ord_mkfset. @@ -673,8 +674,8 @@ move=> leS; have ge0_d: 0 <= d. by apply/(le_trans _ (leS [::] _)); rewrite // big_nil. have smS: summable S by apply/summable_seqP; exists d. split=> //; rewrite /psum (asboolT smS); apply/sup_le_ub. - by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. -apply/ubP=> _ /imsetbP[J ->]; rewrite (big_fset_seq \`|_|) /=. + by exists 0, fset0; rewrite big_fset0. +apply/ubP=> _ [J ->]; rewrite (big_fset_seq \`|_|) /=. by apply/leS; case: J => J /= /canonical_uniq. Qed. @@ -705,11 +706,11 @@ Implicit Type S : T -> R. Lemma psum0 : psum (fun _ : T => 0) = 0 :> R. Proof. rewrite /psum asboolT; first by apply/summable0. -set S := [pred x | _]; suff: S =1 (pred1 0). - by move/eq_sup => ->; rewrite sup1. -move=> x; rewrite {}/S inE; apply/idP/idP => /=. - by case/existsbP=> J /eqP-> /=; rewrite big1 // normr0. -by move=> /eqP->; apply/existsbP; exists fset0; rewrite big_fset0. +set S := [set x | _]%classic; suff: S = (set1 0). + by move => ->; rewrite sup1. +rewrite predeqE => x; split. + by case=> J -> /=; rewrite big1 // normr0. +by move=> ->; exists fset0; rewrite big_fset0. Qed. (* -------------------------------------------------------------------- *) @@ -738,11 +739,11 @@ Proof. rewrite /psum; do 2! case: ifPn => //; first last. + by move/asboolP/summable_abs/asboolP=> ->. + by move/asboolPn/summable_abs/asboolPn=> /negbTE->. -move=> _ _; apply/eq_sup=> x; rewrite !inE; apply/idP/idP. - case/existsbP=> J /eqP->; apply/existsbP; exists J. - by apply/eqP/eq_bigr=> /= j _; rewrite normr_id. -case/existsbP=> J /eqP->; apply/existsbP; exists J. -by apply/eqP/eq_bigr=> /= j _; rewrite normr_id. +move=> _ _; congr sup; rewrite predeqE => x; split. + case=> J ->; exists J. + by under eq_bigr do rewrite normr_id. +case=> J ->; exists J. +by under [in RHS]eq_bigr do rewrite normr_id. Qed. (* -------------------------------------------------------------------- *) @@ -796,17 +797,17 @@ move=> ge0_S1 ge0_S2 smS1 smS2; have smD := summableD smS1 smS2. have ge0D: forall x, 0 <= S1 x + S2 x by move=> x; rewrite addr_ge0. rewrite !psumE // (rwP eqP) eq_le -(rwP andP); split. apply/sup_le_ub. - + by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. - apply/ubP=> _ /imsetbP[J ->]; rewrite big_split /=. + + by exists 0, fset0; rewrite big_fset0. + apply/ubP=> _ [J ->]; rewrite big_split /=. apply/ler_add; rewrite -psumE 1?(le_trans _ (gerfin_psum J _)) //. + by apply/ler_sum=> j _ /=; apply/ler_norm. + by apply/ler_sum=> j _ /=; apply/ler_norm. rewrite -ler_subr_addr; apply/sup_le_ub. -+ by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. -apply/ubP=> _ /imsetbP[J1 ->]; rewrite ler_subr_addr addrC. ++ by exists 0, fset0; rewrite big_fset0. +apply/ubP=> _ [J1 ->]; rewrite ler_subr_addr addrC. rewrite -ler_subr_addr; apply/sup_le_ub. -+ by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. -apply/ubP=> _ /imsetbP[J2 ->]; rewrite ler_subr_addr addrC. ++ by exists 0, fset0; rewrite big_fset0. +apply/ubP=> _ [J2 ->]; rewrite ler_subr_addr addrC. pose J := J1 `|` J2; rewrite -psumE ?(le_trans _ (gerfin_psum J _)) //. pose D := \sum_(j : J) (S1 (val j) + S2 (val j)). apply/(@le_trans _ _ D); last by apply/ler_sum=> i _; apply/ler_norm. @@ -832,14 +833,14 @@ case/asboolP: (summable S) => [smS|NsmS]; last first. have smZ := summableZ c smS; rewrite (rwP eqP) eq_le. apply/andP; split; first rewrite {1}/psum asboolT //. apply/sup_le_ub. - + by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. - apply/ubP=> _ /imsetbP[J ->]; rewrite -ler_pdivr_mull //. + + by exists 0, fset0; rewrite big_fset0. + apply/ubP=> _ [J ->]; rewrite -ler_pdivr_mull //. rewrite mulr_sumr (le_trans _ (gerfin_psum J _)) //. apply/ler_sum=> /= j _; rewrite normrM. by rewrite gtr0_norm // mulKf ?gt_eqF. rewrite -ler_pdivl_mull // {1}/psum asboolT //; apply/sup_le_ub. -+ by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0. -apply/ubP=> _ /imsetbP[J ->]; rewrite ler_pdivl_mull //. ++ by exists 0, fset0; rewrite big_fset0. +apply/ubP=> _ [J ->]; rewrite ler_pdivl_mull //. rewrite mulr_sumr; apply/(le_trans _ (gerfin_psum J _))=> //. by apply/ler_sum=> /= j _; rewrite normrM (gtr0_norm gt0_c). Qed. @@ -915,8 +916,8 @@ Lemma reindex_psum_onto h' : -> (forall i, h i \in P -> h' (h i) = Some i) -> psum S = psum (fun x : U => S (h x)). Proof. -move=> PS hO hP; rewrite !psum_sup_seq; apply/eq_sup=> x. -rewrite !inE; apply/asboolP/asboolP=> -[J uqJ /eqP->] {x}; last first. +move=> PS hO hP; rewrite !psum_sup_seq; congr sup; rewrite predeqE => x. +split=> -[J uqJ ->] {x}; last first. exists [seq h j | j <- J & S (h j) != 0]. rewrite map_inj_in_uniq ?filter_uniq // => y1 y2. rewrite !mem_filter => /andP[nz_S1 _] /andP[nz_S2 _]. @@ -934,7 +935,7 @@ have uqpJ: uniq (pmap h' [seq j | j <- J & S j != 0]). exists (pmap h' [seq j | j <- J & S j != 0]) => //. apply/eqP; rewrite -(big_map h predT \`|S|) (bigID [pred j | S j == 0]) /=. rewrite big1 ?add0r => [i /eqP->|]; first by rewrite normr0. -rewrite -big_filter; apply/perm_big/uniq_perm_eq. +rewrite -big_filter; apply/eqP; apply/perm_big/uniq_perm_eq. + by rewrite filter_uniq. + rewrite map_inj_in_uniq // !map_id => y1 y2 h1 h2. move/(congr1 h'); rewrite !hP ?PS //; last by case. @@ -1093,10 +1094,10 @@ Section SupInterchange. Context {R : realType} {T U : Type}. Lemma interchange_sup (S : T -> U -> R) : - (forall x, has_sup [pred r | `[exists y, r == S x y]]) - -> has_sup [pred r | `[exists x, r == sup [pred r | `[exists y, r == S x y]]]] - -> sup [pred r | `[exists x, r == sup [pred r | `[exists y, r == S x y]]]] - = sup [pred r | `[exists y, r == sup [pred r | `[exists x, r == S x y]]]]. + (forall x, has_sup [set r | exists y, r = S x y]) + -> has_sup [set r | exists x, r = sup [set r | exists y, r = S x y]] + -> sup [set r | exists x, r = sup [set r | exists y, r = S x y]] + = sup [set r | exists y, r == sup [set r | exists x, r = S x y]]. Proof using Type. Admitted. End SupInterchange. diff --git a/theories/boolp.v b/theories/boolp.v index 4810190214..d9c3200e8d 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -554,6 +554,29 @@ apply: (asbool_equiv_eqP existsp_asboolPn); by split=> -[x h]; exists x; apply/negP. Qed. +Lemma existsp_Pn (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 forallp_Pn (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). +Proof. +split => [[p nq pq]|/asboolP]; [exact/nq/pq|]. +by rewrite asbool_neg => /imply_asboolPn. +Qed. + +Lemma orC (P Q : Prop) : (P \/ Q) = (Q \/ P). +Proof. rewrite propeqE; tauto. Qed. + (* -------------------------------------------------------------------- *) Definition xchooseb {T : choiceType} (P : pred T) (h : `[exists x, P x]) := xchoose (existsbP P h). diff --git a/theories/derive.v b/theories/derive.v index 839dbcf7e3..d2a276b39e 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1310,24 +1310,24 @@ Lemma EVT_max (R : realType) (f : R^o -> R^o) (a b : R^o) : a <= b -> {in `[a, b], continuous f} -> exists2 c, c \in `[a, b] & forall t, t \in `[a, b] -> f t <= f c. Proof. -move=> leab fcont; set imf := [pred t | t \in f @` [set x | x \in `[a, b]]]. +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. - by exists (f a); rewrite !inE; apply/imageP; rewrite inE/= lexx. + 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. by move=> ?; rewrite inE => /fcont. - exists (M + 1); apply/ubP => y; rewrite !inE => /imfltM yleM. + exists (M + 1); apply/ubP => y /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. - by rewrite fceqsup; apply: sup_upper_bound=> //; rewrite !inE; apply: imageP. + by rewrite fceqsup; apply: sup_upper_bound=> //; 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/imageP. + by 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. @@ -1336,9 +1336,9 @@ 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 => /invf_continuous. -have : exists2 y, y \in imf & sup imf - k^-1 < y. +have : exists2 y, imf y & sup imf - k^-1 < y. by apply: sup_adherent => //; rewrite invr_gt0. -move=> [y]; rewrite !inE => -[t tab <-] {y}. +move=> [y] -[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//. diff --git a/theories/normedtype.v b/theories/normedtype.v index dbcd9c23bb..f6350da1b0 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2393,28 +2393,31 @@ Arguments cvg_distW {_ _ F FF}. Lemma R_complete (R : realType) (F : set (set R^o)) : ProperFilter F -> cauchy F -> cvg F. Proof. move=> FF F_cauchy; apply/cvg_ex. -pose D := \bigcap_(A in F) (down (mem A)). +pose D := \bigcap_(A in F) (down A). have /cauchyP /(_ 1) [//|x0 x01] := F_cauchy. -have D_has_sup : has_sup (mem D); first split. -- exists (x0 - 1); rewrite inE => A FA. - apply/existsbP; near F => x; first exists x. - 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. +have D_has_sup : has_sup D; first split. +- exists (x0 - 1) => A FA. + near F => x. + exists x. + split. + by near: x. + by rewrite ler_distW 1?distrC 1?ltW ?andbT //; near: x. +- exists (x0 + 1) => x. + move=> /(_ _ x01) [y []]. rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltW]. by move=> /(le_trans _) yx01 _ /yx01. -exists (sup (mem D)). +exists (sup 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 inE. - move=> /(_ (ball_ (fun x => `| x |) x eps%:num) _) /existsbP []. + move=> y. + move=> /(_ (ball_ (fun x => `| x |) x eps%:num) _) []. by near: x; apply: nearP_dep; apply: F_cauchy. - move=> z /andP[]; rewrite inE /ball_ ltr_distl ltr_subl_addr. + move=> z []; rewrite /ball_ ltr_distl ltr_subl_addr. by move=> /andP [/ltW /(le_trans _) le_xeps _ /le_xeps]. -rewrite inE /D /= => A FA; near F => y. -apply/existsbP; exists y; apply/andP; split. - by rewrite inE; near: y. +rewrite /D /= => A FA; near F => y. +exists y; split. + by 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. @@ -2589,7 +2592,7 @@ 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 inE. -have xub_Altx : x \in ub Altx. +have xub_Altx : (ub Altx) x. by apply/ubP => ?; rewrite inE => - [_ /ltW]. have Altxsup : has_sup Altx by apply/has_supP; split=> //; exists x. set z := sup Altx. @@ -2719,14 +2722,14 @@ rewrite le_eqVlt => /orP [/eqP<- _|ltfav]. by exists a => //; rewrite inE/= lexx leab. rewrite le_eqVlt => /orP [/eqP->|ltvfb]. by exists b => //; rewrite inE/= lexx leab. -set A := [pred c | (c <= b) && (f c <= v)]. +set A := [set c | (c <= b) && (f c <= v)]. have An0 : reals.nonempty A by exists a; apply/andP; split=> //; apply: ltW. have supA : has_sup A. by apply/has_supP; split=> //; exists b; apply/ubP => ? /andP []. have supAab : sup A \in `[a, b]. rewrite inE; apply/andP; split; last first. by apply: sup_le_ub => //; apply/ubP => ? /andP []. - by apply: sup_upper_bound => //; rewrite inE leab andTb ltW. + by apply: sup_upper_bound => //; rewrite /A leab andTb ltW. exists (sup A) => //; have lefsupv : f (sup A) <= v. rewrite leNgt; apply/negP => ltvfsup. have vltfsup : 0 < f (sup A) - v by rewrite subr_gt0. @@ -2756,7 +2759,7 @@ rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t. by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltW. move=> t /andP [ltsupt /= letb]; rewrite ltNge; apply/negP => leftv. move: ltsupt => /=; rewrite ltNge => /negP; apply; apply: sup_upper_bound => //. -by rewrite inE leftv letb. +by rewrite /A leftv letb. Grab Existential Variables. all: end_near. Qed. (** Local properties in [R] *) diff --git a/theories/reals.v b/theories/reals.v index f190e298d7..0d57811509 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -9,7 +9,7 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import all_ssreflect all_algebra. -(* ------- *) Require Import boolp ereal. +(* ------- *) Require Import boolp ereal classical_sets. Require Import Setoid. @@ -25,32 +25,33 @@ Import Order.TTheory Order.Syntax GRing.Theory Num.Theory. Delimit Scope real_scope with real. Local Open Scope ring_scope. +Local Open Scope classical_set_scope. (* -------------------------------------------------------------------- *) Section ArchiBound. -Variable (R : archiFieldType). +Variables (d : unit) (R : porderType d). -(* Real set non-emptyness. *) -Definition nonempty (E : pred R) := - exists x : R, x \in E. +(* set non-emptyness. *) +Definition nonempty (E : set R) := + exists x : R, E x. -(* Real upper bound and lower bound sets. *) -Definition ub (E : pred R) : pred R := - [pred z | `[forall y, (y \in E) ==> (y <= z)]]. -Definition lb (E : pred R) : pred R := - [pred z | `[forall y, (y \in E) ==> (z <= y)]]. +(* upper bound and lower bound sets. *) +Definition ub (E : set R) : set R := + [set z | forall y, E y -> (y <= z)%O]. +Definition lb (E : set R) : set R := + [set z | forall y, E y -> (z <= y)%O]. -(* Real down set (i.e., generated order ideal) *) +(* down set (i.e., generated order ideal) *) (* i.e. down E := { x | exists y, y \in E /\ x <= y} *) -Definition down (E : pred R) : pred R := - [pred x | `[exists y, (y \in E) && (x <= y)]]. +Definition down (E : set R) : set R := + [set x | exists y, E y /\ (x <= y)%O]. (* Real set supremum and infimum existence condition. *) -Definition has_ub (E : pred R) := nonempty (ub E). -Definition has_sup (E : pred R) := nonempty E /\ has_ub E. -Definition has_lb (E : pred R) := nonempty (lb E). -Definition has_inf (E : pred R) := nonempty E /\ has_lb E. +Definition has_ub (E : set R) := nonempty (ub E). +Definition has_sup (E : set R) := nonempty E /\ has_ub E. +Definition has_lb (E : set R) := nonempty (lb E). +Definition has_inf (E : set R) := nonempty E /\ has_lb E. End ArchiBound. @@ -61,15 +62,15 @@ Section Mixin. Variable (R : archiFieldType). Record mixin_of : Type := Mixin { - sup : pred R -> R; + sup : set R -> R; _ : - forall E : pred (Num.ArchimedeanField.sort R), - has_sup E -> sup E \in ub E; + forall E : set (Num.ArchimedeanField.sort R), + has_sup E -> ub E (sup E); _ : - forall (E : pred (Num.ArchimedeanField.sort R)) (eps : R), + forall (E : set (Num.ArchimedeanField.sort R)) (eps : R), has_sup E -> 0 < eps -> exists2 e : R, E e & (sup E - eps) < e; _ : - forall E : pred (Num.ArchimedeanField.sort R), + forall E : set (Num.ArchimedeanField.sort R), ~ has_sup E -> sup E = 0 }. @@ -199,31 +200,28 @@ Export Real.Exports. (* -------------------------------------------------------------------- *) Definition sup {R : realType} := Real.sup (Real.class R). -Local Notation "-` E" := [pred x | - x \in E] - (at level 35, right associativity) : fun_scope. -Definition inf {R : realType} (E : pred R) := - sup (-` E). +(*Local Notation "-` E" := [pred x | - x \in E] + (at level 35, right associativity) : fun_scope.*) +Definition inf {R : realType} (E : set R) := - sup (-%R @` E). (* -------------------------------------------------------------------- *) Section BaseReflect. Context {R : archiFieldType}. -Implicit Types E : pred R. +Implicit Types E : set R. Implicit Types x : R. -Lemma nonemptyP E : nonempty E <-> exists x, x \in E. +Lemma nonemptyP E : nonempty E <-> exists x, E x. Proof. by []. Qed. -Lemma ubP E x : reflect (forall y, y \in E -> y <= x) (x \in ub E). -Proof. by apply: (iffP (forallbP _))=> h y; apply/implyP/h. Qed. +Lemma ubP E x : (forall y, E y -> y <= x) <-> (ub E x). +Proof. by []. Qed. -Lemma lbP E x : reflect (forall y, y \in E -> x <= y) (x \in lb E). -Proof. by apply: (iffP (forallbP _))=> h y; apply/implyP/h. Qed. +Lemma lbP E x : (forall y, E y -> x <= y) <-> (lb E x). +Proof. by []. Qed. -Lemma downP E x : reflect (exists2 y, y \in E & x <= y) (x \in down E). -Proof. -apply: (iffP (existsbP _))=> [[y /andP[]]|[y]]. - by exists y. by exists y; apply/andP; split. -Qed. +Lemma downP E x : (exists2 y, E y & x <= y) <-> (down E x). +Proof. split => [[y Ey xy]|[y [Ey xy]]]; by [exists y| exists y]. Qed. Lemma has_ubP {E} : has_ub E <-> nonempty (ub E). Proof. by []. Qed. @@ -241,15 +239,15 @@ End BaseReflect. (* -------------------------------------------------------------------- *) -Lemma sup_upper_bound {R : realType} (E : pred R): - has_sup E -> (forall x, x \in E -> x <= sup E). -Proof. by move=> supE; apply/ubP; case: R E supE=> ? [? ? []]. Qed. +Lemma sup_upper_bound {R : realType} (E : set R): + has_sup E -> (forall x, E x -> x <= sup E). +Proof. by move=> supE; case: R E supE=> ? [? ? []]. Qed. -Lemma sup_adherent {R : realType} (E : pred R) (eps : R) : - has_sup E -> 0 < eps -> exists2 e : R, e \in E & (sup E - eps) < e. +Lemma sup_adherent {R : realType} (E : set R) (eps : R) : + has_sup E -> 0 < eps -> exists2 e : R, E e & (sup E - eps) < e. Proof. by case: R E eps=> ? [? ? []]. Qed. -Lemma sup_out {R : realType} (E : pred R) : ~ has_sup E -> sup E = 0. +Lemma sup_out {R : realType} (E : set R) : ~ has_sup E -> sup E = 0. Proof. by case: R E => ? [? ? []]. Qed. (* -------------------------------------------------------------------- *) @@ -338,14 +336,13 @@ Section RealDerivedOps. Variable R : realType. Implicit Types x y : R. - -Definition floor_set x := [pred y | (y \is a Rint) && (y <= x)]. +Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)]. Definition floor x : R := sup (floor_set x). Definition ifloor x : int := Rtoint (floor x). -Definition range1 (x : R) := [pred y | x <= y < x + 1]. +Definition range1 (x : R) := [set y | x <= y < x + 1]. End RealDerivedOps. (*-------------------------------------------------------------------- *) @@ -353,61 +350,54 @@ Section RealLemmas. Variables (R : realType). -Implicit Types E : pred R. +Implicit Types E : set R. Implicit Types x : R. -Lemma sup_ub {E} : has_ub E -> sup E \in ub E. +Lemma sup_ub {E} : has_ub E -> (ub E) (sup E). Proof. move=> ubE; apply/ubP=> x x_in_E; apply/sup_upper_bound=> //. by apply/has_supP; split; first by exists x. Qed. -Lemma sup_total {E} x : has_sup E -> (x \in down E) || (sup E <= x). +Lemma sup_total {E} x : has_sup E -> (down E) x \/ sup E <= x. Proof. -move=> has_supE; rewrite orbC; case: (lerP (sup E) x)=> hx //=. +move=> has_supE; rewrite orC. +case: (lerP (sup E) x)=> hx /=; [by left|right]. have /(sup_adherent has_supE) : 0 < sup E - x by rewrite subr_gt0. case=> e Ee hlte; apply/downP; exists e => //; move: hlte. by rewrite opprB addrCA subrr addr0 => /ltW. Qed. -Lemma sup_le_ub {E} x : nonempty E -> x \in ub E -> sup E <= x. +Lemma sup_le_ub {E} x : nonempty E -> (ub E) x -> sup E <= x. Proof. move=> hasE /ubP leEx; set y := sup E; pose z := (x + y) / 2%:R. have Dz: 2%:R * z = x + y. by rewrite mulrCA divff ?mulr1 // pnatr_eq0. -have ubE: has_sup E by split; last by exists x; apply/ubP. -have /orP [/downP [t Et lezt] | leyz] := sup_total z ubE. +have ubE : has_sup E by split; last by exists x. +have [/downP [t Et lezt] | leyz] := sup_total z ubE. rewrite -(ler_add2l x) -Dz -mulr2n -[X in _<=X]mulr_natl. rewrite ler_pmul2l ?ltr0Sn //; exact/(le_trans lezt)/leEx. rewrite -(ler_add2r y) -Dz -mulr2n -[X in X<=_]mulr_natl. by rewrite ler_pmul2l ?ltr0Sn. Qed. -Lemma nonemptybP {E} : - `[< nonempty E >] = `[< exists x : R, x \in E >]. -Proof. by apply: (asbool_equiv_eq (nonemptyP _)). Qed. +Lemma nonemptyPn {E} : ~ nonempty E <-> (forall x, ~ E x). +Proof. split => [h x Ex|h [x Ex]]; by [apply h; exists x| apply (h x)]. Qed. -Lemma nonemptyPn {E} : - ~ nonempty E <-> (forall x, x \notin E). +Lemma has_ubPn {E} : ~ has_ub E <-> (forall x, exists2 y, E y & x < y). Proof. -by apply: asbool_eq_equiv; rewrite asbool_neg nonemptybP asbool_forallNb. -Qed. - -Lemma has_ubPn {E} : - ~ has_ub E <-> (forall x, exists2 y, y \in E & x < y). -Proof. split; last first. -+ move=> h /has_ubP [x /ubP] hle; case/(_ x): h => y /hle. +split; last first. + move=> h /has_ubP [x] hle; case/(_ x): h => y /hle. by rewrite leNgt => /negbTE ->. -move/asboolPn; rewrite (asbool_equiv_eq has_ubP). -move/asboolPn/nonemptyPn=> h x; have /ubP {h} := h x. -case/asboolPn/existsp_asboolPn=> y /asboolPn /imply_asboolPn. -by case=> [yE /negP]; rewrite -ltNge => ltx; exists y. +move/forallp_Pn => h x; have {h} := h x. +move=> /existsp_Pn => -[y /imply_Pn[Ey /negP]]. +by rewrite -ltNge => ltx; exists y. Qed. Lemma has_supPn {E} : nonempty E -> - ~ has_sup E <-> (forall x, exists2 y, y \in E & x < y). + ~ has_sup E <-> (forall x, exists2 y, E y & x < y). Proof. -move=> nzE; split=> [/asboolPn|]; rewrite ?(asbool_equiv_eq has_supP). +move=> nzE; split=> [/asboolPn|]; first rewrite (asbool_equiv_eq has_supP). by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_ubPn. by move/has_ubPn=> h /has_supP [_]. Qed. @@ -419,85 +409,97 @@ Section InfTheory. Variables (R : realType). -Implicit Types E : pred R. +Implicit Types E : set R. Implicit Types x : R. -Lemma setNK : involutive (fun E => -` E). -Proof. by move=> E; rewrite funeqE => ?; rewrite !inE opprK. Qed. +Lemma setNK : involutive (fun E : set R => -%R @` E). +Proof. +move=> F; rewrite predeqE => y; split => [|Fy]. + by case=> z -[u xu <-{z} <-{y}]; rewrite opprK. +by exists (- y); rewrite ?opprK //; exists y. +Qed. -Lemma memNE E x : (x \in E) = (- x \in -` E). -Proof. by rewrite inE opprK. Qed. +Lemma memNE E x : E x = (-%R @` E) (- x). +Proof. +rewrite propeqE; split => [Ex|[y Ey]]; [by exists x|]. +by move/eqP; rewrite eqr_opp => /eqP <-. +Qed. -Lemma lb_ubN E x : (x \in lb E) <-> - x \in ub (-` E). +Lemma lb_ubN E x : lb E x <-> ub (-%R @` E) (- x). Proof. -split=> [/lbP|/ubP] xlbE; first by apply/ubP => ? /xlbE; rewrite ler_oppr. -by apply/lbP => y; rewrite memNE => /xlbE; rewrite ler_oppr opprK. +rewrite /lb /ub; split => [xlbE y [z Ez <-{y}]|xlbE y Ey]. +by rewrite ler_oppr opprK; apply xlbE. +by rewrite -(opprK x) ler_oppl; apply xlbE; exists y. Qed. -Lemma ub_lbN E x : (x \in ub E) <-> - x \in lb (-` E). +Lemma ub_lbN E x : ub E x <-> lb (-%R @` E) (- x). Proof. -split; first by move=> ?; apply/lb_ubN; rewrite opprK setNK. +split. + by move=> ?; apply/lb_ubN; rewrite opprK setNK. by move/lb_ubN; rewrite opprK setNK. Qed. -Lemma nonemptyN E : nonempty (-` E) <-> nonempty E. -Proof. by split=> [[x ENx]|[x Ex]]; exists (- x) => //; rewrite -memNE. Qed. +Lemma nonemptyN E : nonempty (-%R @` E) <-> nonempty E. +Proof. +split=> [[x ENx]|[x Ex]]; exists (- x); last by rewrite -memNE. +by rewrite memNE opprK. +Qed. -Lemma has_inf_supN E : has_inf E <-> has_sup (-` E). +Lemma has_inf_supN E : has_inf E <-> has_sup (-%R @` E). Proof. -split=> [/has_infP [En0 [x /lb_ubN xlbe]]|/has_supP [NEn0 [x /ub_lbN xubE]]]. +split=> [/has_infP [En0 [x /lb_ubN xlbe]] |/has_supP[NEn0 [x /ub_lbN xubE]] ]. by apply/has_supP; split; [apply/nonemptyN|exists (- x)]. by apply/has_infP; split; [apply/nonemptyN|rewrite -[E]setNK; exists (- x)]. Qed. -Lemma inf_lower_bound E : - has_inf E -> (forall x, x \in E -> inf E <= x). +Lemma inf_lower_bound E : has_inf E -> (forall x, E x -> inf E <= x). Proof. move=> /has_inf_supN /sup_upper_bound inflb x. by rewrite memNE => /inflb; rewrite ler_oppl. Qed. Lemma inf_adherent E (eps : R) : - has_inf E -> 0 < eps -> exists2 e, e \in E & e < inf E + eps. + has_inf E -> 0 < eps -> exists2 e, E e & e < inf E + eps. Proof. move=> /has_inf_supN supNE /(sup_adherent supNE) [e NEx egtsup]. -by exists (- e) => //; rewrite ltr_oppl -mulN1r mulrDr !mulN1r opprK. +exists (- e); first by case: NEx => x Ex <-{}; rewrite opprK. +by rewrite ltr_oppl -mulN1r mulrDr !mulN1r opprK. Qed. Lemma inf_out E : ~ has_inf E -> inf E = 0. Proof. -move=> ninfE; rewrite -oppr0 -(@sup_out _ (-` E)) => // supNE; apply: ninfE. +move=> ninfE; rewrite -oppr0 -(@sup_out _ (-%R @` E)) => // supNE; apply: ninfE. exact/has_inf_supN. Qed. -Lemma has_lb_ubN E : has_lb E <-> has_ub (-` E). +Lemma has_lb_ubN E : has_lb E <-> has_ub (-%R @` E). Proof. by split=> [/has_lbP [x /lb_ubN]|/has_ubP [x /ub_lbN]]; [|rewrite setNK]; exists (- x). Qed. -Lemma inf_lb E : has_lb E -> inf E \in lb E. +Lemma inf_lb E : has_lb E -> (lb E) (inf E). Proof. by move/has_lb_ubN/sup_ub/ub_lbN; rewrite setNK. Qed. -Lemma lb_le_inf E x : nonempty E -> x \in lb E -> x <= inf E. +Lemma lb_le_inf E x : nonempty E -> (lb E) x -> x <= inf E. Proof. by move=> /(nonemptyN E) En0 /lb_ubN /(sup_le_ub En0); rewrite ler_oppr. Qed. -Lemma has_lbPn E : - ~ has_lb E <-> (forall x, exists2 y, y \in E & y < x). +Lemma has_lbPn E : ~ has_lb E <-> (forall x, exists2 y, E y & y < x). Proof. split=> [/has_lb_ubN /has_ubPn NEnub x|Enlb /has_lb_ubN]. - by have [y ENy ltxy] := NEnub (- x); exists (- y) => //; rewrite ltr_oppl. -apply/has_ubPn => x; have [y Ey ltyx] := Enlb (- x); exists (- y). - by rewrite inE opprK. -by rewrite ltr_oppr. + have [y ENy ltxy] := NEnub (- x); exists (- y); rewrite 1?ltr_oppl //. + by case: ENy => z Ez <-; rewrite opprK. +apply/has_ubPn => x; have [y Ey ltyx] := Enlb (- x). +exists (- y); last by rewrite ltr_oppr. +by exists y => //; rewrite opprK. Qed. Lemma has_infPn E : nonempty E -> - ~ has_inf E <-> (forall x, exists2 y, y \in E & y < x). + ~ has_inf E <-> (forall x, exists2 y, E y & y < x). Proof. -move=> nzE; split=> [/asboolPn|]; rewrite ?(asbool_equiv_eq has_infP). +move=> nzE; split=> [/asboolPn|]; first rewrite (asbool_equiv_eq has_infP). by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_lbPn. by move/has_lbPn=> h /has_infP [_]. Qed. @@ -510,10 +512,10 @@ Variable R : realType. Implicit Types x y : R. -Lemma has_sup_floor_set x: has_sup (floor_set x). +Lemma has_sup_floor_set x : has_sup (floor_set x). Proof. split; [exists (- (Num.bound (-x))%:~R) | exists (Num.bound x)%:~R]. - rewrite inE rpredN rpred_int /= ler_oppl. + rewrite /floor_set rpredN rpred_int /= ler_oppl. case: (ger0P (-x)) => [/archi_boundP/ltW//|]. by move/ltW/le_trans; apply; rewrite ler0z. apply/ubP=> y /andP[_] /le_trans; apply. @@ -521,7 +523,7 @@ case: (ger0P x)=> [/archi_boundP/ltW|] //. by move/ltW/le_trans; apply; rewrite ler0z. Qed. -Lemma sup_in_floor_set x : sup (floor_set x) \in floor_set x. +Lemma sup_in_floor_set x : (floor_set x) (sup (floor_set x)). Proof. have /sup_adherent /(_ ltr01) [y Fy] := has_sup_floor_set x. have /sup_upper_bound /(_ _ Fy) := has_sup_floor_set x. @@ -545,11 +547,13 @@ Proof. by case/andP: (sup_in_floor_set x). Qed. Lemma floorE x : floor x = (ifloor x)%:~R. Proof. by rewrite /ifloor RtointK ?isint_floor. Qed. -Lemma mem_rg1_floor (x : R) : x \in range1 (floor x). +Lemma mem_rg1_floor (x : R) : (range1 (floor x)) x. Proof. -rewrite inE; have /andP[_ ->] /= := sup_in_floor_set x. -case: (boolP (floor x + 1 \in floor_set x)); last first. - by rewrite inE negb_and -ltNge rpredD // ?(Rint1, isint_floor). +rewrite /range1. +have /andP[_ ->] /= := sup_in_floor_set x. +case: (pselect ((floor_set x) (floor x + 1))); last first. + rewrite /floor_set => /negP. + by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_floor). by move/sup_upper_bound=> -/(_ (has_sup_floor_set x)); rewrite ger_addl ler10. Qed. @@ -560,24 +564,24 @@ Lemma floorS_gtr (x : R) : x < floor x + 1. Proof. by case/andP: (mem_rg1_floor x). Qed. Lemma range1z_inj (x : R) (m1 m2 : int) : - x \in range1 m1%:~R -> x \in range1 m2%:~R -> m1 = m2. + (range1 m1%:~R) x -> (range1 m2%:~R) x -> m1 = m2. Proof. move=> /andP[m1x x_m1] /andP[m2x x_m2]. wlog suffices: m1 m2 m1x {x_m1 m2x} x_m2 / (m1 <= m2). by move=> ih; apply/eqP; rewrite eq_le !ih. rewrite -(ler_add2r 1) lez_addr1 -(@ltr_int R) intrD. -by apply/(le_lt_trans m1x). +exact/(le_lt_trans m1x). Qed. -Lemma range1rr (x : R) : x \in range1 x. -Proof. by rewrite inE lexx /= ltr_addl ltr01. Qed. +Lemma range1rr (x : R) : (range1 x) x. +Proof. by rewrite /range1 lexx /= ltr_addl ltr01. Qed. Lemma range1zP (m : int) (x : R) : - reflect (floor x = m%:~R) (x \in range1 m%:~R). + floor x = m%:~R <-> (range1 m%:~R) x. Proof. -apply: (iffP idP)=> [h|<-]; [apply/eqP | by apply/mem_rg1_floor]. -rewrite floorE eqr_int; apply/eqP/(@range1z_inj x) => //. -by rewrite -floorE mem_rg1_floor. +split=> [<-|h]; first exact/mem_rg1_floor. +apply/eqP; rewrite floorE eqr_int; apply/eqP/(@range1z_inj x) => //. +by rewrite /range1 -floorE mem_rg1_floor. Qed. Lemma floor_natz (x : int) : floor x%:~R = x%:~R :> R. @@ -610,17 +614,18 @@ End FloorTheory. Section Sup. Context {R : realType}. -Lemma le_down (S : pred R) : {subset S <= down S}. +Lemma le_down (S : set R) : S `<=` down S. Proof. by move=> x xS; apply/downP; exists x. Qed. -Lemma downK (S : pred R) : down (down S) =i down S. +Lemma downK (S : set R) : down (down S) = down S. Proof. -move=> x; apply/downP/downP=> -[y yS le_xy]; last first. - by exists y=> //; apply/le_down. -by case/downP: yS => z zS le_yz; exists z => //; apply/(le_trans le_xy). +rewrite predeqE => x; split. +- case/downP => y /downP[z Sz yz xy]. + by apply/downP; exists z => //; rewrite (le_trans xy). +- by move=> Sx; apply/downP; exists x. Qed. -Lemma eq_ub (S1 S2 : pred R) : S2 =i S1 -> ub S2 =i ub S1. +(*Lemma eq_ub (S1 S2 : set R) : S2 =i S1 -> ub S2 =i ub S1. Proof. move=> eq_12 x; apply/ubP/ubP=> h y yS; apply/h; by rewrite (eq_12, =^~ eq_12). @@ -682,8 +687,8 @@ Lemma eq_inf (S1 S2 : pred R) : S2 =i S1 -> inf S2 = inf S1. Proof. by move=> eq_12; rewrite /inf; apply/congr1/eq_sup => ?; rewrite inE eq_12. Qed. - -Lemma has_sup_down (S : pred R) : has_sup (down S) <-> has_sup S. +*) +Lemma has_sup_down (S : set R) : has_sup (down S) <-> has_sup S. Proof. split=> /has_supP [nzS nzubS]; apply/has_supP. case: nzS=> x /downP[y yS le_xy]; split; first by exists y. @@ -694,8 +699,8 @@ case: nzubS=> u /ubP ubS; exists u; apply/ubP=> y /downP []. by move=> z zS /le_trans; apply; apply/ubS. Qed. -Lemma le_sup (S1 S2 : pred R) : - {subset S1 <= down S2} -> nonempty S1 -> has_sup S2 +Lemma le_sup (S1 S2 : set R) : + S1 `<=` down S2 -> nonempty S1 -> has_sup S2 -> sup S1 <= sup S2. Proof. move=> le_S12 nz_S1 hs_S2; have hs_S1: has_sup S1. @@ -708,53 +713,51 @@ rewrite subKr => lt_S2x; case/downP: xdS2=> z zS2. by move/(lt_le_trans lt_S2x); rewrite ltNge sup_upper_bound. Qed. -Lemma sup_down (S : pred R) : sup (down S) = sup S. +Lemma sup_down (S : set R) : sup (down S) = sup S. Proof. -case/boolP: `[< has_sup S >] => [/asboolP|/asboolPn]; last first. +case: (pselect (has_sup S)); last first. by move=> supNS; rewrite !sup_out // => /has_sup_down. move=> supS; have supDS: has_sup (down S) by apply/has_sup_down. apply/eqP; rewrite eq_le !le_sup //. by case/has_supP: supS => -[x xS] _; exists x; apply/le_down. - by move=> x xS; rewrite downK le_down. + rewrite downK; exact: le_down. by case/has_supP: supS. Qed. -Lemma sup1 (c : R) : sup (pred1 c) = c. +Lemma sup1 (c : R) : sup [set c] = c. Proof. -have hs: has_sup (pred1 c); first (apply/has_supP; split; exists c). - by rewrite inE eqxx. by apply/ubP => y; rewrite inE => /eqP->. -apply/eqP; rewrite eq_le sup_upper_bound ?inE // andbT. -apply/sup_le_ub; first by exists c; rewrite inE eqxx. -by apply/ubP=> y; rewrite inE => /eqP ->. +have hs : has_sup [set c]; first (apply/has_supP; split; exists c => //). +by move=> y <-. +apply/eqP; rewrite eq_le sup_upper_bound // andbT; apply/sup_le_ub. +by exists c. +by move=> y <-. Qed. -Lemma inf1 (c : R) : inf (pred1 c) = c. +Lemma inf1 (c : R) : inf [set c] = c. Proof. -rewrite /inf; have /eq_sup -> : -` (pred1 c) =i pred1 (- c). - by move=> ?; rewrite !inE eqr_oppLR. +rewrite /inf (_ : -%R @` (set1 c) = set1 (- c)). +by rewrite predeqE => x; split => [[y <- <-] //|->]; exists c. by rewrite sup1 opprK. Qed. Lemma lt_sup_imfset {T : Type} (F : T -> R) l : - has_sup [pred y | `[exists x, y == F x]] -> - l < sup [pred y | `[exists x, y == F x]] -> - exists2 x, l < F x & F x <= sup [pred y | `[exists x, y == F x]]. + has_sup [set y | exists x, y = F x] -> + l < sup [set y | exists x, y = F x] -> + exists2 x, l < F x & F x <= sup [set y | exists x, y = F x]. Proof. -set P := [pred y | _]; move=> hs; rewrite -subr_gt0. -case/(sup_adherent hs)=> _ /imsetbP[x ->]; rewrite subKr => lt_lFx. -exists x=> //; apply/sup_upper_bound => //. -by apply/imsetbP; exists x. +set P := [set y | _]; move=> hs; rewrite -subr_gt0. +case/(sup_adherent hs)=> _ [x ->]; rewrite subKr => lt_lFx. +by exists x => //; apply/sup_upper_bound => //; exists x. Qed. Lemma lt_inf_imfset {T : Type} (F : T -> R) l : - has_inf [pred y | `[exists x, y == F x]] -> - inf [pred y | `[exists x, y == F x]] < l -> - exists2 x, F x < l & inf [pred y | `[exists x, y == F x]] <= F x. -Proof. -set P := [pred y | _]; move=> hs; rewrite -subr_gt0. -case/(inf_adherent hs)=> _ /imsetbP[x ->]; rewrite addrA [_ + l]addrC addrK. -move=> ltFxl; exists x=> //; apply/inf_lower_bound => //. -by apply/imsetbP; exists x. + has_inf [set y | exists x, y = F x] -> + inf [set y | exists x, y = F x] < l -> + exists2 x, F x < l & inf [set y | exists x, y = F x] <= F x. +Proof. +set P := [set y | _]; move=> hs; rewrite -subr_gt0. +case/(inf_adherent hs)=> _ [x ->]; rewrite addrA [_ + l]addrC addrK. +by move=> ltFxl; exists x=> //; apply/inf_lower_bound => //; exists x. Qed. End Sup. From d72641758a7264cb613a2c1029f49285db9de9fd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 12 May 2020 05:30:13 +0900 Subject: [PATCH 2/6] Sets of supremums of extended reals are not empty - move Section ArchiBound from `reals.v` to `classical_sets.v` + could factorize the two definitions of `nonempty` - new lemmas `lee_ninfty_eq` and `lee_ninfty_eq` - new lemma `image_set0` in `classical_sets.v` - move `Section ERealOrderTheory` from `reals.v` to `ereal.v` - new `Section ereal_supremum` in `ereal.v` + Lemma `ereal_supremums_neq0` (sets of supremums of extended reals are not empty) --- theories/boolp.v | 7 ++ theories/classical_sets.v | 44 ++++++++++++ theories/ereal.v | 139 +++++++++++++++++++++++++++++++++++++- theories/normedtype.v | 4 +- theories/reals.v | 134 +----------------------------------- 5 files changed, 190 insertions(+), 138 deletions(-) diff --git a/theories/boolp.v b/theories/boolp.v index d9c3200e8d..ecb8559463 100644 --- a/theories/boolp.v +++ b/theories/boolp.v @@ -561,6 +561,13 @@ split => [[x Px h]|/asboolP]; [exact: Px|]. by rewrite asbool_neg => /existsp_asboolPn. Qed. +Lemma existsp_P (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. +Qed. + Lemma forallp_Pn (T : Type) (P : T -> Prop) : (forall x : T, ~ P x) <-> (~ exists x : T, P x). Proof. diff --git a/theories/classical_sets.v b/theories/classical_sets.v index 19cf5d038d..fbacad2ec6 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -290,6 +290,9 @@ apply eqEsubset => b. - by case=> -[] a Ha <-; apply imageP; [left | right]. Qed. +Lemma image_set0 T U (f : T -> U) : f @` set0 = set0. +Proof. by apply eqEsubset => b // -[]. Qed. + Lemma image_set1 T U (f : T -> U) (t : T) : f @` [set t] = [set f t]. Proof. by apply eqEsubset => b; [case=> a' -> <- | move->; apply imageP]. Qed. @@ -817,3 +820,44 @@ have /Amax <- : R' A (lift t). by have [Rt _] := repr_liftE t; apply: Rtrans Rt. by have [] := repr_liftE t. Qed. + +(* -------------------------------------------------------------------- *) +Section ArchiBound. + +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]. + +(* 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]. + +(* 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 supremums E := [set x | ub E x /\ (forall y, ub E y -> (x <= y)%O)]. + +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. +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. +Qed. + +Definition supremum (x0 : T) E := + if pselect (E !=set0) then xget x0 (supremums E) else x0. + +End ArchiBound. diff --git a/theories/ereal.v b/theories/ereal.v index de3da17306..38d9cfa237 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -4,10 +4,8 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -(* NB: taken out from reals.v and generalized in 2019 *) - From mathcomp Require Import all_ssreflect all_algebra. -Require Import boolp. +Require Import boolp classical_sets reals. Set Implicit Arguments. Unset Strict Implicit. @@ -175,6 +173,12 @@ Proof. exact: num_real. Qed. Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x). Proof. case: x => //= r; exact: num_real. Qed. +Lemma lee_ninfty_eq (R : numDomainType) (x : {ereal R}) : (x <= -oo)%E = (x == -oo%E). +Proof. by case: x. Qed. + +Lemma lee_pinfty_eq (R : numDomainType) (x : {ereal R}) : (+oo <= x)%E = (x == +oo%E). +Proof. by case: x. Qed. + Section ERealOrder_realDomainType. Context {R : realDomainType}. Implicit Types (x y : {ereal R}). @@ -373,3 +377,132 @@ Lemma lee_add2r x a b : (a <= b)%E -> (a + x <= b + x)%E. Proof. rewrite addeC (addeC b); exact: lee_add2l. Qed. End ERealArithTh_realDomainType. + +(* -------------------------------------------------------------------- *) +(* TODO: Check for duplications with `order.v`. Remove them. *) +Section ERealOrderTheory. +Context {R : numDomainType}. +Implicit Types x y z : {ereal R}. + +Local Tactic Notation "elift" constr(lm) ":" ident(x) := + by case: x => [||?]; first by rewrite ?eqe; apply: lm. + +Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) := + by case: x y => [?||] [?||]; first by rewrite ?eqe; apply: lm. + +Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) ident(z) := + by case: x y z => [?||] [?||] [?||]; first by rewrite ?eqe; apply: lm. + +Lemma le0R (x : {ereal R}) : + (0%:E <= x)%E -> (0 <= real_of_er(*TODO: coercion broken*) x)%R. +Proof. by case: x. Qed. + +Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%O -> (r0%:E <= r1%:E)%E. +Proof. by []. Qed. + +Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%O -> (r0%:E < r1%:E)%E. +Proof. by []. Qed. +End ERealOrderTheory. + +Lemma lee_opp2 {R : realDomainType} : {mono @eopp R : x y /~ (x <= y)%E}. +Proof. +move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !ler_opp2. +by rewrite lee_ninfty /Order.le /= realN num_real. +by rewrite lee_pinfty /Order.le /= realN num_real. +Qed. + +Lemma lte_opp2 {R : realDomainType} : {mono @eopp R : x y /~ (x < y)%E}. +Proof. +move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltr_opp2. +by rewrite lte_ninfty /Order.lt /= realN num_real. +by rewrite lte_pinfty /Order.lt /= realN num_real. +Qed. + +Section ereal_supremum. +Variable R : realType. +Local Open Scope classical_set_scope. +Implicit Types S : set {ereal R}. +Implicit Types x : {ereal R}. + +Lemma ereal_ub_pinfty S : ub S +oo. +Proof. by move=> x _; rewrite lee_pinfty. Qed. + +Lemma ereal_ub_set1 x : ub [set x] x. +Proof. by move=> /= y ->. Qed. + +Lemma ereal_ub_ninfty S : ub S -oo -> S = set0 \/ S = [set -oo]. +Proof. +have [[x Sx] Snoo|/set0P/negP] := pselect (S !=set0). + right; rewrite predeqE => y; split => [/Snoo|->{y}]. + by rewrite lee_ninfty_eq => /eqP ->. + by have := Snoo _ Sx; rewrite lee_ninfty_eq => /eqP <-. +by rewrite negbK => /eqP -> _; left. +Qed. + +Let real_of_er_def r0 x : R := if x is r%:E then r else r0. +(* NB: see also real_of_er above *) + +Lemma ereal_supremums_neq0 S : supremums S !=set0. +Proof. +have [/eqP ->|Snoo] := pselect (S == [set -oo]). + by exists -oo; split => [|/= y /(_ -oo)]; [exact: ereal_ub_set1 | exact]. +have [S0|/set0P/negP] := pselect (S !=set0); last first. + by rewrite negbK => /eqP ->; exists -oo; split => // y _; rewrite lee_ninfty. +have [Spoo|Spoo] := pselect (S +oo). + by exists +oo; split => [|/= y /(_ _ Spoo) //]; exact: ereal_ub_pinfty. +have [r Sr] : exists r, S r%:E. + move: S0 Snoo Spoo => [[r Sr _ _|//|Snoo Snoo1 Spoo]]; first by exists r. + apply/existsp_P => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE. + by case=> // r; split => // /nS. +set U := [set x | (real_of_er_def r @` S) x ]. +have [ubU|/set0P/negP] := pselect (ub U !=set0); last first. + rewrite negbK => /eqP; rewrite -subset0 => U0; exists +oo. + split => [|/= [r0 Sr0|//|]]; first exact: ereal_ub_pinfty. + - suff : ub U r0 by move/U0. + by move=> y -[] [r1 Sr1 <-| // | /= _ <-{y}]; rewrite -lee_fin; apply Sr0. + - by move/ereal_ub_ninfty => [|] /eqP //; move/set0P : S0 => /negbTE => ->. +set u : R := sup U. +exists u%:E; split; last first. + case => [r0 Sr0| |]. + - rewrite lee_fin; apply/sup_le_ub; first by exists r, r%:E. + by apply/ubP => r1 -[[r2 /= Sr2 <-{r1}| // | /= _ <-{r1}]]; + rewrite -lee_fin; exact: Sr0. + - by rewrite lee_pinfty. + - by move/ereal_ub_ninfty => [|/eqP //] => /eqP; move/set0P : S0 => /negbTE ->. +case=> [r0 Sr0|//|_]; last by rewrite lee_ninfty. +rewrite lee_fin; apply sup_upper_bound; last by exists r0%:E. +apply/has_supP; split; first by exists r0, r0%:E. +exists u; apply/ubP => y; move=> [] y' Sy' <-{y}. +apply/sup_upper_bound. +- apply/has_supP; split; first by exists r, r%:E. + by case: ubU => x ubUx; exists x. +by case: y' Sy' => [r1 /= Sr1 | // | /= _]; [exists r1%:E | exists r%:E]. +Qed. + +Definition ereal_sup S := supremum -oo S. + +Definition ereal_inf S := - ereal_sup (eopp @` S). + +Lemma ereal_sup_set0 : ereal_sup set0 = -oo. +Proof. by rewrite /ereal_sup /supremum; case: pselect => // -[]. Qed. + +Lemma ereal_sup_set1 x : ereal_sup [set x] = x. +Proof. +rewrite /ereal_sup /supremum; case: pselect => /= [_|x0]; last first. + by exfalso; apply x0; exists x. +by rewrite supremums_set1; case: xgetP => // /(_ x) /(_ erefl). +Qed. + +Lemma ereal_inf_set0 : ereal_inf set0 = +oo. +Proof. by rewrite /ereal_inf image_set0 ereal_sup_set0. Qed. + +Lemma ereal_sup_ub S y (Sy : S y) : y <= ereal_sup S. +Proof. +rewrite /ereal_sup /supremum. +case: pselect => /= [S0|/(_ (ex_intro S y Sy)) //]. +case: xgetP => /=. +by move=> x ->{x} -[] geS _; apply geS. +by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). +Qed. + +End ereal_supremum. diff --git a/theories/normedtype.v b/theories/normedtype.v index f6350da1b0..1023008813 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2591,7 +2591,7 @@ 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 inE. +have Altxn0 : nonempty Altx by exists y; rewrite inE. have xub_Altx : (ub Altx) x. by apply/ubP => ?; rewrite inE => - [_ /ltW]. have Altxsup : has_sup Altx by apply/has_supP; split=> //; exists x. @@ -2723,7 +2723,7 @@ rewrite le_eqVlt => /orP [/eqP<- _|ltfav]. rewrite le_eqVlt => /orP [/eqP->|ltvfb]. by exists b => //; rewrite inE/= lexx leab. set A := [set c | (c <= b) && (f c <= v)]. -have An0 : reals.nonempty A by exists a; apply/andP; split=> //; apply: ltW. +have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW. have supA : has_sup A. by apply/has_supP; split=> //; exists b; apply/ubP => ? /andP []. have supAab : sup A \in `[a, b]. diff --git a/theories/reals.v b/theories/reals.v index 0d57811509..b1dbae7fea 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -9,7 +9,7 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import all_ssreflect all_algebra. -(* ------- *) Require Import boolp ereal classical_sets. +(* ------- *) Require Import boolp classical_sets. Require Import Setoid. @@ -27,34 +27,6 @@ Delimit Scope real_scope with real. Local Open Scope ring_scope. Local Open Scope classical_set_scope. -(* -------------------------------------------------------------------- *) -Section ArchiBound. - -Variables (d : unit) (R : porderType d). - -(* set non-emptyness. *) -Definition nonempty (E : set R) := - exists x : R, E x. - -(* upper bound and lower bound sets. *) -Definition ub (E : set R) : set R := - [set z | forall y, E y -> (y <= z)%O]. -Definition lb (E : set R) : set R := - [set z | forall y, E y -> (z <= y)%O]. - -(* down set (i.e., generated order ideal) *) -(* i.e. down E := { x | exists y, y \in E /\ x <= y} *) -Definition down (E : set R) : set R := - [set x | exists y, E y /\ (x <= y)%O]. - -(* Real set supremum and infimum existence condition. *) -Definition has_ub (E : set R) := nonempty (ub E). -Definition has_sup (E : set R) := nonempty E /\ has_ub E. -Definition has_lb (E : set R) := nonempty (lb E). -Definition has_inf (E : set R) := nonempty E /\ has_lb E. - -End ArchiBound. - (* -------------------------------------------------------------------- *) Module Real. Section Mixin. @@ -625,69 +597,6 @@ rewrite predeqE => x; split. - by move=> Sx; apply/downP; exists x. Qed. -(*Lemma eq_ub (S1 S2 : set R) : S2 =i S1 -> ub S2 =i ub S1. -Proof. -move=> eq_12 x; apply/ubP/ubP=> h y yS; apply/h; - by rewrite (eq_12, =^~ eq_12). -Qed. - -Lemma eq_lb (S1 S2 : pred R) : S2 =i S1 -> lb S2 =i lb S1. -Proof. -by move=> eq_12 x; apply/lbP/lbP=> h y yS; apply/h; rewrite (eq_12, =^~ eq_12). -Qed. - -Lemma eq_has_ub (S1 S2 : pred R) : S2 =i S1 -> has_ub S2 -> has_ub S1. -Proof. -move=> eq_12 /has_ubP[x /ubP xS2]; apply/has_ubP; exists x; apply/ubP => y yS1. -by apply xS2; rewrite eq_12. -Qed. - -Lemma eq_has_lb (S1 S2 : pred R) : S2 =i S1 -> has_lb S2 -> has_lb S1. -Proof. -move=> eq_12 /has_lbP[x /lbP xS2]; apply/has_lbP; exists x; apply/lbP => y yS1. -by apply xS2; rewrite eq_12. -Qed. - -Lemma eq_has_sup (S1 S2 : pred R) : - S2 =i S1 -> has_sup S2 -> has_sup S1. -Proof. -move=> eq_12 /has_supP[[x xS2] [u uS2]]; apply/has_supP; split. - by exists x; rewrite -eq_12. by exists u; rewrite (@eq_ub S2). -Qed. - -Lemma eq_has_inf (S1 S2 : pred R) : - S2 =i S1 -> has_inf S2 -> has_inf S1. -Proof. -move=> eq_12 /has_inf_supN infS1; apply/has_inf_supN; apply: eq_has_sup infS1. -by move=> ?; rewrite inE eq_12. -Qed. - -Lemma eq_has_supb (S1 S2 : pred R) : - S2 =i S1 -> `[< has_sup S2 >] = `[< has_sup S1 >]. -Proof. by move=> eq_12; apply/asboolP/asboolP; apply/eq_has_sup. Qed. - -Lemma eq_has_infb (S1 S2 : pred R) : - S2 =i S1 -> `[< has_inf S2 >] = `[< has_inf S1 >]. -Proof. by move=> eq_12; apply/asboolP/asboolP; apply/eq_has_inf. Qed. - -Lemma eq_sup (S1 S2 : pred R) : S2 =i S1 -> sup S2 = sup S1. -Proof. -wlog: S1 S2 / (sup S1 <= sup S2) => [wlog|le_S1S2] eq_12. - by case: (lerP (sup S1) (sup S2)) => [|/ltW] /wlog ->. -move: le_S1S2; rewrite le_eqVlt => /orP[/eqP->//|lt_S1S2]. -case/boolP: `[< has_sup S2 >] => [/asboolP|] h2; last first. - by rewrite !sup_out // => /asboolPn; rewrite -?(eq_has_supb eq_12). -pose x : R := sup S2 - sup S1; have gt0_x: 0 < x by rewrite subr_gt0. -have [e eS2] := sup_adherent h2 gt0_x; rewrite subKr => lt_S1e. -have /(eq_has_sup eq_12) h1 := h2; have := eS2; rewrite eq_12. -by move/sup_upper_bound=> -/(_ h1); rewrite leNgt lt_S1e. -Qed. - -Lemma eq_inf (S1 S2 : pred R) : S2 =i S1 -> inf S2 = inf S1. -Proof. -by move=> eq_12; rewrite /inf; apply/congr1/eq_sup => ?; rewrite inE eq_12. -Qed. -*) Lemma has_sup_down (S : set R) : has_sup (down S) <-> has_sup S. Proof. split=> /has_supP [nzS nzubS]; apply/has_supP. @@ -761,44 +670,3 @@ by move=> ltFxl; exists x=> //; apply/inf_lower_bound => //; exists x. Qed. End Sup. - -(* -------------------------------------------------------------------- *) -(* TODO: There are many duplications with `order.v`. Remove them. *) -Section ERealOrderTheory. -Context {R : realDomainType}. - -Implicit Types x y z : {ereal R}. - -Local Tactic Notation "elift" constr(lm) ":" ident(x) := - by case: x => [||?]; first by rewrite ?eqe; apply: lm. - -Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) := - by case: x y => [?||] [?||]; first by rewrite ?eqe; apply: lm. - -Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) ident(z) := - by case: x y z => [?||] [?||] [?||]; first by rewrite ?eqe; apply: lm. - -Lemma le0R (l : {ereal R}) : (0%:E <= l)%E -> (0 <= real_of_er(*TODO: coercion broken*) l). -Proof. by case: l. Qed. - -Lemma lee_tofin (x y : R) : x <= y -> (x%:E <= y%:E)%E. -Proof. by []. Qed. - -Lemma lte_tofin (x y : R) : x < y -> (x%:E < y%:E)%E. -Proof. by []. Qed. - -Lemma lee_opp2 : {mono @eopp R : x y /~ (x <= y)%E}. -Proof. -move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !ler_opp2. -by rewrite lee_ninfty /Order.le /= realN num_real. -by rewrite lee_pinfty /Order.le /= realN num_real. -Qed. - -Lemma lte_opp2 : {mono @eopp R : x y /~ (x < y)%E}. -Proof. -move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltr_opp2. -by rewrite lte_ninfty /Order.lt /= realN num_real. -by rewrite lte_pinfty /Order.lt /= realN num_real. -Qed. - -End ERealOrderTheory. From 15a5a707c85123965e0aae6abbbb1059115dea14 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 16 May 2020 19:09:38 +0900 Subject: [PATCH 3/6] 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 | 6 +- theories/altreals/distr.v | 2 +- theories/altreals/realseq.v | 8 +-- theories/altreals/realsum.v | 25 ++++--- theories/boolp.v | 17 +++-- theories/classical_sets.v | 82 ++++++++++++++-------- theories/derive.v | 14 ++-- theories/ereal.v | 38 +++++----- theories/normedtype.v | 45 ++++++------ theories/reals.v | 134 +++++++++++++----------------------- 10 files changed, 183 insertions(+), 188 deletions(-) diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 0631e0a069..24936494b9 100644 --- a/theories/Rstruct.v +++ b/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. diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v index c7b928cf1e..b480132ba3 100644 --- a/theories/altreals/distr.v +++ b/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. diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v index 460fd68fb0..393c996728 100644 --- a/theories/altreals/realseq.v +++ b/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. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 904711d97c..fceeb7afe9 100644 --- a/theories/altreals/realsum.v +++ b/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. diff --git a/theories/boolp.v b/theories/boolp.v index ecb8559463..e7ae124990 100644 --- a/theories/boolp.v +++ b/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. diff --git a/theories/classical_sets.v b/theories/classical_sets.v index fbacad2ec6..cb99b49110 100644 --- a/theories/classical_sets.v +++ b/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, `[

]) 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. diff --git a/theories/derive.v b/theories/derive.v index d2a276b39e..a930bff999 100644 --- a/theories/derive.v +++ b/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. diff --git a/theories/ereal.v b/theories/ereal.v index 38d9cfa237..d32e0ed72c 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -425,57 +425,57 @@ Implicit Types S : set {ereal R}. Implicit Types x : {ereal R}. Lemma ereal_ub_pinfty S : ub S +oo. -Proof. by move=> x _; rewrite lee_pinfty. Qed. - -Lemma ereal_ub_set1 x : ub [set x] x. -Proof. by move=> /= y ->. Qed. +Proof. by apply/ubP=> x _; rewrite lee_pinfty. Qed. Lemma ereal_ub_ninfty S : ub S -oo -> S = set0 \/ S = [set -oo]. Proof. -have [[x Sx] Snoo|/set0P/negP] := pselect (S !=set0). +have [[x Sx] /ubP Snoo|/set0P/negP] := pselect (S !=set0). right; rewrite predeqE => y; split => [/Snoo|->{y}]. by rewrite lee_ninfty_eq => /eqP ->. by have := Snoo _ Sx; rewrite lee_ninfty_eq => /eqP <-. by rewrite negbK => /eqP -> _; left. Qed. +Lemma ereal_supremums_set0_ninfty : supremums (@set0 {ereal R}) -oo. +Proof. by split; [exact/ubP | apply/lbP=> y _; rewrite lee_ninfty]. Qed. + Let real_of_er_def r0 x : R := if x is r%:E then r else r0. (* NB: see also real_of_er above *) Lemma ereal_supremums_neq0 S : supremums S !=set0. Proof. have [/eqP ->|Snoo] := pselect (S == [set -oo]). - by exists -oo; split => [|/= y /(_ -oo)]; [exact: ereal_ub_set1 | exact]. + by exists -oo; split; [rewrite ub_set1 |exact: lb_ub_refl]. have [S0|/set0P/negP] := pselect (S !=set0); last first. - by rewrite negbK => /eqP ->; exists -oo; split => // y _; rewrite lee_ninfty. + by rewrite negbK => /eqP ->; exists -oo; exact: ereal_supremums_set0_ninfty. have [Spoo|Spoo] := pselect (S +oo). - by exists +oo; split => [|/= y /(_ _ Spoo) //]; exact: ereal_ub_pinfty. + by exists +oo; split; [apply/ereal_ub_pinfty | apply/lbP => /= y /ubP; apply]. have [r Sr] : exists r, S r%:E. move: S0 Snoo Spoo => [[r Sr _ _|//|Snoo Snoo1 Spoo]]; first by exists r. - apply/existsp_P => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE. + apply/existsP => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE. by case=> // r; split => // /nS. set U := [set x | (real_of_er_def r @` S) x ]. have [ubU|/set0P/negP] := pselect (ub U !=set0); last first. rewrite negbK => /eqP; rewrite -subset0 => U0; exists +oo. - split => [|/= [r0 Sr0|//|]]; first exact: ereal_ub_pinfty. + split; [exact/ereal_ub_pinfty | apply/lbP => /= -[r0 /ubP Sr0|//|]]. - suff : ub U r0 by move/U0. - by move=> y -[] [r1 Sr1 <-| // | /= _ <-{y}]; rewrite -lee_fin; apply Sr0. + by apply/ubP=> y -[] [r1 Sr1 <-| // | /= _ <-{y}]; rewrite -lee_fin; apply Sr0. - by move/ereal_ub_ninfty => [|] /eqP //; move/set0P : S0 => /negbTE => ->. set u : R := sup U. exists u%:E; split; last first. - case => [r0 Sr0| |]. + apply/lbP=> -[r0 /ubP Sr0| |]. - rewrite lee_fin; apply/sup_le_ub; first by exists r, r%:E. by apply/ubP => r1 -[[r2 /= Sr2 <-{r1}| // | /= _ <-{r1}]]; rewrite -lee_fin; exact: Sr0. - by rewrite lee_pinfty. - by move/ereal_ub_ninfty => [|/eqP //] => /eqP; move/set0P : S0 => /negbTE ->. -case=> [r0 Sr0|//|_]; last by rewrite lee_ninfty. -rewrite lee_fin; apply sup_upper_bound; last by exists r0%:E. -apply/has_supP; split; first by exists r0, r0%:E. +apply/ubP => -[r0 Sr0|//|_]; last by rewrite lee_ninfty. +rewrite lee_fin. +suff : has_sup U by move/sup_upper_bound/ubP; apply; exists r0%:E. +split; first by exists r0, r0%:E. exists u; apply/ubP => y; move=> [] y' Sy' <-{y}. -apply/sup_upper_bound. -- apply/has_supP; split; first by exists r, r%:E. - by case: ubU => x ubUx; exists x. +have : has_sup U by split; first by exists r, r%:E. +move/sup_upper_bound/ubP; apply. by case: y' Sy' => [r1 /= Sr1 | // | /= _]; [exists r1%:E | exists r%:E]. Qed. @@ -501,7 +501,7 @@ Proof. rewrite /ereal_sup /supremum. case: pselect => /= [S0|/(_ (ex_intro S y Sy)) //]. case: xgetP => /=. -by move=> x ->{x} -[] geS _; apply geS. +by move=> x ->{x} -[] /ubP geS _; apply geS. by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index 1023008813..f054d3b715 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2398,26 +2398,24 @@ have /cauchyP /(_ 1) [//|x0 x01] := F_cauchy. have D_has_sup : has_sup D; first split. - exists (x0 - 1) => A FA. near F => x. - exists x. - split. - by near: x. + apply/downP; exists x. + by near: x. by rewrite ler_distW 1?distrC 1?ltW ?andbT //; near: x. -- exists (x0 + 1) => x. - move=> /(_ _ x01) [y []]. +- exists (x0 + 1); apply/ubP => x /(_ _ x01) /downP [y []]. rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltW]. by move=> /(le_trans _) yx01 _ /yx01. exists (sup D). apply: (cvg_distW (_ : R^o)) => /= _ /posnumP[eps]; near=> x. -rewrite ler_distl sup_upper_bound //=. +rewrite ler_distl; move/ubP: (sup_upper_bound D_has_sup) => -> //=. apply: sup_le_ub => //; first by case: D_has_sup. - move=> y. - move=> /(_ (ball_ (fun x => `| x |) x eps%:num) _) []. + have Fxeps : F (ball_ [eta normr] x (eps)%:num). by near: x; apply: nearP_dep; apply: F_cauchy. - move=> z []; rewrite /ball_ ltr_distl ltr_subl_addr. + apply/ubP => y /(_ _ Fxeps) /downP[z []]. + rewrite /ball_ ltr_distl ltr_subl_addr. by move=> /andP [/ltW /(le_trans _) le_xeps _ /le_xeps]. rewrite /D /= => A FA; near F => y. -exists y; split. - by near: y. +apply/downP; exists y. +by 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,14 +2589,13 @@ 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 : nonempty Altx by exists y; rewrite inE. -have xub_Altx : (ub Altx) x. - by apply/ubP => ?; rewrite inE => - [_ /ltW]. -have Altxsup : has_sup Altx by apply/has_supP; split=> //; exists x. +have Altxn0 : Altx !=set0 by exists y; rewrite inE. +have xub_Altx : (ub Altx) x by apply/ubP => ?; rewrite inE => - [_ /ltW]. +have Altxsup : has_sup Altx by 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 inE. + by move/ubP: (sup_upper_bound Altxsup); apply; rewrite inE. have Az : A z. rewrite AeabB; split. suff : {subset `[y, x] <= `[a, b]} by apply. @@ -2610,13 +2607,14 @@ have Az : A z. 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 inE. + by move/ubP : (sup_upper_bound Altxsup); apply; 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. have := Az; rewrite AeabC => - [_ /Cop [_ /posnumP[e] ze_C]]. suff [t Altxt] : exists2 t, Altx t & z < t. - by rewrite ltNge => /negP; apply; apply/sup_upper_bound. + rewrite ltNge => /negP; apply. + by move/ubP : (sup_upper_bound Altxsup); apply => //; rewrite inE. exists (z + (minr (e%:num / 2) ((PosNum ltzx)%:num / 2))); last first. by rewrite ltr_addl. rewrite inE; split; last first. @@ -2724,12 +2722,11 @@ rewrite le_eqVlt => /orP [/eqP->|ltvfb]. by exists b => //; rewrite inE/= lexx leab. set A := [set c | (c <= b) && (f c <= v)]. have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW. -have supA : has_sup A. - by apply/has_supP; split=> //; exists b; apply/ubP => ? /andP []. +have supA : has_sup A by split=> //; exists b; apply/ubP => ? /andP []. have supAab : sup A \in `[a, b]. rewrite inE; apply/andP; split; last first. by apply: sup_le_ub => //; apply/ubP => ? /andP []. - by apply: sup_upper_bound => //; rewrite /A leab andTb ltW. + by move/ubP : (sup_upper_bound supA); apply; rewrite /A leab andTb ltW. exists (sup A) => //; have lefsupv : f (sup A) <= v. rewrite leNgt; apply/negP => ltvfsup. have vltfsup : 0 < f (sup A) - v by rewrite subr_gt0. @@ -2741,7 +2738,7 @@ exists (sup A) => //; have lefsupv : f (sup A) <= v. by rewrite ltr_add2l ltr_oppr opprK ltNge; have /andP [_ ->] := At. rewrite /= /ball /= ger0_norm. by rewrite ltr_subl_addr -ltr_subl_addl. - by rewrite subr_ge0 sup_upper_bound. + by rewrite subr_ge0; move/ubP : (sup_upper_bound supA); exact. apply/eqP; rewrite eq_le; apply/andP; split=> //. rewrite -subr_le0; apply/ler0_addgt0P => _/posnumP[e]. rewrite ler_subl_addr -ler_subl_addl ltW //. @@ -2758,8 +2755,8 @@ rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t. move=> t lttb ltsupt; move: lttb; rewrite /= distrC. by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltW. move=> t /andP [ltsupt /= letb]; rewrite ltNge; apply/negP => leftv. -move: ltsupt => /=; rewrite ltNge => /negP; apply; apply: sup_upper_bound => //. -by rewrite /A leftv letb. +move: ltsupt => /=; rewrite ltNge => /negP; apply. +by move/ubP : (sup_upper_bound supA); apply; rewrite /A leftv letb. Grab Existential Variables. all: end_near. Qed. (** Local properties in [R] *) diff --git a/theories/reals.v b/theories/reals.v index b1dbae7fea..e38a56e787 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -176,43 +176,10 @@ Definition sup {R : realType} := Real.sup (Real.class R). (at level 35, right associativity) : fun_scope.*) Definition inf {R : realType} (E : set R) := - sup (-%R @` E). -(* -------------------------------------------------------------------- *) -Section BaseReflect. -Context {R : archiFieldType}. - -Implicit Types E : set R. -Implicit Types x : R. - -Lemma nonemptyP E : nonempty E <-> exists x, E x. -Proof. by []. Qed. - -Lemma ubP E x : (forall y, E y -> y <= x) <-> (ub E x). -Proof. by []. Qed. - -Lemma lbP E x : (forall y, E y -> x <= y) <-> (lb E x). -Proof. by []. Qed. - -Lemma downP E x : (exists2 y, E y & x <= y) <-> (down E x). -Proof. split => [[y Ey xy]|[y [Ey xy]]]; by [exists y| exists y]. Qed. - -Lemma has_ubP {E} : has_ub E <-> nonempty (ub E). -Proof. by []. Qed. - -Lemma has_lbP {E} : has_lb E <-> nonempty (lb E). -Proof. by []. Qed. - -Lemma has_supP {E} : has_sup E <-> (nonempty E /\ nonempty (ub E)). -Proof. by []. Qed. - -Lemma has_infP {E} : has_inf E <-> (nonempty E /\ nonempty (lb E)). -Proof. by []. Qed. - -End BaseReflect. - (* -------------------------------------------------------------------- *) Lemma sup_upper_bound {R : realType} (E : set R): - has_sup E -> (forall x, E x -> x <= sup E). + has_sup E -> ub E (sup E). Proof. by move=> supE; case: R E supE=> ? [? ? []]. Qed. Lemma sup_adherent {R : realType} (E : set R) (eps : R) : @@ -327,8 +294,8 @@ Implicit Types x : R. Lemma sup_ub {E} : has_ub E -> (ub E) (sup E). Proof. -move=> ubE; apply/ubP=> x x_in_E; apply/sup_upper_bound=> //. -by apply/has_supP; split; first by exists x. +move=> ubE; apply/ubP=> x x_in_E; move: (x) (x_in_E). +by apply/ubP/sup_upper_bound=> //; split; first by exists x. Qed. Lemma sup_total {E} x : has_sup E -> (down E) x \/ sup E <= x. @@ -340,38 +307,35 @@ case=> e Ee hlte; apply/downP; exists e => //; move: hlte. by rewrite opprB addrCA subrr addr0 => /ltW. Qed. -Lemma sup_le_ub {E} x : nonempty E -> (ub E) x -> sup E <= x. +Lemma sup_le_ub {E} x : E !=set0 -> (ub E) x -> sup E <= x. Proof. -move=> hasE /ubP leEx; set y := sup E; pose z := (x + y) / 2%:R. +move=> hasE leEx; set y := sup E; pose z := (x + y) / 2%:R. have Dz: 2%:R * z = x + y. by rewrite mulrCA divff ?mulr1 // pnatr_eq0. -have ubE : has_sup E by split; last by exists x. +have ubE : has_sup E by split => //; exists x. have [/downP [t Et lezt] | leyz] := sup_total z ubE. rewrite -(ler_add2l x) -Dz -mulr2n -[X in _<=X]mulr_natl. - rewrite ler_pmul2l ?ltr0Sn //; exact/(le_trans lezt)/leEx. + rewrite ler_pmul2l ?ltr0Sn //; apply/(le_trans lezt). + by move/ubP : leEx; exact. rewrite -(ler_add2r y) -Dz -mulr2n -[X in X<=_]mulr_natl. by rewrite ler_pmul2l ?ltr0Sn. Qed. -Lemma nonemptyPn {E} : ~ nonempty E <-> (forall x, ~ E x). -Proof. split => [h x Ex|h [x Ex]]; by [apply h; exists x| apply (h x)]. Qed. - Lemma has_ubPn {E} : ~ has_ub E <-> (forall x, exists2 y, E y & x < y). Proof. split; last first. - move=> h /has_ubP [x] hle; case/(_ x): h => y /hle. + move=> h [x] /ubP hle; case/(_ x): h => y /hle. by rewrite leNgt => /negbTE ->. -move/forallp_Pn => h x; have {h} := h x. -move=> /existsp_Pn => -[y /imply_Pn[Ey /negP]]. +move/forallNP => h x; have {h} := h x. +move=> /ubP /existsNP => -[y /imply_classic[Ey /negP]]. by rewrite -ltNge => ltx; exists y. Qed. -Lemma has_supPn {E} : nonempty E -> +Lemma has_supPn {E} : E !=set0 -> ~ has_sup E <-> (forall x, exists2 y, E y & x < y). Proof. -move=> nzE; split=> [/asboolPn|]; first rewrite (asbool_equiv_eq has_supP). - by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_ubPn. -by move/has_ubPn=> h /has_supP [_]. +move=> nzE; split=> [/asboolPn|/has_ubPn h [_]] //. +by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_ubPn. Qed. End RealLemmas. @@ -399,16 +363,16 @@ Qed. Lemma lb_ubN E x : lb E x <-> ub (-%R @` E) (- x). Proof. -rewrite /lb /ub; split => [xlbE y [z Ez <-{y}]|xlbE y Ey]. -by rewrite ler_oppr opprK; apply xlbE. -by rewrite -(opprK x) ler_oppl; apply xlbE; exists y. +split=> [/lbP xlbE|/ubP xlbE]. +by apply/ubP=> y [z Ez <-{y}]; rewrite ler_oppr opprK; apply xlbE. +by apply/lbP => y Ey; rewrite -(opprK x) ler_oppl; apply xlbE; exists y. Qed. Lemma ub_lbN E x : ub E x <-> lb (-%R @` E) (- x). Proof. -split. - by move=> ?; apply/lb_ubN; rewrite opprK setNK. -by move/lb_ubN; rewrite opprK setNK. +split=> [? | /lb_ubN]. +by apply/lb_ubN; rewrite opprK setNK. +by rewrite opprK setNK. Qed. Lemma nonemptyN E : nonempty (-%R @` E) <-> nonempty E. @@ -419,14 +383,14 @@ Qed. Lemma has_inf_supN E : has_inf E <-> has_sup (-%R @` E). Proof. -split=> [/has_infP [En0 [x /lb_ubN xlbe]] |/has_supP[NEn0 [x /ub_lbN xubE]] ]. - by apply/has_supP; split; [apply/nonemptyN|exists (- x)]. -by apply/has_infP; split; [apply/nonemptyN|rewrite -[E]setNK; exists (- x)]. +split=> [ [En0 [x /lb_ubN xlbe]] | [NEn0 [x /ub_lbN xubE]] ]. +by split; [apply/nonemptyN|exists (- x)]. +by split; [apply/nonemptyN|rewrite -[E]setNK; exists (- x)]. Qed. -Lemma inf_lower_bound E : has_inf E -> (forall x, E x -> inf E <= x). +Lemma inf_lower_bound E : has_inf E -> lb E (inf E). Proof. -move=> /has_inf_supN /sup_upper_bound inflb x. +move=> /has_inf_supN /sup_upper_bound /ubP inflb; apply/lbP => x. by rewrite memNE => /inflb; rewrite ler_oppl. Qed. @@ -446,8 +410,7 @@ Qed. Lemma has_lb_ubN E : has_lb E <-> has_ub (-%R @` E). Proof. -by split=> [/has_lbP [x /lb_ubN]|/has_ubP [x /ub_lbN]]; [|rewrite setNK]; - exists (- x). +by split=> [[x /lb_ubN] | [x /ub_lbN]]; [|rewrite setNK]; exists (- x). Qed. Lemma inf_lb E : has_lb E -> (lb E) (inf E). @@ -471,9 +434,8 @@ Qed. Lemma has_infPn E : nonempty E -> ~ has_inf E <-> (forall x, exists2 y, E y & y < x). Proof. -move=> nzE; split=> [/asboolPn|]; first rewrite (asbool_equiv_eq has_infP). - by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_lbPn. -by move/has_lbPn=> h /has_infP [_]. +move=> nzE; split=> [/asboolPn|/has_lbPn h [_] //]. +by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_lbPn. Qed. End InfTheory. @@ -498,13 +460,13 @@ Qed. Lemma sup_in_floor_set x : (floor_set x) (sup (floor_set x)). Proof. have /sup_adherent /(_ ltr01) [y Fy] := has_sup_floor_set x. -have /sup_upper_bound /(_ _ Fy) := has_sup_floor_set x. +have /sup_upper_bound /ubP /(_ _ Fy) := has_sup_floor_set x. rewrite le_eqVlt=> /orP[/eqP<-//| lt_yFx]. rewrite ltr_subl_addr -ltr_subl_addl => lt1_FxBy. pose e := sup (floor_set x) - y; have := has_sup_floor_set x. move/sup_adherent=> -/(_ e) []; first by rewrite subr_gt0. move=> z Fz; rewrite /e opprB addrCA subrr addr0 => lt_yz. -have /sup_upper_bound /(_ _ Fz) := has_sup_floor_set x. +have /sup_upper_bound /ubP /(_ _ Fz) := has_sup_floor_set x. rewrite -(ler_add2r (-y)) => /le_lt_trans /(_ lt1_FxBy). case/andP: Fy Fz lt_yz=> /RintP[yi -> _]. case/andP=> /RintP[zi -> _]; rewrite -rmorphB /= ltrz1 ltr_int. @@ -523,10 +485,11 @@ Lemma mem_rg1_floor (x : R) : (range1 (floor x)) x. Proof. rewrite /range1. have /andP[_ ->] /= := sup_in_floor_set x. -case: (pselect ((floor_set x) (floor x + 1))); last first. +have [|] := pselect ((floor_set x) (floor x + 1)); last first. rewrite /floor_set => /negP. by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_floor). -by move/sup_upper_bound=> -/(_ (has_sup_floor_set x)); rewrite ger_addl ler10. +move/ubP : (sup_upper_bound (has_sup_floor_set x)) => h/h. +by rewrite ger_addl ler10. Qed. Lemma floor_ler (x : R) : floor x <= x. @@ -599,7 +562,7 @@ Qed. Lemma has_sup_down (S : set R) : has_sup (down S) <-> has_sup S. Proof. -split=> /has_supP [nzS nzubS]; apply/has_supP. +split=> -[nzS nzubS]. case: nzS=> x /downP[y yS le_xy]; split; first by exists y. case: nzubS=> u /ubP ubS; exists u; apply/ubP=> z zS. by apply/ubS; apply/downP; exists z. @@ -613,33 +576,32 @@ Lemma le_sup (S1 S2 : set R) : -> sup S1 <= sup S2. Proof. move=> le_S12 nz_S1 hs_S2; have hs_S1: has_sup S1. - apply/has_supP; split=> //; case/has_supP: hs_S2=> _ [x ubx]. + split=> //; case: hs_S2=> _ [x ubx]. exists x; apply/ubP=> y /le_S12 /downP[z zS2 le_yz]. by apply/(le_trans le_yz); move/ubP: ubx; apply. rewrite leNgt -subr_gt0; apply/negP => lt_sup. case: (sup_adherent hs_S1 lt_sup)=> x /le_S12 xdS2. rewrite subKr => lt_S2x; case/downP: xdS2=> z zS2. -by move/(lt_le_trans lt_S2x); rewrite ltNge sup_upper_bound. +move/(lt_le_trans lt_S2x); rewrite ltNge. +by move/ubP: (sup_upper_bound hs_S2) => ->. Qed. Lemma sup_down (S : set R) : sup (down S) = sup S. Proof. -case: (pselect (has_sup S)); last first. - by move=> supNS; rewrite !sup_out // => /has_sup_down. -move=> supS; have supDS: has_sup (down S) by apply/has_sup_down. +have [supS|supNS] := pselect (has_sup S); last first. + by rewrite !sup_out // => /has_sup_down. +have supDS : has_sup (down S) by apply/has_sup_down. apply/eqP; rewrite eq_le !le_sup //. - by case/has_supP: supS => -[x xS] _; exists x; apply/le_down. + by case: supS => -[x xS] _; exists x; apply/le_down. rewrite downK; exact: le_down. - by case/has_supP: supS. + by case: supS. Qed. Lemma sup1 (c : R) : sup [set c] = c. Proof. -have hs : has_sup [set c]; first (apply/has_supP; split; exists c => //). -by move=> y <-. -apply/eqP; rewrite eq_le sup_upper_bound // andbT; apply/sup_le_ub. -by exists c. -by move=> y <-. +have hs : has_sup [set c] by split; [exists c | exact: has_ub_set1]. +apply/eqP; rewrite eq_le; move/ubP: (sup_upper_bound hs) => -> //. +by rewrite andbT; apply/sup_le_ub; [exists c | rewrite ub_set1]. Qed. Lemma inf1 (c : R) : inf [set c] = c. @@ -655,8 +617,8 @@ Lemma lt_sup_imfset {T : Type} (F : T -> R) l : exists2 x, l < F x & F x <= sup [set y | exists x, y = F x]. Proof. set P := [set y | _]; move=> hs; rewrite -subr_gt0. -case/(sup_adherent hs)=> _ [x ->]; rewrite subKr => lt_lFx. -by exists x => //; apply/sup_upper_bound => //; exists x. +case/(sup_adherent hs) => _[x ->]; rewrite subKr=> lt_lFx. +by exists x => //; move/ubP : (sup_upper_bound hs) => -> //; exists x. Qed. Lemma lt_inf_imfset {T : Type} (F : T -> R) l : @@ -666,7 +628,7 @@ Lemma lt_inf_imfset {T : Type} (F : T -> R) l : Proof. set P := [set y | _]; move=> hs; rewrite -subr_gt0. case/(inf_adherent hs)=> _ [x ->]; rewrite addrA [_ + l]addrC addrK. -by move=> ltFxl; exists x=> //; apply/inf_lower_bound => //; exists x. +by move=> ltFxl; exists x=> //; move/lbP : (inf_lower_bound hs) => -> //; exists x. Qed. End Sup. From 2eef8b5670541cc6dd4f105a6de10a2ea1183d6d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 25 May 2020 19:01:17 +0900 Subject: [PATCH 4/6] rebase sequences.v --- theories/sequences.v | 55 +++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 29 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index c14ef28f58..f767b7e5d0 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -347,56 +347,55 @@ Section sequences_R_lemmas. Variable R : realType. Lemma cvg_has_ub (u_ : R^o ^nat) : - cvg u_ -> has_ub (mem [set `|u_ n| | n in setT]). + cvg u_ -> has_ub [set `|u_ n| | n in setT]. Proof. -move=> /cvg_seq_bounded/pinfty_ex_gt0[M M_gt0 /= uM]; apply/has_ubP/nonemptyP. -by exists M; apply/ubP => x; rewrite inE => -[n _ <-{x}]; exact: uM. +move=> /cvg_seq_bounded/pinfty_ex_gt0[M M_gt0 /= uM]. +by exists M; apply/ubP => x -[n _ <-{x}]; exact: uM. Qed. (* TODO: move *) -Lemma has_ub_image_norm (S : set R) : - has_ub (mem (normr @` S)) -> has_ub (mem S). +Lemma has_ub_image_norm (S : set R) : has_ub (normr @` S) -> has_ub S. Proof. -case/has_ubP => M /ubP uM; apply/has_ubP; exists `|M|; apply/ubP => r. -rewrite !inE => rS. +case => M /ubP uM; exists `|M|; apply/ubP => r rS. rewrite (le_trans (real_ler_norm _)) ?num_real //. rewrite (le_trans (uM _ _)) ?real_ler_norm ?num_real //. -by rewrite !inE; exists r. +by exists r. Qed. -Lemma cvg_has_sup (u_ : R^o ^nat) : cvg u_ -> has_sup (mem (u_ @` setT)). +Lemma cvg_has_sup (u_ : R^o ^nat) : cvg u_ -> has_sup (u_ @` setT). Proof. move/cvg_has_ub; rewrite -/(_ @` _) -(image_comp u_ normr setT). -move=> /has_ub_image_norm uM; apply/has_supP; split => //. -by exists (u_ 0%N); rewrite !inE; exists 0%N. +move=> /has_ub_image_norm uM; split => //. +by exists (u_ 0%N), 0%N. Qed. -Lemma cvg_has_inf (u_ : R^o ^nat) : cvg u_ -> has_inf (mem (u_ @` setT)). +Lemma cvg_has_inf (u_ : R^o ^nat) : cvg u_ -> has_inf (u_ @` setT). Proof. -move/is_cvgN/cvg_has_sup; rewrite has_inf_supN; apply eq_has_sup => r /=. -rewrite !inE; apply/asbool_equiv_eq; split => /=. -by case=> n _ <- /= ; rewrite opprK; exists n. -by case=> n _ /eqP; rewrite -eqr_oppLR => /eqP <-; exists n. +move/is_cvgN/cvg_has_sup; rewrite has_inf_supN. +suff -> : (- u_) @` setT = -%R @` (u_ @` setT) by []. +rewrite predeqE => x; split. +by case=> n _ <-; exists (u_ n) => //; exists n. +by case=> y [] n _ <- <-; exists n. Qed. Lemma nondecreasing_cvg (u_ : (R^o) ^nat) (M : R) : nondecreasing_seq u_ -> (forall n, u_ n <= M) -> - u_ --> (sup (mem (u_ @` setT)) : R^o). + u_ --> (sup (u_ @` setT) : R^o). Proof. -move=> u_nd u_M; set S := mem _; set M0 := sup S. +move=> u_nd u_M; set S := _ @` _; set M0 := sup S. have supS : has_sup S. - apply/has_supP; split; first by exists (u_ 0%N); rewrite in_setE; exists 0%N. - by exists M; apply/ubP => x; rewrite in_setE => -[n _ <-{x}]. + split; first by exists (u_ 0%N), 0%N. + by exists M; apply/ubP => x -[n _ <-{x}]. 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). - rewrite in_setE => -[p _] <-{x} => /ltW M0u_p. - exists p; rewrite M0u_p /=; apply/sup_upper_bound => //. - by rewrite in_setE; exists p. + move=> -[p _] <-{x} => /ltW M0u_p. + exists p; rewrite M0u_p /=; have /ubP := sup_upper_bound supS. + by apply; exists p. near=> n; have pn : (p <= n)%N by near: n; apply: locally_infty_ge. rewrite distrC ler_norml ler_sub_addl (ler_trans M0u_p (u_nd _ _ pn)) /=. rewrite ler_subl_addr (@le_trans _ _ M0) ?ler_addr //. -by apply/sup_upper_bound => //; rewrite in_setE; exists n. +by have /ubP := sup_upper_bound supS; apply; exists n. Grab Existential Variables. all: end_near. Qed. Lemma nondecreasing_is_cvg (u_ : (R^o) ^nat) (M : R) : @@ -417,13 +416,11 @@ Qed. Lemma nonincreasing_cvg (u_ : (R^o) ^nat) (m : R) : nonincreasing_seq u_ -> (forall n, m <= u_ n) -> - u_ --> (inf (mem (u_ @` setT)) : R^o). + u_ --> (inf (u_ @` setT) : R^o). Proof. rewrite -nondecreasing_opp => /(@nondecreasing_cvg _ (- m)) u_sup mu_. -rewrite -[X in X --> _]opprK /inf (@eq_sup _ (mem ((-%R \o u_) @` setT))). - by apply: cvgN; apply u_sup => p; rewrite ler_oppl opprK. -move=> r; rewrite -[in X in _ = X](opprK r); apply asbool_equiv_eq. -by rewrite -(image_inj oppr_inj) image_comp. +rewrite -[X in X --> _]opprK /inf image_comp. +by apply: cvgN; apply u_sup => p; rewrite ler_oppl opprK. Qed. Lemma nonincreasing_is_cvg (u_ : (R^o) ^nat) (m : R) : From 413e0c32b4c44409b93406eee07529bb2f90a2ee Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 26 May 2020 06:02:33 +0900 Subject: [PATCH 5/6] add doc and lemmas about supremum --- theories/classical_sets.v | 20 ++++++++------- theories/ereal.v | 54 +++++++++++++++++++++++++++++++++++---- 2 files changed, 60 insertions(+), 14 deletions(-) diff --git a/theories/classical_sets.v b/theories/classical_sets.v index cb99b49110..5b52f26055 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -85,6 +85,11 @@ Require Import boolp. (* upper bound has a maximal element. We also proved an analogous version *) (* for preorders, where maximal is replaced with premaximal: t is *) (* premaximal if whenever t < s we also have s < t. *) +(* *) +(* * Upper and lower bounds: *) +(* ul, lb == upper bound and lower bound sets *) +(* supremum x0 E == supremum of E or x0 if E is empty *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -826,15 +831,14 @@ 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 := 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]. +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]. Lemma ubP E x : (forall y, E y -> (y <= x)%O) <-> ub E x. -Proof. by rewrite /ub; unlock. Qed. +Proof. by []. Qed. Lemma lbP E x : (forall y, E y -> (x <= y)%O) <-> lb E x. -Proof. by rewrite /lb; unlock. Qed. +Proof. by []. Qed. Lemma ub_set1 x y : ub [set x] y = (x <= y)%O. Proof. @@ -852,7 +856,7 @@ 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 := locked [set x | exists y, E y /\ (x <= y)%O]. +Definition down E : set T := [set x | exists y, E y /\ (x <= y)%O]. (* Real set supremum and infimum existence condition. *) Definition has_ub E := ub E !=set0. @@ -863,9 +867,7 @@ 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. +Proof. by split => [[y Ey xy]|[y [Ey xy]]]; [exists y| exists y]. Qed. Definition supremums E := ub E `&` lb (ub E). diff --git a/theories/ereal.v b/theories/ereal.v index d32e0ed72c..99a59013f2 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -5,7 +5,25 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import all_ssreflect all_algebra. -Require Import boolp classical_sets reals. +Require Import boolp classical_sets reals posnum. + +(******************************************************************************) +(* Extended real numbers *) +(* *) +(* Given a type R for numbers, {ereal R} is the type R extended with symbols *) +(* -oo and +oo (notation scope: %E), suitable to represent extended real *) +(* numbers. When R is a numDomainType, {ereal R} is equipped with a canonical *) +(* POrderType and operations for addition/opposite. When R is a *) +(* realDomainType, {ereal R} is equipped with a Canonical OrderType. *) +(* *) +(* r%:E == injects real numbers into {ereal R} *) +(* +%E, -%E == addition/opposite for extended reals *) +(* (\sum_(i in A) f i)%E == bigopg-like notation in scope %E *) +(* ereal_sup E == supremum of E *) +(* ereal_inf E == infimum of E *) +(* ereal_supremums_neq0 S == S has a supremum *) +(* *) +(******************************************************************************) Set Implicit Arguments. Unset Strict Implicit. @@ -91,7 +109,7 @@ Variable (R : countType). Definition ereal_countMixin := PcanCountMixin (@codeK R). Canonical ereal_countType := CountType {ereal R} ereal_countMixin. -End ERealCount. + End ERealCount. Section ERealOrder. Context {R : numDomainType}. @@ -339,7 +357,7 @@ End ERealArithTh_numDomainType. Section ERealArithTh_realDomainType. Context {R : realDomainType}. -Implicit Types x y a b : {ereal R}. +Implicit Types x y z a b : {ereal R}. Lemma sube_gt0 x y: (0%:E < y - x)%E = (x < y)%E. Proof. @@ -376,6 +394,12 @@ Qed. Lemma lee_add2r x a b : (a <= b)%E -> (a + x <= b + x)%E. Proof. rewrite addeC (addeC b); exact: lee_add2l. Qed. +Lemma lte_subl_addr x (r : R) z : (x - r%:E < z)%E = (x < z + r%:E)%E. +Proof. +move: x r z => [x| |] r [z| |] //=; rewrite ?lte_pinfty ?lte_ninfty //. +by rewrite !lte_fin ltr_subl_addr. +Qed. + End ERealArithTh_realDomainType. (* -------------------------------------------------------------------- *) @@ -496,13 +520,33 @@ Qed. Lemma ereal_inf_set0 : ereal_inf set0 = +oo. Proof. by rewrite /ereal_inf image_set0 ereal_sup_set0. Qed. -Lemma ereal_sup_ub S y (Sy : S y) : y <= ereal_sup S. +Lemma ereal_sup_ub S : ub S (ereal_sup S). Proof. -rewrite /ereal_sup /supremum. +move=> y Sy; rewrite /ereal_sup /supremum. case: pselect => /= [S0|/(_ (ex_intro S y Sy)) //]. case: xgetP => /=. by move=> x ->{x} -[] /ubP geS _; apply geS. by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). Qed. +Lemma ub_ereal_sup S M : ub S M -> (ereal_sup S <= M)%E. +Proof. +rewrite /ereal_sup /supremum; case: pselect => /= [|_ _]. +- move=> S0 SM; case: xgetP => [x ->{x} [_]| _] /=; first exact. + by rewrite lee_ninfty. +- by rewrite lee_ninfty. +Qed. + +Lemma ub_ereal_sup_adherent S (e : {posnum R}) (r : R) : + ereal_sup S = r%:E -> exists x, S x /\ (ereal_sup S - e%:num%:E < x)%E. +Proof. +move=> Sr. +have : ~ ub S (ereal_sup S - e%:num%:E)%E. + move/ub_ereal_sup; apply/negP. + by rewrite -ltNge Sr lte_subl_addr lte_fin ltr_addl. +move/asboolP; rewrite asbool_neg; case/existsp_asboolPn => /= x. +case/imply_classic => ? ?; exists x; split => //. +by rewrite ltNge; apply/negP. +Qed. + End ereal_supremum. From fb9adc720483018e31f1d07a3260fcc8944833a5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 2 Jun 2020 20:53:43 +0900 Subject: [PATCH 6/6] add changelog information --- CHANGELOG_UNRELEASED.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c1ee5bdc82..f908a9cfe0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,23 @@ ### Added +- in `boolp.v`, lemmas for classical reasoning `existsNP`, `existsP`, + `forallNP`, `forallP`, `imply_classic`, `orC`. +- in `classical_sets.v`, definitions for supremums: `ul`, `lb`, + `supremum` +- in `ereal.v`: + + technical lemmas `lee_ninfty_eq`, `lee_pinfty_eq`, `lte_subl_addr` + + lemmas about supremum: `ereal_supremums_neq0` + + definitions: + * `ereal_sup`, `ereal_inf` + + lemmas about `ereal_sup`: + * `ereal_sup_ub`, `ub_ereal_sup`, `ub_ereal_sup_adherent` + ### Changed +- in `reals.v`, `pred` replaced by `set` from `classical_sets.v` + + change propagated in many files + ### Renamed ### Removed