Commit 80b7f17a authored by BOLDO Sylvie's avatar BOLDO Sylvie

Recycling the Pff/Float library

parent cbb451bf
......@@ -27,7 +27,10 @@ FILES = \
Prop/Round_odd.v \
Prop/Double_rounding.v \
IEEE754/Binary.v \
IEEE754/Bits.v
IEEE754/Bits.v \
Translate/Pff.v \
Translate/Ftranslate_flocq2Pff.v \
Translate/Missing_theos.v
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
......@@ -87,7 +90,7 @@ install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop IEEE754; do mkdir -p @libdir@/$d; done
for d in Core Calc Prop IEEE754 Translate; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
......
......@@ -18,10 +18,8 @@ COPYING file for more details.
*)
(** Translation from Flocq to Pff *)
Require Import Float.Veltkamp.
Require Import Float.RND.
From Flocq Require Import Core Binary.
From Flocq Require Import Pff Core Binary.
Section RND_Closest_c.
(* extension of pff for rounding function with arbitrary tie *)
......@@ -29,7 +27,7 @@ Variable b : Fbound.
Variable beta : radix.
Variable p : nat.
Coercion Local FtoRradix := FtoR beta.
Coercion FtoRradix := FtoR beta.
Hypothesis pGreaterThanOne : 1 < p.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta p.
......@@ -88,10 +86,10 @@ unfold RND_Closest; case (Rle_dec _ _); intros H1.
case (Rle_lt_or_eq_dec _ _ H1); intros H2.
(* . *)
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
rewrite Faux.Rabsolu_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
case (Rle_or_lt f r); intros H4.
rewrite Faux.Rabsolu_left1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
......@@ -102,10 +100,10 @@ now apply Rlt_le.
(* . *)
case (choice _).
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
rewrite Faux.Rabsolu_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
case (Rle_or_lt f r); intros H5.
rewrite Faux.Rabsolu_left1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
......@@ -115,11 +113,11 @@ apply (RND_Max_correct b beta p) with (r:=r); try easy.
now apply Rlt_le.
(* . *)
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
rewrite Faux.Rabsolu_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite <- H2.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
case (Rle_or_lt f r); intros H5.
rewrite Faux.Rabsolu_left1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
......@@ -129,11 +127,11 @@ apply (RND_Max_correct b beta p) with (r:=r); try easy.
now apply Rlt_le.
(* . *)
apply Rnot_le_lt in H1.
rewrite Faux.Rabsolu_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
rewrite Faux.Rabsolu_left1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
case (Rle_or_lt f r); intros H4.
rewrite Faux.Rabsolu_left1; [ idtac | apply V4; auto with real ].
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
apply Ropp_le_contravar, Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
......@@ -177,7 +175,7 @@ omega.
Qed.
Lemma FtoR_F2R: forall (f:Float.float) (g: float beta), Float.Fnum f = Fnum g -> Float.Fexp f = Fexp g ->
Lemma FtoR_F2R: forall (f:Pff.float) (g: float beta), Pff.Fnum f = Fnum g -> Pff.Fexp f = Fexp g ->
FtoR beta f = F2R g.
Proof.
intros f g H1 H2; unfold FtoR, F2R.
......@@ -218,7 +216,7 @@ Lemma pff_format_is_format: forall f, Fbounded b f ->
(generic_format beta (FLT_exp (-dExp b) p) (FtoR beta f)).
intros f Hf.
apply generic_format_FLT; auto with zarith.
exists (Float beta (Float.Fnum f) (Float.Fexp f)).
exists (Float beta (Pff.Fnum f) (Pff.Fexp f)).
unfold F2R, FtoR; simpl.
rewrite bpow_powerRZ.
reflexivity.
......@@ -232,7 +230,7 @@ Qed.
Lemma format_is_pff_format': forall r,
(generic_format beta (FLT_exp (-dExp b) p) r) ->
Fbounded b (Float.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r))
Fbounded b (Pff.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r))
(cexp beta (FLT_exp (-dExp b) p) r)).
Proof.
intros x; unfold generic_format.
......@@ -309,10 +307,10 @@ Qed.
Lemma pff_canonic_is_canonic: forall f, Fcanonic beta b f -> FtoR beta f <> 0 ->
canonical beta (FLT_exp (- dExp b) p)
(Float beta (Float.Fnum f) (Float.Fexp f)).
(Float beta (Pff.Fnum f) (Pff.Fexp f)).
Proof.
intros f Hf1 Hf2; unfold canonical; simpl.
assert (K:(F2R (Float beta (Float.Fnum f) (Float.Fexp f)) = FtoR beta f)).
assert (K:(F2R (Float beta (Pff.Fnum f) (Pff.Fexp f)) = FtoR beta f)).
unfold FtoR, F2R; simpl.
now rewrite bpow_powerRZ.
unfold cexp, FLT_exp.
......@@ -321,21 +319,21 @@ destruct (mag beta (FtoR beta f)) as (e, He).
simpl; destruct Hf1.
(* . *)
destruct H as (H1,H2).
cut (Float.Fexp f = e-p)%Z.
cut (Pff.Fexp f = e-p)%Z.
intros V; rewrite V.
apply sym_eq; apply Zmax_left.
rewrite <- V; destruct H1; auto with zarith.
assert (e = Float.Fexp f + p)%Z;[idtac|omega].
assert (e = Pff.Fexp f + p)%Z;[idtac|omega].
apply trans_eq with (mag beta (FtoR beta f)).
apply sym_eq; apply mag_unique.
apply He; assumption.
apply mag_unique.
rewrite <- K; unfold F2R; simpl.
rewrite Rabs_mult.
rewrite (Rabs_right (bpow beta (Float.Fexp f))).
rewrite (Rabs_right (bpow beta (Pff.Fexp f))).
2: apply Rle_ge; apply bpow_ge_0.
split.
replace (Float.Fexp f + p - 1)%Z with ((p-1)+Float.Fexp f)%Z by ring.
replace (Pff.Fexp f + p - 1)%Z with ((p-1)+Pff.Fexp f)%Z by ring.
rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
......@@ -385,6 +383,7 @@ apply FsubnormFabs; auto with zarith.
apply radix_gt_1.
split; [idtac|split]; assumption.
rewrite Fabs_correct; auto with real zarith.
apply Rabs_pos.
apply radix_gt_0.
unfold firstNormalPos, FtoR, nNormMin.
simpl.
......@@ -437,7 +436,7 @@ unfold FNeven, Feven, Even.
exists 0%Z.
rewrite Zmult_0_r.
apply eq_IZR.
apply Rmult_eq_reg_l with (powerRZ beta (Float.Fexp (Fnormalize beta b (Zabs_nat p) f)))%R.
apply Rmult_eq_reg_l with (powerRZ beta (Pff.Fexp (Fnormalize beta b (Zabs_nat p) f)))%R.
rewrite Rmult_0_r.
rewrite <- L; unfold FtoR; simpl; ring.
apply powerRZ_NOR; auto with zarith real.
......@@ -449,8 +448,8 @@ destruct H as (g,(Hg1,(Hg2,Hg3))).
left.
unfold FNeven, Feven.
apply equiv_RNDs_aux.
replace (Float.Fnum (Fnormalize beta b (Zabs_nat p) f)) with (Fnum g); try assumption.
replace g with (Float beta (Float.Fnum (Fnormalize beta b (Zabs_nat p) f)) (Float.Fexp (Fnormalize beta b (Zabs_nat p) f))).
replace (Pff.Fnum (Fnormalize beta b (Zabs_nat p) f)) with (Fnum g); try assumption.
replace g with (Float beta (Pff.Fnum (Fnormalize beta b (Zabs_nat p) f)) (Pff.Fexp (Fnormalize beta b (Zabs_nat p) f))).
easy.
apply canonical_unique with (FLT_exp (- dExp b) p).
2: assumption.
......@@ -484,7 +483,7 @@ Qed.
Lemma round_NE_is_pff_round: forall (r:R),
exists f:Float.float, (Fcanonic beta b f /\ (EvenClosest b beta (Zabs_nat p) r f) /\
exists f:Pff.float, (Fcanonic beta b f /\ (EvenClosest b beta (Zabs_nat p) r f) /\
FtoR beta f = round beta (FLT_exp (-dExp b) p) rndNE r).
intros r.
exists (RND_EvenClosest b beta (Zabs_nat p) r).
......@@ -613,7 +612,7 @@ Qed.
Lemma round_N_is_pff_round: forall choice, forall (r:R),
exists f:Float.float, (Fcanonic beta b f /\ (Closest b beta r f) /\
exists f:Pff.float, (Fcanonic beta b f /\ (Closest b beta r f) /\
FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r).
Proof.
intros choice r.
......@@ -650,7 +649,7 @@ apply RND_Max_correct; assumption.
rewrite pff_round_DN_is_round; fold d.
rewrite pff_round_UP_is_round; fold u.
apply Rmult_lt_reg_r with (/2)%R.
apply RlIt2.
apply pos_half_prf.
apply Rlt_le_trans with (1:=L).
right; simpl; field.
rewrite pff_round_N_is_round.
......@@ -682,7 +681,7 @@ apply RND_Max_correct; assumption.
rewrite pff_round_DN_is_round; fold d.
rewrite pff_round_UP_is_round; fold u.
apply Rmult_lt_reg_r with (/2)%R.
apply RlIt2.
apply pos_half_prf.
apply Rle_lt_trans with (2:=L).
right; simpl; field.
rewrite pff_round_N_is_round.
......@@ -696,7 +695,7 @@ Qed.
Lemma FloatFexp_gt: forall e f, Fbounded b f ->
(bpow beta (e+p) <= Rabs (FtoR beta f))%R ->
(e < Float.Fexp f)%Z.
(e < Pff.Fexp f)%Z.
Proof.
intros e f Ff H1.
apply lt_bpow with beta.
......@@ -770,7 +769,7 @@ apply is_Fzero_rep2 with beta; try assumption.
apply radix_gt_1.
(* f <> 0 *)
rewrite ulp_neq_0; try assumption.
replace (FtoR beta f) with (F2R (Float beta (Float.Fnum f) (Float.Fexp f))).
replace (FtoR beta f) with (F2R (Float beta (Pff.Fnum f) (Pff.Fexp f))).
rewrite <- pff_canonic_is_canonic; try assumption.
simpl; rewrite CanonicFulp; try assumption.
unfold FtoR; simpl; rewrite bpow_powerRZ; ring.
......@@ -788,7 +787,7 @@ Lemma Fulp_ulp: forall f, Fbounded b f ->
intros f H.
assert (Y1: (1 < beta)%Z) by apply radix_gt_1.
assert (Y2:Z.abs_nat p <> 0).
apply notEqLt.
apply sym_not_eq, Nat.lt_neq.
replace 0 with (Z.abs_nat 0) by easy.
apply Zabs_nat_lt; omega.
rewrite FulpComp with (q:=Fnormalize beta b (Z.abs_nat p) f); try assumption.
......@@ -807,7 +806,7 @@ End Equiv.
Section Equiv_instanc.
Lemma round_NE_is_pff_round_b32: forall (r:R),
exists f:Float.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\
exists f:Pff.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\
FtoR 2 f = round radix2 (FLT_exp (-149) 24) rndNE r).
Proof.
apply (round_NE_is_pff_round radix2 bsingle 24).
......@@ -817,7 +816,7 @@ Qed.
Lemma round_NE_is_pff_round_b64: forall (r:R),
exists f:Float.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\
exists f:Pff.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\
FtoR 2 f = round radix2 (FLT_exp (-1074) 53) rndNE r).
apply (round_NE_is_pff_round radix2 bdouble 53).
Proof.
......
Require Import Psatz.
Require Import Float.Veltkamp.
Require Import Float.RND.
Require Export Float.Fast2Sum.
Require Import Float.TwoSum.
Require Import Float.FmaErr.
Require Import Float.Dekker.
Require Import Float.FmaErrApprox.
Require Import Float.Axpy.
Require Import Float.discriminant.
Require Import Float.discriminant3.
From Flocq Require Import Core Plus_error Mult_error Operations Sterbenz.
Require Import Ftranslate_flocq2Pff.
From Flocq Require Import Pff Ftranslate_flocq2Pff.
Open Scope R_scope.
......@@ -68,10 +58,10 @@ destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
(* *)
pose (Iplus := fun (f g:Float.float) => RND_Closest
pose (Iplus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f + FtoR radix2 g)).
pose (Iminus := fun (f g:Float.float) => RND_Closest
pose (Iminus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f - FtoR radix2 g)).
assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
......@@ -97,7 +87,7 @@ now rewrite Zopp_involutive.
(* *)
assert (K: FtoR 2 (Iminus fy (Iminus (Iplus fx fy) fx)) =
FtoR 2 fx + FtoR 2 fy - FtoR 2 (Iplus fx fy)).
apply Fast2Sum.Dekker with (make_bound radix2 prec emin) (Zabs_nat prec); try assumption.
apply Pff.Dekker_FTS with (make_bound radix2 prec emin) (Zabs_nat prec); try assumption.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
......@@ -111,7 +101,8 @@ apply make_bound_p; omega.
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
apply notEqLt, lt_Zlt_inv.
apply sym_not_eq, Nat.lt_neq.
apply lt_Zlt_inv.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply FcanonicFopp.
......@@ -129,7 +120,7 @@ now rewrite round_N_opp_sym.
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
apply notEqLt, lt_Zlt_inv.
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply RND_Closest_canonic.
......@@ -144,7 +135,7 @@ rewrite H1,H2.
rewrite Fopp_correct.
f_equal; ring.
(* . *)
unfold Fast2Sum.FtoRradix.
unfold Pff.FtoRradix.
change 2%Z with (radix_val radix2).
rewrite Hfx, Hfy; assumption.
(* *)
......@@ -201,10 +192,10 @@ destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
(* *)
pose (Iplus := fun (f g:Float.float) => RND_Closest
pose (Iplus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f + FtoR radix2 g)).
pose (Iminus := fun (f g:Float.float) => RND_Closest
pose (Iminus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f - FtoR radix2 g)).
assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
......@@ -242,14 +233,14 @@ apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
(* . *)
unfold TwoSum.FtoRradix.
unfold FtoRradix.
intros p q r s Fp Fq Fr Fs M1 M2.
now rewrite 2!H1, M1, M2.
(* . *)
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
apply notEqLt, lt_Zlt_inv.
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply RND_Closest_canonic.
......@@ -265,7 +256,7 @@ now rewrite 2!H1, Rplus_comm.
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
apply notEqLt, lt_Zlt_inv.
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply FcanonicFopp.
......@@ -283,7 +274,7 @@ now rewrite round_N_opp_sym.
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
apply notEqLt, lt_Zlt_inv.
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply RND_Closest_canonic.
......@@ -344,7 +335,7 @@ Let tx:=round_flt (x-hx).
Lemma C_format: format (bpow s +1).
Proof with auto with typeclass_instances.
apply generic_format_FLT.
exists (Float beta (Zpower beta s+1)%Z 0%Z); simpl.
exists (Defs.Float beta (Zpower beta s+1)%Z 0%Z); simpl.
unfold F2R; simpl.
rewrite plus_IZR, IZR_Zpower; try omega.
simpl; ring.
......@@ -442,9 +433,11 @@ replace (Z.abs_nat (prec - s)) with (Z.abs_nat prec - Z.abs_nat s)%nat.
rewrite <- (p'GivesBound beta (make_bound beta prec emin) (Zabs_nat s) (Zabs_nat prec)) at 2.
simpl; easy.
apply radix_gt_1.
apply ZleLe; rewrite inj_abs; auto with zarith.
apply ZleLe; rewrite inj_minus, 2!inj_abs, Zmax_r; simpl; auto with zarith.
apply Nat2Z.inj.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite 2!inj_abs; omega.
rewrite inj_minus; repeat rewrite inj_abs; try omega.
apply Zmax_r; omega.
apply N2Z.inj.
rewrite H4.
rewrite Zabs2N.id_abs.
......@@ -521,7 +514,7 @@ exact H3.
apply Zpos_eq_iff.
apply trans_eq with (Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s)).
rewrite <- p''GivesBound with (b:=make_bound beta prec emin) at 2.
easy.
simpl; auto.
apply radix_gt_1.
rewrite Zpower_Zpower_nat,Z2Pos.id.
f_equal; apply sym_eq, Zabs2Nat.inj_sub; omega.
......@@ -599,7 +592,7 @@ rewrite <- Zsucc_pred.
apply inj_abs.
apply Zpower_NR0.
apply Zlt_le_weak; apply radix_gt_0.
apply notEqLt, lt_Zlt_inv.
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
rewrite inj_abs.
apply Zpower_nat_less.
apply radix_gt_1.
......@@ -627,11 +620,11 @@ Lemma underf_mult_aux:
Fbounded b x ->
Fbounded b y ->
(bpow beta (e + 2 * prec - 1)%Z <= Rabs (FtoR beta x * FtoR beta y)) ->
(e <= Float.Fexp x + Float.Fexp y)%Z.
(e <= Pff.Fexp x + Pff.Fexp y)%Z.
Proof.
intros e x y Fx Fy H.
assert (HH: forall z, Fbounded b z
-> Rabs (FtoR beta z) < bpow beta (Float.Fexp z + prec)).
-> Rabs (FtoR beta z) < bpow beta (Pff.Fexp z + prec)).
clear -precisionGt1 pGivesBound; intros z Hz.
unfold FtoR; rewrite <- bpow_powerRZ.
rewrite Rabs_mult, Rmult_comm.
......@@ -645,7 +638,7 @@ rewrite <- abs_IZR, <- IZR_Zpower;[idtac|omega].
apply IZR_lt.
apply Zlt_le_trans with (1:=T1).
rewrite Zpower_Zpower_nat; omega.
assert (e+2*prec-1 < (Float.Fexp x+prec) +(Float.Fexp y +prec))%Z; try omega.
assert (e+2*prec-1 < (Pff.Fexp x+prec) +(Pff.Fexp y +prec))%Z; try omega.
(* *)
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=H).
......@@ -662,7 +655,7 @@ Lemma underf_mult_aux':
Fbounded b x ->
Fbounded b y ->
(bpow beta (-dExp b + 2 * prec - 1)%Z <= Rabs (FtoR beta x * FtoR beta y)) ->
(-dExp b <= Float.Fexp x + Float.Fexp y)%Z.
(-dExp b <= Pff.Fexp x + Pff.Fexp y)%Z.
Proof.
intros.
now apply underf_mult_aux.
......@@ -904,11 +897,11 @@ assert (Z.div2 prec <= prec)%Z; try omega.
rewrite Z.div2_div; apply Zlt_le_weak.
apply Z_div_lt; omega.
(* *)
assert (D:(((- dExp (make_bound beta prec emin) <= Float.Fexp fx + Float.Fexp fy)%Z ->
assert (D:(((- dExp (make_bound beta prec emin) <= Pff.Fexp fx + Pff.Fexp fy)%Z ->
(FtoR beta fx * FtoR beta fy = FtoR beta fr + FtoR beta ft4)) /\
Rabs (FtoR beta fx * FtoR beta fy - (FtoR beta fr + FtoR beta ft4)) <=
7 / 2 * powerRZ beta (- dExp (make_bound beta prec emin)))).
apply Dekker.Dekker with (Zabs_nat prec) fpx fqx fhx ftx fpy fqy fhy fty
apply Dekker with (Zabs_nat prec) fpx fqx fhx ftx fpy fqy fhy fty
fx1y1 fx1y2 fx2y1 fx2y2 ft1 ft2 ft3; try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
......@@ -1224,7 +1217,7 @@ rewrite Hfbe1'', Hfr1''; apply Hff'.
rewrite Hfbe2; apply Hfga'.
apply FcanonicUnique with (4:=Hfr1) (precision:=Zabs_nat prec).
apply radix_gt_1.
apply notEqLt.
apply sym_not_eq, Nat.lt_neq.
apply absolu_lt_nz; omega.
apply make_bound_p; omega.
apply RND_Closest_canonic.
......@@ -1240,7 +1233,7 @@ apply make_bound_p; omega.
rewrite Hfu1'', Hfal1''; fold u1; fold alpha1.
apply FcanonicUnique with (4:=Hfbe1) (precision:=Zabs_nat prec).
apply radix_gt_1.
apply notEqLt.
apply sym_not_eq, Nat.lt_neq.
apply absolu_lt_nz; omega.
apply make_bound_p; omega.
apply RND_Closest_canonic.
......@@ -2180,11 +2173,10 @@ apply FcanonicBound with radix2; try assumption.
apply FcanonicBound with radix2; try assumption.
apply FcanonicBound with radix2; try assumption.
apply FcanonicBound with radix2; try assumption.
apply FcanonicBound with radix2; try assumption.
(* underflow *)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega.
assert (emin < Float.Fexp fd)%Z; try omega.
assert (emin < Pff.Fexp fd)%Z; try omega.
apply FloatFexp_gt with radix2 (make_bound radix2 prec emin) prec; try assumption.
apply make_bound_p; omega.
apply FcanonicBound with radix2; try assumption.
......@@ -2192,7 +2184,7 @@ rewrite Hfd.
apply U4_discri1; assumption.
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega.
assert (emin < Float.Fexp ft)%Z; try omega.
assert (emin < Pff.Fexp ft)%Z; try omega.
apply FloatFexp_gt with radix2 (make_bound radix2 prec emin) prec; try assumption.
apply make_bound_p; omega.
now apply FcanonicBound with radix2.
......@@ -2202,47 +2194,19 @@ apply bpow_le; omega.
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega.
rewrite inj_abs;[idtac|omega].
assert (emin +prec <= Float.Fexp fa +Float.Fexp fc)%Z; try omega.
apply underf_mult_aux with radix2 (make_bound radix2 prec emin) prec; try easy.
apply make_bound_p; omega.
rewrite Hfa, Hfc.
apply Rle_trans with (2:=U2 Zac).
apply bpow_le; omega.
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega.
rewrite inj_abs; try omega.
assert (emin +prec-1 < Float.Fexp fq)%Z; try omega.
apply FloatFexp_gt with radix2 (make_bound radix2 prec emin) prec; try assumption.
apply make_bound_p; omega.
now apply FcanonicBound with radix2.
rewrite Hfq''.
apply abs_round_ge_generic...
apply FLT_format_bpow...
omega.
apply Rle_trans with (2:=U2 Zac).
apply bpow_le; omega.
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega.
rewrite inj_abs;[idtac|omega].
assert (emin +prec <= Float.Fexp fb +Float.Fexp fb)%Z; try omega.
apply underf_mult_aux with radix2 (make_bound radix2 prec emin) prec; try easy.
apply make_bound_p; omega.
replace 2%Z with (radix_val radix2) by easy.
rewrite Hfb.
apply Rle_trans with (2:=U1 Zbb).
apply bpow_le; omega.
rewrite <- bpow_powerRZ.
apply bpow_le; simpl (radix_val radix2); omega.
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega.
rewrite inj_abs;[idtac|omega].
assert (emin +prec-1 < Float.Fexp fp)%Z; try omega.
apply FloatFexp_gt with radix2 (make_bound radix2 prec emin) prec; try assumption.
apply make_bound_p; omega.
now apply FcanonicBound with radix2.
rewrite Hfp''.
apply abs_round_ge_generic...
apply FLT_format_bpow...
omega.
apply Rle_trans with (2:=U1 Zbb).
apply bpow_le; omega.
replace 2%Z with (radix_val radix2) by easy.
rewrite Hfa, Hfc.
apply Rle_trans with (2:=U2 Zac).
rewrite <- bpow_powerRZ.
apply bpow_le; simpl (radix_val radix2); omega.
replace 2%Z with (radix_val radix2) by easy.
right; apply CanonicGeNormal with prec; try assumption.
apply make_bound_p; omega.
......
This source diff could not be displayed because it is too large. You can view the blob instead.
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