fixes #330

CHANGELOG_UNRELEASED.md

@@ -24,13 +24,33 @@
   + lemmas `g_sigma_completed_algebra_genE`, `negligible_sub_caratheodory`,
     `completed_caratheodory_measurable`
 
+- in `reals.v`:
+  + lemma `mem_rg1_floor`
+
+- in `mathcomp_extra.v`:
+  + lemma `ge_floor`
+
+- in `mathcomp_extra.v`:
+  + lemmas `intr1`, `int1r`, `natr_def`
+
 ### Changed
 
 - in `topology.v`:
   + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
     `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
 	into local `Let`'s
 
+- in `reals.v`:
+  + definitions `Rceil`, `Rfloor`
+
+- moved from `reals.v` to `mathcomp_extra.v`
+  + lemma `lt_succ_floor`: conclusion changed to match `lt_succ_floor` in MathComp,
+    generalized to `archiDomainType`
+  + generalized to `archiDomainType`:
+    lemmas `floor_ge0`, `floor_le0`, `floor_lt0`, `floor_natz`,
+    `floor_ge_int`, `floor_neq0`, `floor_lt_int`, `ceil_ge`, `ceil_ge0`, `ceil_gt0`,
+    `ceil_le0`, `ceil_ge_int`, `ceil_lt_int`, `ceilN`, `abs_ceil_ge`
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -56,8 +76,19 @@
 
 ### Deprecated
 
+- in `reals.v`:
+  + `floor_le` (use `ge_floor` instead)
+  + `le_floor` (use `Num.Theory.floor_le` instead)
+  + `le_ceil` (use `ceil_ge` instead)
+
 ### Removed
 
+- in `reals.v`:
+  + definition `floor` (use `Num.floor` instead)
+  + definition `ceil` (use `Num.ceil` instead)
+  + lemmas `floor0`, `floor1`
+  + lemma `le_floor` (use `Num.Theory.floor_le` instead)
+
 ### Infrastructure
 
 ### Misc

classical/mathcomp_extra.v

@@ -374,3 +374,83 @@ by elim: p => //= p <-;
 Qed.
 
 End positive.
+
+Lemma intr1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+Lemma int1r {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+From mathcomp Require Import archimedean.
+
+Lemma natr_def (n : int) : (n \is a Num.nat) = (0 <= n)%R.
+Proof. by []. Qed.
+
+Section floor_ceil.
+Context {R : archiDomainType}.
+Implicit Type x : R.
+
+Lemma ge_floor x : (Num.floor x)%:~R <= x.
+Proof. by rewrite Num.Theory.ge_floor. Qed.
+
+Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x).
+Proof. by rewrite -Num.Theory.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.
+
+Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
+Proof. by rewrite 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.
+
+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.
+
+Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
+Proof. by rewrite Num.Theory.le_ceil. 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.
+
+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.
+
+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.
+  by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl.
+by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor.
+Qed.
+
+End floor_ceil.

theories/altreals/realsum.v

@@ -2,9 +2,8 @@
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
-
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect all_algebra.
+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.
@@ -142,16 +141,16 @@ 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 := `|floor (1 / `|f x|)|%N; exists j; rewrite inE.
+  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 -RfloorE; apply lt_succ_Rfloor.
+  rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//.
+  by rewrite intr1 mathcomp_extra.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.
-move/finiteNP; pose j := `|floor (M / i.+1%:R)|.+1.
-pose K := (`|floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP.
+move/finiteNP; pose j := `|Num.floor (M / i.+1%:R)|.+1.
+pose K := (`|Num.floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP.
 move=> h; have /asboolP[] := xchooseP h.
 set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset x in s].
 suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM.
@@ -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.
-by rewrite natrD /= mulr1n pmulrn -{1}[floor _]gez0_abs // floor_ge0.
+have /andP[_] := mem_rg1_floor M; rewrite -addn1.
+by rewrite natrD /= mulr1n pmulrn -{1}[Num.floor _]gez0_abs // floor_ge0.
 Qed.
+
 End SummableCountable.
 
 (* -------------------------------------------------------------------- *)
@@ -1201,9 +1201,8 @@ Qed.
 
 Lemma sum_seq1 S x : (forall y, S y != 0 -> x == y) -> sum S = S x.
 Proof.
-move=> domS; rewrite (sum_finseq (r := [:: x])) //.
-  by move=> y; rewrite !inE => /domS /eqP->.
-by rewrite big_seq1.
+move=> domS; rewrite (sum_finseq (r := [:: x])) ?big_seq1//.
+by move=> y; rewrite !inE => /domS /eqP->.
 Qed.
 
 End SumTheory.

theories/ereal.v

@@ -1266,7 +1266,7 @@ rewrite predeq2E => x A; split.
     case=> [r' /= re'r'| |]/=.
     * rewrite /ereal_ball in re'r'.
       have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E).
-        apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //.
+        apply: reA; rewrite /ball /= ltr_norml//.
         rewrite ger0_norm ?subr_ge0// in re'r'.
         have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R.
           move: re'r'; rewrite /e' lt_min => /andP[+ _].
@@ -1276,7 +1276,7 @@ rewrite predeq2E => x A; split.
         rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT.
         rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0.
         by rewrite -lee_fin -le_contract.
-      apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //.
+      apply: reA; rewrite /ball /= ltr_norml//.
       rewrite ltr0_norm ?subr_lt0// opprB in re'r'.
       apply/andP; split; last first.
         by rewrite (@lt_trans _ _ 0%R) // subr_lt0 -lte_fin -lt_contract.
@@ -1402,21 +1402,24 @@ Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
 Proof.
 move=> P; rewrite /ereal_loc_seq.
 case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first.
-    have /ZnatP[N Nfloor] : floor (Num.max d 0%R) \is a Znat.
-      by rewrite Znat_def floor_ge0 le_max lexx orbC.
+    have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat.
+      by rewrite natr_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.
-    by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
-  have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
-    by rewrite Znat_def floor_ge0 le_max lexx orbC.
+    apply; rewrite (lt_le_trans (mathcomp_extra.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 natr_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.
-  by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
-have /ZnatP[N Nfloor] : floor (d%:num^-1) \is a Num.nat.
-  by rewrite Znat_def floor_ge0.
+  apply; rewrite (lt_le_trans (mathcomp_extra.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 natr_def floor_ge0.
 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.
-by rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor lerD// ler_nat.
+rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
+by rewrite !natr1 mulrz_nat ler_nat.
 Qed.