Skip to content

Commit

Permalink
replace some `|Num.floor _| with Num.trunc _
Browse files Browse the repository at this point in the history
  • Loading branch information
pi8027 committed Dec 4, 2024
1 parent a86e8e5 commit aae93e5
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 20 deletions.
3 changes: 3 additions & 0 deletions classical/mathcomp_extra.v
Original file line number Diff line number Diff line change
Expand Up @@ -433,6 +433,9 @@ Section floor_ceil.
Context {R : archiDomainType}.
Implicit Type x : R.

Lemma lt_succ_trunc x : x < (Num.trunc x).+1%:R.
Proof. by have [/Num.Theory.trunc_itv/andP[]//|/lt_le_trans->] := leP 0 x. Qed.

Lemma ge_floor x : (Num.floor x)%:~R <= x.
Proof. exact: Num.Theory.ge_floor. Qed.

Expand Down
20 changes: 6 additions & 14 deletions reals/real_interval.v
Original file line number Diff line number Diff line change
Expand Up @@ -150,10 +150,8 @@ Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
Proof.
rewrite predeqE => y; split=> /=; last first.
by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy.
rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=.
rewrite in_itv /= xy /=.
have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_pwDr.
by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// intrD1 lt_succ_floor.
rewrite in_itv /= andbT => xy; exists (trunc y).+1 => //=.
by rewrite in_itv /= xy /= lt_succ_trunc.
Qed.

Lemma itv_o_inftyEbigcup x :
Expand Down Expand Up @@ -240,12 +238,8 @@ move gxE : (g x) => gx; case: gx gxE => [gx| |gxoo fxoo]; last 2 first.
- by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye.
move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first.
by exists 0%N => //; rewrite /E/= fxoo gxE// addye// leey.
rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1|%N => //.
rewrite /E/= -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW.
rewrite fxE gxE lee_fin -[leRHS]invrK lef_pV2//.
- by rewrite intrD1 ltW// lt_succ_floor.
- by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
- by rewrite posrE invr_gt0.
rewrite lte_fin -subr_gt0 => fgx; exists (trunc (fx - gx)^-1) => //.
by rewrite /E/= fxE gxE lee_fin invf_ple ?posrE//; apply/ltW/lt_succ_trunc.
Qed.

End set_ereal.
Expand All @@ -257,10 +251,8 @@ apply/seteqP; split=> [x ->|].
by move=> i _/=; rewrite in_itv/= lexx ltrBlDr ltrDl invr_gt0 ltr0n.
move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT.
apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//.
have := rx `|floor e^-1|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE.
rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
by rewrite intrD1 lt_succ_floor.
have := rx (trunc e^-1) I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
by rewrite lerB// invf_ple ?posrE//; apply/ltW/lt_succ_trunc.
Qed.

Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
Expand Down
8 changes: 2 additions & 6 deletions reals/reals.v
Original file line number Diff line number Diff line change
Expand Up @@ -529,12 +529,8 @@ Proof. exact: Num.Theory.floor_le. Qed.

Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x.
Proof.
move=> yx; exists `|floor (x - y)^-1|%N.
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_ge_int// invr_ge0 subr_ge0 ltW.
by rewrite intrD1 lt_succ_floor.
move=> yx; exists (trunc (x - y)^-1).
by rewrite -ltrBrDl invf_plt 1?posrE 1?subr_gt0// lt_succ_trunc.
Qed.

End FloorTheory.
Expand Down

0 comments on commit aae93e5

Please sign in to comment.