fixes #330 (floor and ceil subsumed by MathComp) (#1244)

* fixes #330

---------

Co-authored-by: Kazuhiko Sakaguchi <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -27,13 +27,37 @@
   + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`)
   + lemma `FTC1Ny`
 
+- in `reals.v`:
+  + lemma `mem_rg1_floor`
+
+- in `mathcomp_extra.v`:
+  + lemma `ge_floor`
+
+- in `mathcomp_extra.v`:
+  + lemmas `intr1D`, `intrD1`, `floor_eq`, `floorN`
+
 ### 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_lt0`, `floor_natz`,
+    `floor_ge_int`, `floor_neq0`, `floor_lt_int`, `ceil_ge`, `ceil_ge0`, `ceil_gt0`,
+    `ceil_le0`, `ceil_ge_int`, `ceilN`, `abs_ceil_ge`
+  + generalized to `archiDomainType` and precondition generalized:
+    * `floor_le0`
+  + generalized to `archiDomainType` and renamed:
+    * `ceil_lt_int` -> `ceil_gt_int`
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -62,8 +86,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 intrD1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+Lemma intr1D {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+From mathcomp Require Import archimedean.
+
+Section floor_ceil.
+Context {R : archiDomainType}.
+Implicit Type x : R.
+
+Lemma ge_floor x : (Num.floor x)%:~R <= x.
+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 -floor_ge_int. Qed.
+
+Lemma floor_le0 x : (x < 1) = (Num.floor x <= 0).
+Proof. by rewrite -ltzD1 add0r -floor_lt_int. Qed.
+
+Lemma floor_lt0 x : (x < 0) = (Num.floor x < 0).
+Proof. by rewrite -floor_lt_int. Qed.
+
+Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
+Proof. exact: Num.Theory.lt_succ_floor. Qed.
+
+Lemma floor_eq x m : (Num.floor x == m) = (m%:~R <= x < (m + 1)%:~R).
+Proof.
+apply/eqP/idP; [move=> <-|by move=> /Num.Theory.floor_def ->].
+by rewrite Num.Theory.ge_floor//= Num.Theory.lt_succ_floor.
+Qed.
+
+Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
+Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.le_ceil` instead")]
+Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
+Proof. exact: Num.Theory.le_ceil. Qed.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le_int`")]
+Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
+Proof. exact: Num.Theory.ceil_le_int. Qed.
+
+Lemma ceil_gt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
+Proof. by rewrite ltNge Num.Theory.ceil_le_int// -ltNge. Qed.
+
+Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
+Proof. by rewrite /Num.ceil opprK. Qed.
+
+Lemma floorN x : Num.floor (- x) = - Num.ceil x.
+Proof. by rewrite /Num.ceil opprK. Qed.
+
+Lemma ceil_ge0 x : (- 1 < x) = (0 <= Num.ceil x).
+Proof. by rewrite ltrNl floor_le0 floorN lerNl oppr0. Qed.
+
+Lemma ceil_gt0 x : (0 < x) = (0 < Num.ceil x).
+Proof. by rewrite -ceil_gt_int. Qed.
+
+Lemma ceil_le0 x : (x <= 0) = (Num.ceil x <= 0).
+Proof. by rewrite -Num.Theory.ceil_le_int. Qed.
+
+Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R.
+Proof.
+rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x.
+  by rewrite !gtr0_norm// -?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl.
+by rewrite !ler0_norm -?ceil_le0// opprK intrD1 ltW// lt_succ_floor.
+Qed.
+
+End floor_ceil.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")]
+Notation ceil_lt_int := ceil_gt_int (only parsing).

theories/Rstruct.v

@@ -29,6 +29,7 @@ Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
 Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
 Require Import Rtrigo1 Reals.
 From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
+From mathcomp Require Import archimedean.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra.
 
@@ -87,7 +88,7 @@ Proof. by move=> *; rewrite Rplus_assoc. Qed.
 HB.instance Definition _ := GRing.isZmodule.Build R
   RplusA Rplus_comm Rplus_0_l Rplus_opp_l.
 
-Fact RmultA : associative (Rmult).
+Fact RmultA : associative Rmult.
 Proof. by move=> *; rewrite Rmult_assoc. Qed.
 
 Fact R1_neq_0 : R1 != R0.
@@ -292,7 +293,7 @@ rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _).
 exact: Rle_minus.
 Qed.
 
-HB.instance Definition _ := Num.RealField_isArchimedean.Build R
+HB.instance Definition _ := Num.NumDomain_bounded_isArchimedean.Build R
   Rarchimedean_axiom.
 
 (** Here are the lemmas that we will use to prove that R has

theories/altreals/realsum.v

@@ -2,12 +2,11 @@
 (* 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.
+From mathcomp.classical Require Import classical_sets functions.
 Require Import topology.
 
 Set Implicit Arguments.
@@ -16,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,28 +141,24 @@ Lemma summable_countn0 : summable f -> countable [pred x | f x != 0].
 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.
-  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.
+  move=> x; rewrite !inE => nz_fx; exists (Num.trunc `|f x|^-1).
+  rewrite inE mul1r invf_plt ?unfold_in /= ?normr_gt0 //.
+  by have/trunc_itv/andP[]: 0 <= `|f x|^-1 by rewrite invr_ge0 normr_ge0.
 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=> h; have /asboolP[] := xchooseP h.
+move=> /finiteNP/(_ ((Num.trunc M).+1 * i.+1)%N)/asboolP/exists_asboolP 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.
 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_Rfloor M; rewrite RfloorE -addn1.
-by rewrite natrD /= mulr1n pmulrn -{1}[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 case/trunc_itv/andP: ge0_M.
 Qed.
+
 End SummableCountable.
 
 (* -------------------------------------------------------------------- *)
@@ -1201,9 +1197,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

@@ -5,8 +5,8 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra finmap archimedean.
-From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
+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.
 
@@ -1266,7 +1267,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 +1277,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 +1403,23 @@ 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.
+    have /natrP[N Nfloor] : Num.floor (Num.max d 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.
     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.
+    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.
-  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.
+  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.
 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.
+by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor !natr1 mulrz_nat ler_nat.
 Qed.