From 9df3f3f68b8c49af962445d0cac9b45d38c28823 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 11 Jul 2024 13:38:43 +0200 Subject: [PATCH] Tidy some proofs --- classical/mathcomp_extra.v | 52 ++++++++++++--------------- theories/altreals/realsum.v | 18 +++++----- theories/ereal.v | 10 +++--- theories/lebesgue_integral.v | 29 +++++++-------- theories/lebesgue_measure.v | 10 +++--- theories/lebesgue_stieltjes_measure.v | 4 +-- theories/normedtype.v | 5 +-- theories/real_interval.v | 10 +++--- theories/reals.v | 37 +++++++------------ theories/sequences.v | 8 ++--- theories/topology.v | 7 ++-- 11 files changed, 83 insertions(+), 107 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index c0fc66e95..ce3d24845 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -388,64 +388,56 @@ Context {R : archiDomainType}. Implicit Type x : R. Lemma ge_floor x : (Num.floor x)%:~R <= x. -Proof. by rewrite Num.Theory.ge_floor. Qed. +Proof. exact: Num.Theory.ge_floor. Qed. + +Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x). +Proof. exact: Num.Theory.floor_ge_int. Qed. + +Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z). +Proof. by rewrite ltNge floor_ge_int -ltNge. Qed. Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x). -Proof. by rewrite -Num.Theory.floor_ge_int. Qed. +Proof. by rewrite -floor_ge_int. Qed. Lemma floor_le0 x : x <= 0 -> Num.floor x <= 0. Proof. by move/Num.Theory.floor_le; rewrite Num.Theory.floor0. Qed. Lemma floor_lt0 x : x < 0 -> Num.floor x < 0. -Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _)). Qed. +Proof. by rewrite -floor_lt_int. Qed. Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R. -Proof. by rewrite Num.Theory.lt_succ_floor. Qed. +Proof. exact: Num.Theory.lt_succ_floor. Qed. Lemma floor_natz n : Num.floor (n%:R : R) = n%:~R :> int. -Proof. -by rewrite (@Num.Theory.floor_def _ _ n%:~R)// intr1 !mulrz_nat lexx/= ltr_nat addn1. -Qed. - -Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x). -Proof. by rewrite Num.Theory.floor_ge_int. Qed. +Proof. by rewrite (Num.Theory.intrKfloor n) intz. Qed. Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1). -Proof. -apply/idP/orP => [|[x0|/Num.Theory.floor_le r1]]; first rewrite neq_lt => /orP[x0|x0]. -- by left; apply: contra_lt x0; rewrite -floor_ge_int. -- by right; rewrite (le_trans _ (ge_floor _))// ler1z -gtz0_ge1. -- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int. -- by rewrite gt_eqF// (lt_le_trans _ r1)// Num.Theory.floor1. -Qed. - -Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z). -Proof. by rewrite ltNge Num.Theory.floor_ge_int// -ltNge. Qed. +Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed. Lemma ceil_ge x : x <= (Num.ceil x)%:~R. -Proof. by rewrite Num.Theory.le_ceil. Qed. +Proof. exact: Num.Theory.le_ceil. Qed. + +Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z). +Proof. exact: Num.Theory.ceil_le_int. Qed. + +Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x). +Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed. Lemma ceil_ge0 x : 0 <= x -> 0 <= Num.ceil x. Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed. Lemma ceil_gt0 x : 0 < x -> 0 < Num.ceil x. -Proof. by move=> ?; rewrite oppr_gt0 floor_lt0 // ltrNl oppr0. Qed. +Proof. by rewrite -ceil_lt_int. Qed. Lemma ceil_le0 x : x <= 0 -> Num.ceil x <= 0. -Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed. - -Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z). -Proof. by rewrite Num.Theory.ceil_le_int. Qed. - -Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x). -Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed. +Proof. by rewrite -ceil_ge_int. Qed. Lemma ceilN x : Num.ceil (- x) = - Num.floor x. Proof. by rewrite /Num.ceil opprK. Qed. Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R. Proof. -rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x. +rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x. by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl. by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor. Qed. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 886773498..cc88039f4 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -6,7 +6,7 @@ From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp.classical Require Import boolp. Require Import xfinmap ereal reals discrete realseq. -From mathcomp.classical Require Import classical_sets functions mathcomp_extra. +From mathcomp.classical Require Import classical_sets functions. Require Import topology. Set Implicit Arguments. @@ -15,6 +15,7 @@ Unset Printing Implicit Defensive. Unset SsrOldRewriteGoalsOrder. Import Order.TTheory GRing.Theory Num.Theory. +From mathcomp.classical Require Import mathcomp_extra. Local Open Scope fset_scope. Local Open Scope ring_scope. @@ -141,11 +142,9 @@ Proof. case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > 1 / p.+1%:~R]. set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}. move=> x; rewrite !inE => nz_fx. - pose j := `|Num.floor (1 / `|f x|)|%N; exists j; rewrite inE. - rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //. - rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z. - rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//. - by rewrite intr1 mathcomp_extra.lt_succ_floor. + pose j := `|Num.floor (`|f x|^-1)|%N; exists j; rewrite inE. + rewrite mul1r invf_plt ?unfold_in /= ?ltr0z ?normr_gt0 // /j -addn1 /=. + by rewrite PoszD gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0// lt_succ_floor. apply/(countable_sub le)/cunion_countable=> i /=. case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|]. by apply/finite_countable/finiteP; exists s => x /le_Eis. @@ -157,10 +156,9 @@ suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM. apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first. apply/ler_sum=> /= m _; apply/ltW. by have:= fsvalP m; rewrite in_fset => /le_sEi. -rewrite sumr_const -cardfE card_fseq undup_id // eq_si -mulr_natr -pmulrn. -rewrite mul1r natrM mulrCA mulVf ?mulr1 ?pnatr_eq0 //. -have /andP[_] := mem_rg1_floor M; rewrite -addn1. -by rewrite natrD /= mulr1n pmulrn -{1}[Num.floor _]gez0_abs // floor_ge0. +rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si. +rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//. +by rewrite pmulrn -addn1 PoszD gez0_abs ?floor_ge0// lt_succ_floor. Qed. End SummableCountable. diff --git a/theories/ereal.v b/theories/ereal.v index 5c537d399..414423e22 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -6,7 +6,7 @@ (* -------------------------------------------------------------------- *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import fsbigop cardinality set_interval. Require Import reals signed topology. Require Export constructive_ereal. @@ -55,6 +55,7 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Import numFieldTopology.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope ring_scope. @@ -1406,13 +1407,13 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs by rewrite Znat_def floor_ge0 le_max lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin. have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_max lexx. - apply; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor. + apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor. by rewrite natr1 mulrz_nat ler_nat. have /natrP[N Nfloor] : Num.floor (Num.max (- d)%R 0%R) \is a Num.nat. by rewrite Znat_def floor_ge0 le_max lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl. have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_max lexx. - apply; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor. + apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor. by rewrite natr1 mulrz_nat ler_nat. have /natrP[N Nfloor] : Num.floor d%:num^-1 \is a Num.nat. by rewrite Znat_def floor_ge0. @@ -1420,6 +1421,5 @@ exists N => // n leNn; apply: dP; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0. rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0. rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r. -rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor. -by rewrite !natr1 mulrz_nat ler_nat. +by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor !natr1 mulrz_nat ler_nat. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 9ca1e3de0..d8f29b968 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences real_interval. Require Import esum measure lebesgue_measure numfun realfun function_spaces. @@ -83,6 +83,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldTopology.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -1288,20 +1289,14 @@ Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic = Proof. rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. - rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N. - rewrite /= mem_index_iota; apply/andP; split. - rewrite -ltez_nat gez0_abs ?floor_ge0; last first. - by rewrite mulr_ge0// (le_trans _ nr). - apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)); last first. - by apply: floor_le; rewrite natrM natrX ler_pM2r. - by rewrite -floor_ge_int. - rewrite -ltz_nat gez0_abs; last first. - by rewrite floor_ge0 mulr_ge0// (le_trans _ nr). - rewrite -(@ltr_int R) (le_lt_trans (ge_floor _)) ?num_real//. - by rewrite PoszM intrM -natrX ltr_pM2r. + rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs ?floor_ge0; last first. + by rewrite mulr_ge0// (le_trans _ nr). + rewrite -floor_ge_int -floor_lt_int. + by rewrite !PoszM -!natrXE !rmorphM !rmorphXn /= ler_wpM2r ?ltr_pM2r. rewrite /= in_itv /=; apply/andP; split. - rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//. + rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) //. by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr). - rewrite ltr_pdivlMr// (lt_le_trans (mathcomp_extra.lt_succ_floor _))//. + rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//. rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (floor _))// floor_ge0. by rewrite mulr_ge0// (le_trans _ nr). - rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn]. @@ -1432,15 +1427,15 @@ rewrite notin_setE /B /setI /= => /not_andP[] // /negP. rewrite -ltNge => fxn _. have K : (`|floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N. rewrite -ltz_nat gez0_abs; last by rewrite floor_ge0 mulr_ge0// ltW. - rewrite -(@ltr_int R); rewrite (le_lt_trans (ge_floor _)) ?num_real// PoszM intrM. + rewrite -(@ltr_int R); rewrite (le_lt_trans (ge_floor _))// PoszM intrM. by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin). have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K). rewrite implyTb indicE mem_set ?mulr1; last first. rewrite /A K /= inE; split=> //=; exists (fine (f x)); last by rewrite fineK. rewrite in_itv /=; apply/andP; split. - rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//. + rewrite ler_pdivrMr// (le_trans _ (ge_floor _))//. by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW. - rewrite ltr_pdivlMr// (lt_le_trans (mathcomp_extra.lt_succ_floor _))//. + rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//. rewrite -[in leRHS]natr1 -intr1 lerD2r// -{1}(@gez0_abs (floor _))//. by rewrite floor_ge0// mulr_ge0// ltW. rewrite mulf_eq0// -exprVn; apply/negP; rewrite negb_or expf_neq0//= andbT. @@ -1543,7 +1538,7 @@ have : fine (f x) < n%:R. rewrite -(@ler_nat R); apply: lt_le_trans. rewrite -natr1 (_ : `| _ |%:R = (floor (fine (f x)))%:~R); last first. by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0. - by rewrite intr1 mathcomp_extra.lt_succ_floor. + by rewrite intr1 lt_succ_floor. rewrite -lte_fin (fineK fxfin) => fxn. have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn. by have := Hm _ mn; rewrite approx_nx0. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e5fb6d24f..4d184c1bc 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1155,10 +1155,10 @@ rewrite [X in measurable X](_ : _ = exact: emeasurable_fun_infty_c]. rewrite predeqE => t; split => [/= [Dt ft]|]. have [ft0|ft0] := leP 0%R (fine (f t)). - exists `|(ceil (fine (f t)))%real|%N => //=; split => //; split. + exists `|ceil (fine (f t))|%N => //=; split => //; split. by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge. - exists `|(floor (fine (f t)))%real|%N => //=; split => //; split. + exists `|floor (fine (f t))|%N => //=; split => //; split. rewrite natr_absz ltr0_norm ?floor_lt0// EFinN. by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real. by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). @@ -1403,7 +1403,7 @@ Lemma eset1Ny : Proof. rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr. move=> [r|/(_ O Logic.I)|]//. -move=> /(_ `|(floor r)%real|%N Logic.I); rewrite /= in_itv/= ltNge. +move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge. rewrite lee_fin; have [r0|r0] := leP 0%R r. by rewrite (le_trans _ r0) // lerNl oppr0 ler0n. rewrite lerNl -abszN natr_absz gtr0_norm; last first. @@ -1414,7 +1414,7 @@ Qed. Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). Proof. rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. -move=> [r| |/(_ O Logic.I)] // /(_ `|(ceil r)%real|%N Logic.I); rewrite /= in_itv /=. +move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. rewrite andbT lte_fin ltNge. have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). by rewrite natr_absz gtr0_norm // ?ceil_ge// ceil_gt0. @@ -2400,7 +2400,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <= by apply: bigcup_measurable => *; exact: measurable_closure. have finite_set_F i : finite_set (F i). apply: contrapT. - pose M := `|(ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R)))%real|.+1. + pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1. move/(infinite_set_fset M) => [/= C] CsubFi McardC. have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <= mu (\bigcup_(j in [set` C]) closure (B j)). diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index f6647899a..3cd2d3355 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -482,9 +482,9 @@ Lemma wlength_sigma_finite (f : R -> R) : Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. - exists `|((floor `|x|%R)%real + 1)%R|%N; rewrite //= in_itv/=. + exists `|(floor `|x| + 1)%R|%N; rewrite //= in_itv/=. rewrite !natr_absz intr_norm intrD. - suff: `|x| < `|(floor `|x|)%real%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. + suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. rewrite [ltRHS]ger0_norm//. by rewrite intr1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm. by rewrite addr_ge0// ler0z floor_ge0. diff --git a/theories/normedtype.v b/theories/normedtype.v index 64ed061c7..989a456dd 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import rat interval zmodp vector fieldext falgebra. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval Rstruct. Require Import ereal reals signed topology prodnormedzmodule function_spaces. @@ -146,6 +146,7 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldTopology.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -5779,7 +5780,7 @@ rewrite ler_pdivlMr// mulrC -ler_pdivlMr//. have [f0|f0] := eqVneq 0 f. by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0. rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym. -by rewrite natr_absz// ger0_norm// mathcomp_extra.ge_floor. +by rewrite natr_absz// ger0_norm// ge_floor. Qed. Lemma cover_vitali_collection_partition : diff --git a/theories/real_interval.v b/theories/real_interval.v index ce860e82a..a6d27e349 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import fingroup perm rat archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Export set_interval. From HB Require Import structures. Require Import reals ereal signed topology normedtype sequences. @@ -14,6 +14,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -176,8 +177,7 @@ rewrite predeqE => y; split=> /=; last first. rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=. rewrite in_itv /= xy /=. have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_pwDr. -rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW//. -by rewrite intr1 mathcomp_extra.lt_succ_floor. +by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// intr1 lt_succ_floor. Qed. Lemma itv_o_inftyEbigcup x : @@ -344,7 +344,7 @@ move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first. rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1|%N => //. rewrite /E/= -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW. rewrite fxE gxE lee_fin -[leRHS]invrK lef_pV2//. -- by rewrite intr1 ltW// mathcomp_extra.lt_succ_floor. +- by rewrite intr1 ltW// lt_succ_floor. - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW. - by rewrite posrE invr_gt0. Qed. @@ -367,7 +367,7 @@ apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//. have := rx `|floor e^-1|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE. rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. -by rewrite intr1 mathcomp_extra.lt_succ_floor. +by rewrite intr1 lt_succ_floor. Qed. Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : diff --git a/theories/reals.v b/theories/reals.v index 92d228f78..3e64c8148 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -39,9 +39,8 @@ (******************************************************************************) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. -From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect all_algebra archimedean. +From mathcomp Require Import boolp classical_sets set_interval. Require Import Setoid. @@ -54,6 +53,7 @@ Unset Printing Implicit Defensive. Unset SsrOldRewriteGoalsOrder. Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory. +From mathcomp Require Import mathcomp_extra. (* -------------------------------------------------------------------- *) Delimit Scope real_scope with real. @@ -465,20 +465,17 @@ Lemma RfloorE x : Rfloor x = (floor x)%:~R. Proof. by []. Qed. Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x. -Proof. -rewrite /range1 /mkset intr1 mathcomp_extra.lt_succ_floor andbT. -by rewrite mathcomp_extra.ge_floor. -Qed. +Proof. by rewrite /range1 /mkset intr1 ge_floor lt_succ_floor. Qed. Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. -Proof. by rewrite /Rfloor; exact: mem_rg1_floor. Qed. +Proof. exact: mem_rg1_floor. Qed. Lemma Rfloor_le x : Rfloor x <= x. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. #[deprecated(since="mathcomp-analysis 1.3.0", note="use `ge_floor` instead")] Lemma floor_le x : (floor x)%:~R <= x. -Proof. by rewrite mathcomp_extra.ge_floor. Qed. +Proof. by rewrite ge_floor. Qed. Lemma lt_succ_Rfloor x : x < Rfloor x + 1. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. @@ -499,8 +496,7 @@ Proof. by rewrite /range1/mkset lexx /= ltrDl ltr01. Qed. Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x. Proof. split=> [<-|h]; first exact/mem_rg1_Rfloor. -apply/eqP; rewrite RfloorE eqr_int; apply/eqP/(@range1z_inj x) => //. -by rewrite /range1/mkset -RfloorE mem_rg1_Rfloor. +by congr intmul; apply/floor_def; rewrite -intr1. Qed. Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R. @@ -511,20 +507,13 @@ Lemma Rfloor0 : Rfloor 0 = 0 :> R. Proof. by rewrite /Rfloor floor0. Qed. Lemma Rfloor1 : Rfloor 1 = 1 :> R. Proof. by rewrite /Rfloor floor1. Qed. Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}. -Proof. -move=> x y le_xy; case: lerP=> //=; rewrite -Rint_ler_addr1 ?isint_Rfloor //. -move/(lt_le_trans (lt_succ_Rfloor y))/lt_le_trans/(_ (Rfloor_le x)). -by rewrite ltNge le_xy. -Qed. +Proof. by move=> x y /Num.Theory.floor_le; rewrite ler_int. Qed. Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x). -Proof. -apply/idP/idP; last by move/le_trans => /(_ _ (Rfloor_le x)). -by move/le_Rfloor; apply le_trans; rewrite Rfloor_natz. -Qed. +Proof. by rewrite ler_int floor_ge_int. Qed. Lemma Rfloor_lt_int x (z : int) : (x < z%:~R) = (Rfloor x < z%:~R). -Proof. by rewrite ltNge Rfloor_ge_int -ltNge. Qed. +Proof. by rewrite ltr_int floor_lt_int. Qed. Lemma Rfloor_le0 x : x <= 0 -> Rfloor x <= 0. Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed. @@ -534,7 +523,7 @@ Proof. by move=> x0; rewrite (le_lt_trans _ x0) // Rfloor_le. Qed. #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.floor_le` instead")] Lemma le_floor : {homo @Num.floor R : x y / x <= y}. -Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed. +Proof. exact: Num.Theory.floor_le. Qed. Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x. Proof. @@ -542,8 +531,8 @@ move=> yx; exists `|floor (x - y)^-1|%N. rewrite -ltrBrDl -{2}(invrK (x - y)%R) ltf_pV2 ?qualifE/= ?ltr0n//. by rewrite invr_gt0 subr_gt0. rewrite -natr1 natr_absz ger0_norm. - by rewrite -mathcomp_extra.floor_ge_int// invr_ge0 subr_ge0 ltW. -by rewrite intr1 mathcomp_extra.lt_succ_floor. + by rewrite -floor_ge_int// invr_ge0 subr_ge0 ltW. +by rewrite intr1 lt_succ_floor. Qed. End FloorTheory. diff --git a/theories/sequences.v b/theories/sequences.v index da6077f95..0d26a3acf 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat archimedean. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import set_interval. Require Import reals ereal signed topology normedtype landau. @@ -92,6 +92,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldNormedType.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -1274,9 +1275,8 @@ Proof. rewrite /series; near \oo => N; have xN : x < N%:R; last first. rewrite -(@is_cvg_series_restrict N.+1). by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup. -near: N; exists (absz (floor x)).+1 => // m; rewrite /mkset -(@ler_nat R). -move/lt_le_trans => -> //. -rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor x))//. +near: N; exists `|floor x|.+1 => // m; rewrite /mkset -(@ler_nat R). +move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x))//. by rewrite -intr1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW. Unshelve. all: by end_near. Qed. diff --git a/theories/topology.v b/theories/topology.v index 59039eebc..565e0721e 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality mathcomp_extra fsbigop. +From mathcomp Require Import cardinality fsbigop. Require Import reals signed. (**md**************************************************************************) @@ -447,6 +447,7 @@ Unset Printing Implicit Defensive. Obligation Tactic := idtac. Import Order.TTheory GRing.Theory Num.Theory. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -4991,8 +4992,8 @@ move=> E; rewrite -entourage_ballE => -[e e0 subE]. exists `|Num.floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball. rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1. rewrite natr_absz ger0_norm; last first. - by rewrite -mathcomp_extra.floor_ge_int ?invr_ge0// ltW. -by rewrite intr1 ltW// mathcomp_extra.lt_succ_floor. + by rewrite -floor_ge_int ?invr_ge0// ltW. +by rewrite intr1 ltW// lt_succ_floor. Qed. (** Specific pseudoMetric spaces *)