Commit cb21f113 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename F2R_gt_0_reg into gt_0_F2R.

parent 99aabd6e
......@@ -43,7 +43,7 @@ unfold cexp.
apply inbetween_float_bounds in Bx.
assert (0 <= m)%Z as Hm.
{ apply Zlt_succ_le.
eapply F2R_gt_0_reg.
eapply gt_0_F2R.
apply Rlt_trans with (1 := Px).
apply Bx. }
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|<-].
......@@ -83,7 +83,7 @@ destruct Px as [Px|Px].
rewrite <- Px in Bx.
destruct Bx as [Bx1 Bx2].
apply lt_0_F2R in Bx1.
apply F2R_gt_0_reg in Bx2.
apply gt_0_F2R in Bx2.
omega.
Qed.
......@@ -893,7 +893,7 @@ apply inbetween_float_bounds with (1 := H1).
rewrite <- Hx in Hx'.
split.
apply le_0_F2R with (1 := proj1 Hx').
apply F2R_gt_0_reg with (1 := proj2 Hx').
apply gt_0_F2R with (1 := proj2 Hx').
rewrite Hm, <- Hx in H1 |- *.
clear -H1.
case H1.
......@@ -970,7 +970,7 @@ intros x m e l [Hx|Hx] H1 H2.
rewrite <- Hx in Hx'.
split.
apply le_0_F2R with (1 := proj1 Hx').
apply F2R_gt_0_reg with (1 := proj2 Hx').
apply gt_0_F2R with (1 := proj2 Hx').
rewrite Hm, <- Hx in H1 |- *.
clear -H1.
destruct H1 as [_ | l' [H _] _].
......@@ -1107,7 +1107,7 @@ assert (IZR (-m) < 0)%R.
rewrite opp_IZR.
apply Ropp_lt_gt_0_contravar.
apply IZR_lt.
apply F2R_gt_0_reg with beta e.
apply gt_0_F2R with beta e.
rewrite <- H.
apply Rabs_pos_lt.
now apply Rlt_not_eq.
......
......@@ -180,7 +180,7 @@ apply le_F2R with e.
now rewrite F2R_0.
Qed.
Theorem F2R_gt_0_reg :
Theorem gt_0_F2R :
forall m e : Z,
(0 < F2R (Float beta m e))%R ->
(0 < m)%Z.
......@@ -526,7 +526,7 @@ split.
exact He.
rewrite (Zplus_comm e1), (Zplus_comm e2).
assert (Hp2: (0 < m2)%Z).
apply (F2R_gt_0_reg m2 e2).
apply (gt_0_F2R m2 e2).
apply Rlt_trans with (2 := H12).
now apply F2R_gt_0.
rewrite <- 2!mag_F2R.
......
......@@ -502,7 +502,7 @@ rewrite Fx.
apply Rle_trans with (bpow (fexp (mag beta x))).
now apply bpow_le.
apply bpow_le_F2R.
apply F2R_gt_0_reg with beta (cexp x).
apply gt_0_F2R with beta (cexp x).
now rewrite <- Fx.
Qed.
......
......@@ -158,7 +158,7 @@ unfold F2R; simpl.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply IZR_le, (Zlt_le_succ 0).
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
now rewrite <- Fx.
Qed.
......@@ -446,7 +446,7 @@ intros x e Fx Hx' Hx.
(* *)
assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z.
assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z.
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
rewrite <- Fx.
apply Rle_lt_trans with (2:=Hx).
apply bpow_ge_0.
......@@ -489,7 +489,7 @@ pattern (bpow (cexp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
rewrite <- plus_IZR.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rgt_not_eq.
......@@ -551,7 +551,7 @@ apply Rmult_le_compat_r.
apply bpow_ge_0.
apply IZR_le.
assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z.
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
rewrite <- Fx.
apply Rle_lt_trans with (2:=proj1 Ex').
apply bpow_ge_0.
......@@ -879,7 +879,7 @@ pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply IZR_le, (Zlt_le_succ 0).
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
now rewrite <- Fx.
Qed.
......@@ -1015,7 +1015,7 @@ pattern (bpow (cexp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
rewrite <- plus_IZR.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rgt_not_eq.
......@@ -1344,7 +1344,7 @@ omega.
absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z.
omega.
split.
apply F2R_gt_0_reg with beta (cexp beta fexp x).
apply gt_0_F2R with beta (cexp beta fexp x).
now rewrite <- Fx.
apply lt_IZR.
apply Rmult_lt_reg_r with (bpow (cexp beta fexp x)).
......
......@@ -958,7 +958,7 @@ now apply f_equal.
apply abs_cond_Zopp.
apply Zle_trans with (2 := Hm).
apply Zlt_succ_le.
apply F2R_gt_0_reg with radix2 e1.
apply gt_0_F2R with radix2 e1.
apply Rle_lt_trans with (1 := Rabs_pos x).
exact (proj2 (inbetween_float_bounds _ _ _ _ _ H1a)).
(* . *)
......@@ -1094,7 +1094,7 @@ exact inbetween_int_NA_sign.
(* *)
apply inbetween_float_bounds in Bx.
apply Zlt_succ_le.
eapply F2R_gt_0_reg.
eapply gt_0_F2R.
apply Rle_lt_trans with (2 := proj2 Bx).
apply Rabs_pos.
Qed.
......@@ -1138,7 +1138,7 @@ now apply f_equal.
apply abs_cond_Zopp.
apply Zle_trans with (2 := Hm).
apply Zlt_succ_le.
apply F2R_gt_0_reg with radix2 e1.
apply gt_0_F2R with radix2 e1.
apply Rle_lt_trans with (1 := Rabs_pos x).
exact (proj2 (inbetween_float_bounds _ _ _ _ _ H1a)).
(* . *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment