Skip to content

Commit

Permalink
fixes #330
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Jul 1, 2024
1 parent 47d1b22 commit f3f04b1
Show file tree
Hide file tree
Showing 14 changed files with 277 additions and 224 deletions.
36 changes: 36 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,31 @@
+ lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
`subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
into local `Let`'s
- in `reals.v`:
+ lemma `mem_rg1_floor`
+ lemma `ge_floor`

- in `mathcomp_extra.v`:
+ lemmas `intr1`, `int1r`, `natr_def`

- in `mathcomp_extra.v`:
+ lemma `ge_floor`

- in `reals.v`:
+ lemma `mem_rg1_floor`

### Changed

- 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 `ge_floor`, `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

Expand All @@ -56,8 +81,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
80 changes: 80 additions & 0 deletions classical/mathcomp_extra.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
23 changes: 11 additions & 12 deletions theories/altreals/realsum.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -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.
Expand Down
25 changes: 14 additions & 11 deletions theories/ereal.v
Original file line number Diff line number Diff line change
Expand Up @@ -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[+ _].
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Loading

0 comments on commit f3f04b1

Please sign in to comment.