From 2eacae76e6f805636b966874ae5400d959c65c42 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 11 Apr 2025 11:59:20 +0200 Subject: [PATCH 1/2] Cleanup --- classical/unstable.v | 2 +- experimental_reals/distr.v | 4 ++-- experimental_reals/realseq.v | 9 ++++----- experimental_reals/realsum.v | 3 +-- reals/reals.v | 6 ++---- 5 files changed, 10 insertions(+), 14 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 563dcb9891..3981d02280 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -65,7 +65,7 @@ Proof. apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//. case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1. by rewrite addrCA addrK. -by rewrite addrCA addrAC subrr add0r. +by rewrite addrC subrKA. Qed. Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R. diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 0ad57d5412..d9de9c917c 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -335,7 +335,7 @@ Definition mflip (xt : R) := Lemma isd_mflip xt : isdistr (mflip xt). Proof. apply/isdistr_finP; split=> [b|]. + by case: b; rewrite ?subr_ge0 cp01_clamp. -+ by rewrite /index_enum !unlock /= addr0 addrCA subrr addr0. ++ by rewrite /index_enum !unlock /= addr0 addrC subrK. Qed. Definition dflip (xt : R) := locked (mkdistr (isd_mflip xt)). @@ -1133,7 +1133,7 @@ Qed. Lemma pr_and A B mu : \P_[mu] [predI A & B] = \P_[mu] A + \P_[mu] B - \P_[mu] [predU A & B]. -Proof. by rewrite pr_or opprB addrCA subrr addr0. Qed. +Proof. by rewrite pr_or subKr. Qed. Lemma ler_pr_or A B mu : \P_[mu] [predU A & B] <= \P_[mu] A + \P_[mu] B. diff --git a/experimental_reals/realseq.v b/experimental_reals/realseq.v index f8d1d909e1..c9150c5966 100644 --- a/experimental_reals/realseq.v +++ b/experimental_reals/realseq.v @@ -122,7 +122,7 @@ have gt0_e: 0 < e by rewrite subr_gt0. move=> x y; rewrite !inE/= /eclamp pmulr_rle0 // invr_le0. rewrite lern0 /= !ltr_distl => /andP[_ lt1] /andP[lt2 _]. apply/(lt_trans lt1)/(le_lt_trans _ lt2). -by rewrite lerBrDl addrCA -splitr /e addrCA subrr addr0. +by rewrite lerBrDl addrCA -splitr /e addrC subrK. Qed. Lemma separable {R : realType} (l1 l2 : \bar R) : @@ -303,9 +303,8 @@ Lemma ncvgM u v lu lv : ncvg u lu%:E -> ncvg v lv%:E -> Proof. move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S. have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)). - move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl. - rewrite !addrA -[LHS]add0r; congr (_ + _); rewrite mulrDr. - by rewrite !(mulrN, mulNr) (addrCA (lu * lv)) subrr addr0 subrr. + move=> n; rewrite {}/a {}/b /=. + by rewrite addrC mulrBr addrAC subrK addrC mulrBl subrK. apply/(ncvg_eq eq); rewrite -[X in X%:E]addr0; apply/ncvgD. by apply/ncvgC. rewrite -[X in X%:E]addr0; apply/ncvgD. + apply/ncvgMr; first rewrite -[X in X%:E](subrr lv). @@ -388,7 +387,7 @@ case: l1 l2 => [l1||] [l2||] //=; first last. move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)). case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //. rewrite ltr_distl => /andP[] /(le_lt_trans _) h _; apply: h. -by rewrite {cv}/e opprB addrCA subrr addr0. +by rewrite {cv}/e subKr. Qed. Lemma ncvg_lt (u : nat -> R) (l1 l2 : \bar R) : diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v index 6c09eb180f..8a7358d9ea 100644 --- a/experimental_reals/realsum.v +++ b/experimental_reals/realsum.v @@ -465,8 +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 ge0_e (summable_sup smS)) => y. -case=> /= J ->; rewrite /e /psum (asboolT smS). -rewrite opprB addrCA subrr addr0 => lt_xSJ. +case=> /= J ->; rewrite /e /psum (asboolT smS) subKr => 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. rewrite (eq_bigr (S \o val)) => /= [j _|]; first by rewrite ger0_norm. diff --git a/reals/reals.v b/reals/reals.v index 601ad4fe7c..974c5d10ad 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -281,8 +281,7 @@ Qed. Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x. Proof. 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 Dz: 2%:R * z = x + y by rewrite mulrC divfK// pnatr_eq0. have ubE : has_sup E by split => //; exists x. have [/downP [t Et lezt] | leyz] := sup_total z ubE. rewrite -(lerD2l x) -Dz -mulr2n -[leRHS]mulr_natl. @@ -334,8 +333,7 @@ have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n. have [r Ar supBr] := sup_adherent e2pos supA. have [s Bs supAs] := sup_adherent e2pos supB. have := ltrD supBr supAs. -rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA. -rewrite subrr add0r; apply/negP; rewrite -leNgt. +rewrite -addrACA -opprD -splitr subKr; apply/negP; rewrite -leNgt. by apply: sup_upper_bound => //; exists r => //; exists s. Qed. From 2cd6603752eb7bdbe8301bbe0f4eb9094fbc82cd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 19 May 2025 23:29:10 +0900 Subject: [PATCH 2/2] cleaning in ereal.v --- classical/unstable.v | 2 +- theories/derive.v | 4 +- theories/ereal.v | 99 +++++++++++++++++--------------------------- 3 files changed, 42 insertions(+), 63 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 3981d02280..50b3d4605d 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -65,7 +65,7 @@ Proof. apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//. case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1. by rewrite addrCA addrK. -by rewrite addrC subrKA. +by rewrite (addrC (x + y)) subrKA. Qed. Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R. diff --git a/theories/derive.v b/theories/derive.v index 4669920fdd..db9062fc37 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -325,7 +325,7 @@ rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD. rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0]. rewrite /ball_ /= => eX. apply/nbhs_ballP. - by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0. + by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0. rewrite /g2. have [->|v0] := eqVneq v 0. rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. @@ -340,7 +340,7 @@ rewrite ltr_pdivlMr ?normr_gt0 // => jvi j0. rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //. have /Hi/le_lt_trans -> // : ball 0 i (j *: v). by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ. -rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVr ?unitfE ?gt_eqF //. +rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVf ?gt_eqF//. rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first. by rewrite pmulr_rgt0 // normr_gt0. rewrite normrZ mulrC -mulrA. diff --git a/theories/ereal.v b/theories/ereal.v index 842176faeb..57d721ac28 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -399,7 +399,7 @@ have sSoo : supremums S +oo. by move=> /= y /(_ _ Spoo); rewrite leye_eq => /eqP ->. case: xgetP. by move=> _ -> sSxget; move: (is_subset1_supremums sSoo sSxget). -by move/(_ +oo) => gSoo; exfalso; exact: gSoo. +by move=> /(_ +oo); exact: contra_notP. Qed. Definition ereal_sup S := supremum -oo S. @@ -1175,15 +1175,13 @@ Qed. Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) : let e' := (r - fine (expand (contract r%:E - e%:num)))%R in ball r e' r' -> (r' < r)%R -> - (`|contract r%:E - (e)%:num| < 1)%R -> + (`|contract r%:E - e%:num| < 1)%R -> ereal_ball r%:E e%:num r'%:E. Proof. move=> e' re'r' rr' X; rewrite /ereal_ball. rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//. -move: re'r'. -rewrite /ball /= gtr0_norm // ?subr_gt0// /e'. -rewrite -ltrBlDl addrAC subrr add0r ltrNl opprK -lte_fin. -rewrite fine_expand // lt_expandLR ?inE ?ltW//. +move: re'r'; rewrite /ball /= gtr0_norm ?subr_gt0// /e'. +rewrite ltrD2l ltrN2 -lte_fin fine_expand// lt_expandLR ?inE ?ltW//. by rewrite ltrBlDl addrC -ltrBlDl. Qed. @@ -1318,12 +1316,12 @@ Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) : ereal_ball r%:E e%:num `<=` A -> nbhs r%:E A. Proof. move=> reA. -have [|reN1] := boolP (contract r%:E - e%:num == -1)%R. +have [/eqP|reN1] := eqVneq (contract r%:E - e%:num)%R (-1)%R. rewrite subr_eq addrC => /eqP reN1. - have [re1|] := boolP (contract r%:E + e%:num == 1)%R. - move/eqP : reN1; rewrite -(eqP re1) opprD addrCA subrr addr0 -subr_eq0. - rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0]. - move: re1; rewrite r0 contract0 add0r => /eqP e1. + have [re1|] := eqVneq (contract r%:E + e%:num)%R 1%R. + move/eqP : reN1; rewrite -re1 opprD addrC subrK -subr_eq0 opprK. + rewrite -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0]. + move: re1; rewrite r0 contract0 add0r => e1. apply/nbhs_ballP; exists 1%R => //= r'; rewrite /ball /= sub0r normrN => r'1. apply: reA. by rewrite /ereal_ball r0 contract0 sub0r normrN e1 contract_lt1. @@ -1338,10 +1336,9 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R. have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E). apply: contract_ereal_ball_fin_le; last exact/ltW. by rewrite -lee_fin -(contractK r%:E) -(contractK r'%:E) le_expand. - apply: contract_ereal_ball_fin_lt; last first. - by rewrite reN1 addrAC subrr add0r. + apply: contract_ereal_ball_fin_lt; last by rewrite reN1 lerBlDl. rewrite -lte_fin -(contractK r%:E) -(contractK r'%:E). - by rewrite lt_expand // inE; exact: contract_le1. + by rewrite lt_expand // inE contract_le1. exact: contract_ereal_ball_pinfty. have : nbhs r%:E (setT `\ -oo) by apply/nbhs_ballP; exists 1%R => /=. move=> /nbhs_ballP[_/posnumP[e']] /=; rewrite /ball /= => h. @@ -1351,9 +1348,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. by apply: (@nbhs_fin_out_above _ e) => //; rewrite re1. move: re1; rewrite neq_lt => /orP[re1|re1]. have ? : (`|contract r%:E - e%:num| < 1)%R. - rewrite ltr_norml reN1 andTb ltrBlDl. + rewrite ltr_norml reN1/= -/(contract _%:E) ltrBlDl. rewrite (@lt_le_trans _ _ 1%R) // ?lerDr//. - by case/ltr_normlP : (contract_lt1 r). + by rewrite (le_lt_trans (ler_norm _))// contract_lt1. have ? : (`|contract r%:E + e%:num| < 1)%R. rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_ltD //. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. @@ -1372,10 +1369,9 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1]. move=> rr'; apply: ball_ereal_ball_fin_le => //. by apply: le_ball re'r'; rewrite ge_min lexx orbT. move: re'r'; rewrite /ball /= lt_min => /andP[]. - rewrite gtr0_norm ?subr_gt0 // -ltrBlDl addrAC subrr add0r ltrNl. - rewrite opprK -lte_fin fine_expand // => r'e'r _. + rewrite gtr0_norm ?subr_gt0// ltrD2l ltrN2 -lte_fin fine_expand// => re'r _. exact: expand_ereal_ball_fin_lt. - by apply :(@nbhs_fin_out_above _ e) => //; rewrite ltW. + by apply: (@nbhs_fin_out_above _ e) => //; rewrite ltW. have [re1|re1] := ltrP 1 (contract r%:E + e%:num). exact: (@nbhs_fin_out_above_below _ e). move: re1; rewrite le_eqVlt => /orP[re1|re1]. @@ -1428,11 +1424,10 @@ rewrite predeq2E => x A; split. have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R. move: re'r'; rewrite /e' lt_min => /andP[+ _]. rewrite /e' ltrBrDl addrC -ltrBrDl => /lt_le_trans. - by apply; rewrite opprB addrCA subrr addr0. + by apply; rewrite opprB addrC subrK. rewrite -lt_expandRL ?inE ?contract_le1 // !contractK lte_fin. rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT. - rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0. - by rewrite -lee_fin -le_contract. + by rewrite (@lt_le_trans _ _ 0%R)// subr_ge0 -lee_fin -le_contract. apply: reA; rewrite /ball /= ltr_norml//. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. @@ -1449,26 +1444,20 @@ rewrite predeq2E => x A; split. have [cr0|cr0] := lerP 0 (contract r%:E). move: re'2; rewrite ler0_norm; last first. by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E). - rewrite opprB ltrBrDl addrCA subrr addr0 => h. - exfalso. - move: h; apply/negP; rewrite -leNgt. - by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)). + rewrite opprB ltrBrDl addrC subrK ltNge; apply: contraNP => _. + by rewrite (le_trans (ler_norm _))// contract_le1. move: re'2; rewrite ler0_norm; last first. by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E). - rewrite opprB ltrBrDl addrCA subrr addr0 => h. - exfalso. - move: h; apply/negP; rewrite -leNgt. - by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)). + rewrite opprB ltrBrDl addrC subrK ltNge; apply: contraNP => _. + by rewrite (le_trans (ler_norm _))// contract_le1. * move=> /xsectionP/=; rewrite /ereal_ball [contract -oo]/= opprK. rewrite lt_min => /andP[re'1 _]. move: re'1. rewrite ger0_norm; last first. rewrite addrC -lerBlDl add0r. by move: (contract_le1 r%:E); rewrite ler_norml => /andP[]. - rewrite ltrD2l => h. - exfalso. - move: h; apply/negP; rewrite -leNgt -lerNl. - by move: (contract_le1 (r%:E - e%:num%:E)); rewrite ler_norml => /andP[]. + rewrite ltrD2l ltNge; apply: contraNP => _. + by rewrite lerNl lerNnormlW// contract_le1. + exists (diag (1 - contract M%:E))%R; rewrite /diag. exists (1 - contract M%:E)%R => //=. by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm. @@ -1480,41 +1469,31 @@ rewrite predeq2E => x A; split. rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr subr_gt0 in rM1. by rewrite -lte_fin -lt_contract. * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA. - * rewrite /ereal_ball /= opprK => h {MA}. - exfalso. - move: h; apply/negP. - rewrite -leNgt [in leRHS]ger0_norm // lerBlDr. - rewrite -/(contract M%:E) addrC -lerBlDr opprD addrA subrr sub0r. - by move: (contract_le1 M%:E); rewrite ler_norml => /andP[]. + * rewrite /ereal_ball /= opprK ltNge; apply: contraNP => _. + rewrite [in leRHS]ger0_norm // lerD2l. + by rewrite -/(contract M%:E) lerNl lerNnormlW// contract_le1. + exists (diag (1 + contract M%:E)%R); rewrite /diag. exists (1 + contract M%:E)%R => //=. - rewrite -ltrBlDl sub0r. - by move: (contract_lt1 M); rewrite ltr_norml => /andP[]. + by rewrite -/(contract M%:E) -ltrBlDl sub0r ltrNnormlW// contract_lt1. case=> [r| |] /xsectionP/=. * rewrite /ereal_ball => /= rM1. apply: MA; rewrite lte_fin. rewrite ler0_norm in rM1; last first. - rewrite lerBlDl addr0 ltW //. - by move: (contract_lt1 r); rewrite ltr_norml => /andP[]. - rewrite opprB opprK -ltrBlDl addrK in rM1. - by rewrite -lte_fin -lt_contract. - * rewrite /ereal_ball /= -opprD normrN => h {MA}. - exfalso. - move: h; apply/negP. - rewrite -leNgt [in leRHS]ger0_norm// -lerBlDr addrAC. - rewrite subrr add0r -/(contract M%:E). - by rewrite (le_trans _ (ltW (contract_lt1 M))) // ler_norm. - * rewrite /ereal_ball /= => _; exact: MA. + by rewrite subr_le0 -/(contract r%:E) lerNnormlW// contract_le1. + move: rM1; rewrite opprB opprK -ltrBlDl addrK. + by rewrite -!/(contract _%:E) lt_contract lte_fin. + * rewrite /ereal_ball/= -opprD normrN ger0_norm// ltrD2l. + by rewrite -/(contract M%:E) ltNge (le_trans (ler_norm _))// contract_le1. + * by rewrite /ereal_ball /= => _; exact: MA. - case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA]] //=. + by apply: (@nbhs_fin_inbound _ e) => ? ?; exact/sEA/xsectionP/reA. - + have [|] := boolP (e%:num <= 1)%R. - by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/xsectionP/reA. - by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/xsectionP/reA. - + have [|] := boolP (e%:num <= 1)%R. - move/nbhs_oo_down_e1; apply => ? ?; apply: sEA. - by rewrite /xsection/= inE; exact: reA. - by rewrite -ltNge =>/nbhs_oo_down_1e; apply => ? ?; exact/sEA/xsectionP/reA. + + have [|] := lerP e%:num 1%R. + * by move/nbhs_oo_up_e1; apply => x ex; exact/sEA/xsectionP/reA. + * by move/nbhs_oo_up_1e; apply => x ex; exact/sEA/xsectionP/reA. + + have [|] := lerP e%:num 1%R. + * by move/nbhs_oo_down_e1; apply => x ex; exact/sEA/xsectionP/reA. + * by move/nbhs_oo_down_1e; apply => x ex; exact/sEA/xsectionP/reA. Qed. HB.instance Definition _ := Nbhs_isPseudoMetric.Build R (\bar R)