Commit f91c2225 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Homogenized theorem names from Float_prop.

parent ab0e88f5
......@@ -1308,14 +1308,14 @@ right; rewrite J1,J2; reflexivity.
apply Rle_trans with (1:=uLev).
right; rewrite J3,J4; reflexivity.
case same_sign; intros (L1,L2).
rewrite J1 in L1; apply Fnum_ge_0_compat in L1; simpl in L1.
rewrite J3 in L2; apply Fnum_ge_0_compat in L2; simpl in L2.
rewrite J1 in L1; apply Fnum_ge_0 in L1; simpl in L1.
rewrite J3 in L2; apply Fnum_ge_0 in L2; simpl in L2.
left.
rewrite Z.abs_eq in H0.
omega.
omega.
rewrite J1 in L1; apply Fnum_le_0_compat in L1; simpl in L1.
rewrite J3 in L2; apply Fnum_le_0_compat in L2; simpl in L2.
rewrite J1 in L1; apply Fnum_le_0 in L1; simpl in L1.
rewrite J3 in L2; apply Fnum_le_0 in L2; simpl in L2.
right.
rewrite Z.abs_neq in H0.
omega.
......
......@@ -28,9 +28,9 @@ Proof.
intros m e.
case Zlt_bool_spec ; intros H.
apply Rlt_bool_true.
now apply F2R_lt_0_compat.
now apply F2R_lt_0.
apply Rlt_bool_false.
now apply F2R_ge_0_compat.
now apply F2R_ge_0.
Qed.
Definition plus (x y : float beta) :=
......@@ -112,7 +112,7 @@ rewrite F2R_0.
now apply round_0.
destruct H as [H|H].
elim Rgt_not_le with (1 := H).
now apply F2R_le_0_compat.
now apply F2R_le_0.
now elim Hz.
Qed.
......@@ -196,7 +196,7 @@ apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
rewrite Rsgn_div.
apply f_equal2 ; apply Rsgn_F2R.
contradict Hm.
apply F2R_eq_0_reg with (1 := Hm).
apply eq_0_F2R with (1 := Hm).
exact Hy.
unfold Rdiv.
rewrite Rabs_mult, Rabs_Rinv.
......
......@@ -162,7 +162,7 @@ apply Rplus_le_le_0_compat with (2 := Ho1).
apply Rmult_le_pos.
apply Rplus_le_le_0_compat with (1 := Ho1).
now apply Rle_trans with (1 := Rle_0_1).
now apply F2R_ge_0_compat.
now apply F2R_ge_0.
apply (conj Ho2).
intros H.
specialize (Ho (Rle_trans _ _ _ H (Rmin_l _ _))).
......@@ -229,7 +229,7 @@ Lemma hombnd_sub_init :
Proof.
intros u v Fu Fv.
split.
now apply F2R_ge_0_compat.
now apply F2R_ge_0.
unfold F2R at 1 3 ; simpl.
rewrite 2!Rmult_1_l.
repeat split ; try apply Rle_refl.
......@@ -239,7 +239,7 @@ rewrite round_generic.
unfold Rminus at 1.
rewrite Rplus_opp_r, Rabs_R0.
apply Rmult_le_pos.
now apply F2R_ge_0_compat.
now apply F2R_ge_0.
apply Rabs_pos.
apply valid_rnd_N.
apply FLT_format_plus_small ; try easy.
......
......@@ -587,7 +587,7 @@ intros x m e l [Hx|l' Hx Hl].
rewrite Hx.
split.
apply Rle_refl.
apply F2R_lt_compat.
apply F2R_lt.
apply Zlt_succ.
split.
now apply Rlt_le.
......@@ -649,7 +649,7 @@ Theorem inbetween_float_ex :
Proof.
intros m e l.
apply inbetween_ex.
apply F2R_lt_compat.
apply F2R_lt.
apply Zlt_succ.
Qed.
......@@ -666,7 +666,7 @@ apply inbetween_unique with (1 := H) (2 := H').
destruct (inbetween_float_bounds x m e l H) as (H1,H2).
destruct (inbetween_float_bounds x m' e l' H') as (H3,H4).
cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; omega.
now split ; apply F2R_lt_reg with beta e ; apply Rle_lt_trans with x.
now split ; apply lt_F2R with beta e ; apply Rle_lt_trans with x.
Qed.
End Fcalc_bracket_generic.
......@@ -644,7 +644,7 @@ assert (H: (e + k)%Z = cexp beta fexp x).
unfold k. ring.
refine (conj _ H).
rewrite <- H.
apply F2R_eq_compat.
apply F2R_eq.
replace (scaled_mantissa beta fexp x) with (IZR (Zfloor (scaled_mantissa beta fexp x))).
rewrite Ztrunc_IZR.
unfold scaled_mantissa.
......@@ -686,7 +686,7 @@ apply inbetween_float_bounds with (1 := H1).
(* *)
assert (Hm: (0 <= m)%Z).
cut (0 < m + 1)%Z. omega.
apply F2R_lt_reg with beta e.
apply lt_F2R with beta e.
rewrite F2R_0.
apply Rlt_trans with (1 := Hx).
apply Hx'.
......@@ -787,7 +787,7 @@ assert (Hx': (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R).
apply inbetween_float_bounds with (1 := H1).
rewrite <- Hx in Hx'.
split.
apply F2R_le_0_reg with (1 := proj1 Hx').
apply le_0_F2R with (1 := proj1 Hx').
apply F2R_gt_0_reg with (1 := proj2 Hx').
rewrite Hm, <- Hx in H1 |- *.
clear -H1.
......@@ -931,7 +931,7 @@ change (m = cond_Zopp false (choice false m loc_Exact))%Z.
rewrite <- (Zrnd_IZR rnd m) at 1.
assert (0 <= IZR m)%R.
apply IZR_le.
apply F2R_ge_0_reg with beta e.
apply ge_0_F2R with beta e.
rewrite <- H.
apply Rabs_pos.
rewrite <- Rlt_bool_false with (1 := H0).
......
......@@ -37,7 +37,7 @@ apply bpow_gt_0.
Qed.
(** Basic facts *)
Theorem F2R_le_reg :
Theorem le_F2R :
forall e m1 m2 : Z,
(F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
(m1 <= m2)%Z.
......@@ -49,7 +49,7 @@ apply bpow_gt_0.
exact H.
Qed.
Theorem F2R_le_compat :
Theorem F2R_le :
forall m1 m2 e : Z,
(m1 <= m2)%Z ->
(F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R.
......@@ -61,7 +61,7 @@ apply bpow_ge_0.
now apply IZR_le.
Qed.
Theorem F2R_lt_reg :
Theorem lt_F2R :
forall e m1 m2 : Z,
(F2R (Float beta m1 e) < F2R (Float beta m2 e))%R ->
(m1 < m2)%Z.
......@@ -73,7 +73,7 @@ apply bpow_gt_0.
exact H.
Qed.
Theorem F2R_lt_compat :
Theorem F2R_lt :
forall e m1 m2 : Z,
(m1 < m2)%Z ->
(F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.
......@@ -85,7 +85,7 @@ apply bpow_gt_0.
now apply IZR_lt.
Qed.
Theorem F2R_eq_compat :
Theorem F2R_eq :
forall e m1 m2 : Z,
(m1 = m2)%Z ->
(F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
......@@ -94,14 +94,14 @@ intros e m1 m2 H.
now apply (f_equal (fun m => F2R (Float beta m e))).
Qed.
Theorem F2R_eq_reg :
Theorem eq_F2R :
forall e m1 m2 : Z,
F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
m1 = m2.
Proof.
intros e m1 m2 H.
apply Zle_antisym ;
apply F2R_le_reg with e ;
apply le_F2R with e ;
rewrite H ;
apply Rle_refl.
Qed.
......@@ -131,6 +131,15 @@ rewrite <- Ropp_mult_distr_l_reverse.
now rewrite opp_IZR.
Qed.
Theorem F2R_cond_Zopp :
forall b m e,
F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).
Proof.
intros [|] m e ; unfold F2R ; simpl.
now rewrite opp_IZR, Ropp_mult_distr_l_reverse.
apply refl_equal.
Qed.
(** Sign facts *)
Theorem F2R_0 :
forall e : Z,
......@@ -141,33 +150,33 @@ unfold F2R. simpl.
apply Rmult_0_l.
Qed.
Theorem F2R_eq_0_reg :
Theorem eq_0_F2R :
forall m e : Z,
F2R (Float beta m e) = 0%R ->
m = Z0.
Proof.
intros m e H.
apply F2R_eq_reg with e.
apply eq_F2R with e.
now rewrite F2R_0.
Qed.
Theorem F2R_ge_0_reg :
Theorem ge_0_F2R :
forall m e : Z,
(0 <= F2R (Float beta m e))%R ->
(0 <= m)%Z.
Proof.
intros m e H.
apply F2R_le_reg with e.
apply le_F2R with e.
now rewrite F2R_0.
Qed.
Theorem F2R_le_0_reg :
Theorem le_0_F2R :
forall m e : Z,
(F2R (Float beta m e) <= 0)%R ->
(m <= 0)%Z.
Proof.
intros m e H.
apply F2R_le_reg with e.
apply le_F2R with e.
now rewrite F2R_0.
Qed.
......@@ -177,89 +186,89 @@ Theorem F2R_gt_0_reg :
(0 < m)%Z.
Proof.
intros m e H.
apply F2R_lt_reg with e.
apply lt_F2R with e.
now rewrite F2R_0.
Qed.
Theorem F2R_lt_0_reg :
Theorem lt_0_F2R :
forall m e : Z,
(F2R (Float beta m e) < 0)%R ->
(m < 0)%Z.
Proof.
intros m e H.
apply F2R_lt_reg with e.
apply lt_F2R with e.
now rewrite F2R_0.
Qed.
Theorem F2R_ge_0_compat :
Theorem F2R_ge_0 :
forall f : float beta,
(0 <= Fnum f)%Z ->
(0 <= F2R f)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_le_compat.
now apply F2R_le.
Qed.
Theorem F2R_le_0_compat :
Theorem F2R_le_0 :
forall f : float beta,
(Fnum f <= 0)%Z ->
(F2R f <= 0)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_le_compat.
now apply F2R_le.
Qed.
Theorem F2R_gt_0_compat :
Theorem F2R_gt_0 :
forall f : float beta,
(0 < Fnum f)%Z ->
(0 < F2R f)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_lt_compat.
now apply F2R_lt.
Qed.
Theorem F2R_lt_0_compat :
Theorem F2R_lt_0 :
forall f : float beta,
(Fnum f < 0)%Z ->
(F2R f < 0)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_lt_compat.
now apply F2R_lt.
Qed.
Theorem F2R_neq_0_compat :
Theorem F2R_neq_0 :
forall f : float beta,
(Fnum f <> 0)%Z ->
(F2R f <> 0)%R.
Proof.
intros f H H1.
apply H.
now apply F2R_eq_0_reg with (Fexp f).
now apply eq_0_F2R with (Fexp f).
Qed.
Lemma Fnum_ge_0_compat: forall (f : float beta),
Lemma Fnum_ge_0: forall (f : float beta),
(0 <= F2R f)%R -> (0 <= Fnum f)%Z.
Proof.
intros f H.
case (Zle_or_lt 0 (Fnum f)); trivial.
intros H1; contradict H.
apply Rlt_not_le.
now apply F2R_lt_0_compat.
now apply F2R_lt_0.
Qed.
Lemma Fnum_le_0_compat: forall (f : float beta),
Lemma Fnum_le_0: forall (f : float beta),
(F2R f <= 0)%R -> (Fnum f <= 0)%Z.
Proof.
intros f H.
case (Zle_or_lt (Fnum f) 0); trivial.
intros H1; contradict H.
apply Rlt_not_le.
now apply F2R_gt_0_compat.
now apply F2R_gt_0.
Qed.
(** Floats and bpow *)
......@@ -279,7 +288,7 @@ Theorem bpow_le_F2R :
Proof.
intros m e H.
rewrite <- F2R_bpow.
apply F2R_le_compat.
apply F2R_le.
now apply (Zlt_le_succ 0).
Qed.
......@@ -426,7 +435,7 @@ destruct (mag beta (F2R (Float beta m e))) as (ex, He).
simpl.
apply mag_unique.
assert (Hp1: (0 < F2R (Float beta m e))%R).
now apply F2R_gt_0_compat.
now apply F2R_gt_0.
specialize (He (Rgt_not_eq _ _ Hp1)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
destruct He as (He1, He2).
......@@ -496,9 +505,9 @@ elim Rlt_not_le with (1 := H21).
apply Zge_le in H0.
apply (F2R_change_exp e1 m2 e2) in H0.
rewrite H0.
apply F2R_le_compat.
apply F2R_le.
apply Zlt_le_succ.
apply (F2R_lt_reg e1).
apply (lt_F2R e1).
now rewrite <- H0.
(* . *)
split.
......@@ -507,7 +516,7 @@ rewrite (Zplus_comm e1), (Zplus_comm e2).
assert (Hp2: (0 < m2)%Z).
apply (F2R_gt_0_reg m2 e2).
apply Rlt_trans with (2 := H12).
now apply F2R_gt_0_compat.
now apply F2R_gt_0.
rewrite <- 2!mag_F2R.
destruct (mag beta (F2R (Float beta m1 e1))) as (e1', H1).
simpl.
......@@ -518,7 +527,7 @@ rewrite <- (Zabs_eq m1), F2R_Zabs.
apply H1.
apply Rgt_not_eq.
apply Rlt_gt.
now apply F2R_gt_0_compat.
now apply F2R_gt_0.
now apply Zlt_le_weak.
clear H1.
rewrite <- F2R_Zabs, Zabs_eq.
......@@ -535,13 +544,4 @@ apply sym_not_eq.
now apply Zlt_not_eq.
Qed.
Theorem F2R_cond_Zopp :
forall b m e,
F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).
Proof.
intros [|] m e ; unfold F2R ; simpl.
now rewrite opp_IZR, Ropp_mult_distr_l_reverse.
apply refl_equal.
Qed.
End Float_prop.
......@@ -169,7 +169,7 @@ intros He.
specialize (He Zm).
unfold F2R at 3. simpl.
rewrite F2R_change_exp with (1 := He).
apply F2R_eq_compat.
apply F2R_eq.
rewrite Rmult_assoc, <- bpow_plus, <- IZR_Zpower, <- mult_IZR.
now rewrite Ztrunc_IZR.
now apply Zle_left.
......@@ -187,7 +187,7 @@ apply generic_format_F2R.
simpl in *; intros H3.
rewrite H1; apply H2.
intros Y; apply H3.
apply F2R_eq_0_reg with beta e.
apply eq_0_F2R with beta e.
now rewrite H1.
Qed.
......@@ -232,7 +232,7 @@ rewrite H in H1.
rewrite <- H2 in H1. clear H2.
rewrite H1 in H |- *.
apply (f_equal (fun m => Float beta m e2)).
apply F2R_eq_reg with (1 := H).
apply eq_F2R with (1 := H).
Qed.
Theorem scaled_mantissa_generic :
......@@ -466,7 +466,7 @@ intros x m e (Hx,Hx2) Hf.
apply Rlt_not_le with (1 := Hx2). clear Hx2.
rewrite Hf.
fold e.
apply F2R_le_compat.
apply F2R_le.
apply Zlt_le_succ.
apply lt_IZR.
rewrite <- scaled_mantissa_generic with (1 := Hf).
......@@ -483,7 +483,7 @@ intros (m, e) Hf.
unfold canonical in Hf. simpl in Hf.
unfold generic_format, scaled_mantissa.
rewrite <- Hf.
apply F2R_eq_compat.
apply F2R_eq.
unfold F2R. simpl.
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
now rewrite Ztrunc_IZR.
......@@ -720,7 +720,7 @@ assert (Heq: fexp ex = fexp ey -> (round x <= round y)%R).
rewrite mag_unique_pos with (1 := Hex).
rewrite mag_unique_pos with (1 := Hey).
rewrite H.
apply F2R_le_compat.
apply F2R_le.
apply Zrnd_le.
apply Rmult_le_compat_r with (2 := Hxy).
apply bpow_ge_0.
......@@ -853,7 +853,7 @@ Proof.
intros x.
unfold round.
rewrite <- F2R_Zopp, cexp_opp, scaled_mantissa_opp.
apply F2R_eq_compat.
apply F2R_eq.
apply sym_eq.
exact (Zopp_involutive _).
Qed.
......@@ -938,7 +938,7 @@ now apply Ropp_lt_contravar.
now apply Ropp_le_contravar.
(* . 0 <= y *)
apply Rle_trans with 0%R.
apply F2R_le_0_compat. simpl.
apply F2R_le_0. simpl.
rewrite <- (Zrnd_IZR rnd 0).
apply Zrnd_le...
simpl.
......@@ -946,7 +946,7 @@ rewrite <- (Rmult_0_l (bpow (- fexp (mag beta x)))).
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply Rlt_le.
apply F2R_ge_0_compat. simpl.
apply F2R_ge_0. simpl.
rewrite <- (Zrnd_IZR rnd 0).
apply Zrnd_le...
apply Rmult_le_pos.
......@@ -955,7 +955,7 @@ apply bpow_ge_0.
(* x = 0 *)
rewrite Hx.
rewrite round_0...
apply F2R_ge_0_compat.
apply F2R_ge_0.
simpl.
rewrite <- (Zrnd_IZR rnd 0).
apply Zrnd_le...
......@@ -2291,7 +2291,7 @@ intros Zx.
unfold cexp at 1.
rewrite mag_round_ZR...
contradict Zx.
apply F2R_eq_0_reg with (1 := Zx).
apply eq_0_F2R with (1 := Zx).
(* - - round fexp2 x has too many digits for fexp1 *)
destruct (round_bounded_large_pos fexp2 rnd x ex He Ex) as (Hr1,[Hr2|Hr2]).
apply generic_format_F2R.
......
......@@ -113,7 +113,7 @@ rewrite (Rabs_pos_eq _ (Rlt_le _ _ H0x)) in Hex.
destruct (Zle_or_lt ex (fexp ex)) as [Hxe|Hxe].
(* small x *)
assert (Hd3 : Fnum xd = Z0).
apply F2R_eq_0_reg with beta (Fexp xd).
apply eq_0_F2R with beta (Fexp xd).
change (F2R xd = R0).
rewrite Hxd.
apply round_DN_small_pos with (1 := Hex) (2 := Hxe).
......
......@@ -1861,7 +1861,7 @@ case negligible_exp_spec.
(* without minimal exponent *)
intros K; contradict Hx2.
apply Rlt_not_eq.
apply F2R_gt_0_compat; simpl.
apply F2R_gt_0; simpl.
apply Zlt_le_trans with 1%Z.
apply Pos2Z.is_pos.
apply Zfloor_lub.
......
This diff is collapsed.
......@@ -79,7 +79,7 @@ apply generic_format_F2R.
rewrite <- H0; intros H3.
apply monotone_exp.
apply mag_le_abs.
rewrite H0; apply F2R_neq_0_compat; easy.
rewrite H0; apply F2R_neq_0; easy.
apply Rmult_le_reg_l with (/Rabs y)%R.
apply Rinv_0_lt_compat.
apply Rabs_pos_lt.
......
......@@ -150,7 +150,7 @@ apply relative_error.
unfold x.
rewrite <- F2R_Zabs.
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
apply lt_F2R with beta emin.
rewrite F2R_0, F2R_Zabs.
now apply Rabs_pos_lt.
Qed.
......@@ -218,7 +218,7 @@ exact Hp.
unfold x.
rewrite <- F2R_Zabs.
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
apply lt_F2R with beta emin.
rewrite F2R_0, F2R_Zabs.
now apply Rabs_pos_lt.
Qed.
......@@ -296,7 +296,7 @@ apply relative_error_N.
unfold x.
rewrite <- F2R_Zabs.
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
apply lt_F2R with beta emin.
rewrite F2R_0, F2R_Zabs.
now apply Rabs_pos_lt.
Qed.
......@@ -381,7 +381,7 @@ apply relative_error_N_round with (1 := Hp).
unfold x.
rewrite <- F2R_Zabs.
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
apply lt_F2R with beta emin.
rewrite F2R_0, F2R_Zabs.
now apply Rabs_pos_lt.
Qed.
......
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