Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 7 commits into from
Jul 16, 2024
Merged
Show file tree
Hide file tree
Changes from 5 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 33 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,13 +27,35 @@
+ 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 `intr1`, `int1r`

### 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`, `ceil_lt_int`, `ceilN`, `abs_ceil_ge`
+ generalized to `archiDomainType` and precondition generalized:
+ `floor_le0`

### Renamed

- in `constructive_ereal.v`:
Expand Down Expand Up @@ -62,8 +84,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
71 changes: 71 additions & 0 deletions classical/mathcomp_extra.v
Original file line number Diff line number Diff line change
Expand Up @@ -374,3 +374,74 @@ 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.
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

From mathcomp Require Import archimedean.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why don't you import archimedean at the beginning of the file?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because only the next section needs it; if at some point this section moves to mathcomp I will not forget to erase even the Require Import.


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 (_ : 1 = 1%:~R)// floor_lt_int -ltzD1 add0r => /le_lt_trans; exact.
Qed.

Lemma floor_lt0 x : x < 0 -> Num.floor x < 0.
Proof. by rewrite -floor_lt_int. Qed.
pi8027 marked this conversation as resolved.
Show resolved Hide resolved

Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
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.intrKfloor n) intz. Qed.
pi8027 marked this conversation as resolved.
Show resolved Hide resolved

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.
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
Proof. exact: Num.Theory.le_ceil. Qed.
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
Proof. exact: Num.Theory.ceil_le_int. Qed.
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

Lemma ceil_ge0 x : 0 <= x -> 0 <= Num.ceil x.
Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.
affeldt-aist marked this conversation as resolved.
Show resolved Hide resolved

Lemma ceil_gt0 x : 0 < x -> 0 < Num.ceil x.
Proof. by rewrite -ceil_lt_int. Qed.

Lemma ceil_le0 x : x <= 0 -> Num.ceil x <= 0.
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 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.
5 changes: 3 additions & 2 deletions theories/Rstruct.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
pi8027 marked this conversation as resolved.
Show resolved Hide resolved
Rarchimedean_axiom.

(** Here are the lemmas that we will use to prove that R has
Expand Down
31 changes: 14 additions & 17 deletions theories/altreals/realsum.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -142,27 +142,25 @@ 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.
pose j := `|Num.floor (`|f x|^-1)|%N; exists j; rewrite inE.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are many occurrences of absz (Num.floor x). Did you check if Num.trunc can replace some of them or not? (That would be the case when x is positive and absz serves just as a type cast from int to nat.)

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.
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.
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 rewrite pmulrn -addn1 PoszD gez0_abs ?floor_ge0// lt_succ_floor.
Qed.

End SummableCountable.

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1201,9 +1199,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.
Expand Down
23 changes: 13 additions & 10 deletions theories/ereal.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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[+ _].
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Loading
Loading