fixes #330

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,14 @@
 
 ### Added
 
+- in `reals.v`:
+  + lemma `mem_rg1_floor`
+
 ### Changed
 
+- in `reals.v`:
+  + definitions `Rceil`, `ceil`, `Rfloor`, `floor`
+
 ### Renamed
 
 - in `constructive_ereal.v`:

theories/altreals/realsum.v

@@ -145,8 +145,7 @@ set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >
   pose j := `|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 -RfloorE; apply lt_succ_Rfloor.
+  by rewrite 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.
@@ -160,9 +159,10 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
   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_Rfloor M; rewrite RfloorE -addn1.
+have /andP[_] := mem_rg1_floor M; rewrite -addn1.
 by rewrite natrD /= mulr1n pmulrn -{1}[floor _]gez0_abs // floor_ge0.
 Qed.
+
 End SummableCountable.
 
 (* -------------------------------------------------------------------- *)

theories/lebesgue_integral.v

@@ -1293,7 +1293,7 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
         by rewrite mulr_ge0// (le_trans _ nr).
       apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first.
         by apply: le_floor; rewrite natrM natrX ler_pM2r.
-      by rewrite floor_natz intz.
+      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 (reals.floor_le _))//.

theories/lebesgue_stieltjes_measure.v

@@ -481,11 +481,11 @@ Proof.
 exists (fun k => `](- k%:R), k%:R]%classic).
   apply/esym; rewrite -subTset => /= x _ /=.
   exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=.
-  rewrite !natr_absz intr_norm intrD -RfloorE.
-  suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->].
+  rewrite !natr_absz intr_norm intrD.
+  suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
   rewrite [ltRHS]ger0_norm//.
-    by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm.
-  by rewrite addr_ge0// -Rfloor0 le_Rfloor.
+    by rewrite (le_lt_trans _ (lt_succ_floor _))// ?ler_norm.
+  by rewrite addr_ge0// ler0z floor_ge0.
 move=> k; split => //; rewrite wlength_itv /= -EFinB.
 by case: ifP; rewrite ltey.
 Qed.

theories/reals.v

@@ -244,15 +244,15 @@ Variable R : realType.
 Implicit Types x y : R.
 Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)].
 
-Definition Rfloor x : R := sup (floor_set x).
+Definition floor x : int := Num.floor x.
 
-Definition floor x : int := Rtoint (Rfloor x).
+Definition Rfloor x : R := (floor x)%:~R.
 
 Definition range1 (x : R) := [set y | x <= y < x + 1].
 
-Definition Rceil x := - Rfloor (- x).
+Definition ceil x := Num.ceil x.
 
-Definition ceil x := - floor (- x).
+Definition Rceil x : R := (ceil x)%:~R.
 
 End RealDerivedOps.
 
@@ -470,27 +470,29 @@ by rewrite absz_eq0 subr_eq0 eq_sym (negbTE ne_yz).
 Qed.
 
 Lemma isint_Rfloor x : Rfloor x \is a Rint.
-Proof. by case/andP: (sup_in_floor_set x). Qed.
+Proof. by rewrite inE; exists (floor x). Qed.
 
 Lemma RfloorE x : Rfloor x = (floor x)%:~R.
-Proof. by rewrite /floor RtointK ?isint_Rfloor. Qed.
+Proof. by []. Qed.
 
-Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
+Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x.
 Proof.
 rewrite /range1/mkset.
-have /andP[_ ->] /= := sup_in_floor_set x.
-have [|] := pselect ((floor_set x) (Rfloor x + 1)); last first.
-  rewrite /floor_set => /negP.
-  by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_Rfloor).
-move/ubP : (sup_upper_bound (has_sup_floor_set x)) => h/h.
-by rewrite gerDl ler10.
+rewrite [X in _ + X](_ : 1 = 1%:~R)// -intrD lt_succ_floor ?andbT ?num_real//.
+by rewrite ge_floor// num_real.
+Qed.
+
+Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
+Proof.
+rewrite /range1 /mkset [X in _ + X](_ : 1 = 1%:~R)// -intrD.
+by rewrite lt_succ_floor ?num_real// andbT ge_floor// num_real.
 Qed.
 
 Lemma Rfloor_le x : Rfloor x <= x.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
 
 Lemma floor_le x : (floor x)%:~R <= x.
-Proof. by rewrite -RfloorE; exact: Rfloor_le. Qed.
+Proof. by rewrite ge_floor// num_real. Qed.
 
 Lemma lt_succ_Rfloor x : x < Rfloor x + 1.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
@@ -547,25 +549,27 @@ Lemma Rfloor_lt0 x : x < 0 -> Rfloor x < 0.
 Proof. by move=> x0; rewrite (le_lt_trans _ x0) // Rfloor_le. Qed.
 
 Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int.
-Proof. by rewrite /floor (Rfloor_natz n) Rtointz intz. Qed.
+Proof. by have /intr_inj -> := Rfloor_natz n; rewrite -pmulrn/= natz. Qed.
 
 Lemma floor0 : floor (0 : R) = 0.
-Proof. by rewrite /floor Rfloor0 (_ : 0 = 0%:R) // Rtointn. Qed.
+Proof. by rewrite /floor floor0. Qed.
 
 Lemma floor1 : floor (1 : R) = 1.
-Proof. by rewrite /floor Rfloor1 (_ : 1 = 1%:R) // Rtointn. Qed.
+Proof. by rewrite /floor floor1. Qed.
 
 Lemma floor_ge0 x : (0 <= floor x) = (0 <= x).
-Proof. by rewrite -(@ler_int R) -RfloorE -Rfloor_ge_int. Qed.
+Proof. by rewrite -floor_ge_int// num_real. Qed.
 
 Lemma floor_le0 x : x <= 0 -> floor x <= 0.
-Proof. by move=> ?; rewrite -(@ler_int R) -RfloorE Rfloor_le0. Qed.
+Proof. by move=> x0; rewrite -floor0 Num.Theory.floor_le. Qed.
 
 Lemma floor_lt0 x : x < 0 -> floor x < 0.
-Proof. by move=> ?; rewrite -(@ltrz0 R) RtointK ?isint_Rfloor// Rfloor_lt0. Qed.
+Proof.
+by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _))// num_real.
+Qed.
 
 Lemma le_floor : {homo @floor R : x y / x <= y}.
-Proof. by move=>*; rewrite -(@ler_int R) !RtointK ?isint_Rfloor ?le_Rfloor. Qed.
+Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed.
 
 Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).
 Proof.
@@ -577,7 +581,9 @@ apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0].
 Qed.
 
 Lemma lt_succ_floor x : x < (floor x)%:~R + 1.
-Proof. by rewrite -RfloorE lt_succ_Rfloor. Qed.
+Proof.
+by rewrite [X in _ + X](_ : 1 = 1%:~R)// -intrD lt_succ_floor// num_real.
+Qed.
 
 Lemma floor_lt_int x (z : int) : (x < z%:~R) = (floor x < z).
 Proof. by rewrite Rfloor_lt_int RfloorE ltr_int. Qed.
@@ -592,7 +598,7 @@ 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 floor_ge0 invr_ge0 subr_ge0 ltW.
-by rewrite -RfloorE lt_succ_Rfloor.
+by rewrite lt_succ_floor.
 Qed.
 
 End FloorTheory.
@@ -603,25 +609,25 @@ Variable R : realType.
 Implicit Types x y : R.
 
 Lemma isint_Rceil x : Rceil x \is a Rint.
-Proof. by rewrite /Rceil rpredN isint_Rfloor. Qed.
+Proof. by rewrite /Rceil RintC. Qed.
 
 Lemma Rceil0 : Rceil 0 = 0 :> R.
-Proof. by rewrite /Rceil oppr0 Rfloor0 oppr0. Qed.
+Proof. by rewrite /Rceil /ceil ceil0. Qed.
 
 Lemma Rceil_ge x : x <= Rceil x.
-Proof. by rewrite /Rceil lerNr Rfloor_le. Qed.
+Proof. by rewrite /Rceil le_ceil// num_real. Qed.
 
 Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.
-Proof. by move=> x y ?; rewrite lerNl opprK le_Rfloor // lerNl opprK. Qed.
+Proof. by move=> x y ?; rewrite /Rceil /ceil ler_int ceil_le. Qed.
 
 Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x.
-Proof. by move=> ?; rewrite -Rceil0 le_Rceil. Qed.
+Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed.
 
 Lemma RceilE x : Rceil x = (ceil x)%:~R.
-Proof. by rewrite /Rceil /ceil RfloorE mulrNz. Qed.
+Proof. by []. Qed.
 
 Lemma ceil_ge x : x <= (ceil x)%:~R.
-Proof. by rewrite -RceilE; exact: Rceil_ge. Qed.
+Proof. by rewrite le_ceil// num_real. Qed.
 
 Lemma ceil_ge0 x : 0 <= x -> 0 <= ceil x.
 Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.
@@ -636,12 +642,13 @@ Lemma le_ceil : {homo @ceil R : x y / x <= y}.
 Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed.
 
 Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (ceil x <= z).
-Proof. by rewrite /ceil lerNl -floor_ge_int// -lerNr mulrNz opprK. Qed.
+Proof. by rewrite /ceil; apply: ceil_le_int; rewrite num_real. Qed.
 
 Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x).
 Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
 
-Lemma ceilN x : ceil (- x) = - floor x. Proof. by rewrite /ceil opprK. Qed.
+Lemma ceilN x : ceil (- x) = - floor x. Proof.
+Proof. by rewrite /ceil /Num.ceil opprK. Qed.
 
 Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed.
 

theories/topology.v

@@ -5682,7 +5682,10 @@ Proof. by rewrite /distN invr0 reals.floor0. Qed.
 
 Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n.
 Proof.
-by rewrite /distN invrK floor_natz -[RHS]distn0; congr absz; rewrite subr0 intz.
+rewrite /distN invrK.
+apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm//; last first.
+  by rewrite -(floor0 R) floor_le.
+by rewrite -intrEfloor intrEge0.
 Qed.
 
 Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.