Commit c517cdec authored by BOLDO Sylvie's avatar BOLDO Sylvie
Browse files

Generalization (radix) of Translation PFF/Flocq + Veltkamp (1/2)

parent d38545f2
......@@ -26,11 +26,12 @@ Require Import Fappli_IEEE.
Section Bounds.
Variable beta : radix.
Variable p E:Z.
Hypothesis precisionNotZero : (1 < p)%Z.
Definition make_bound := Bound
(Z.to_pos (Zpower 2%Z p))
(Z.to_pos (Zpower beta p))
(Z.abs_N E).
Lemma make_bound_Emin: (E <= 0)%Z ->
......@@ -42,13 +43,13 @@ now apply Z.abs_neq.
Qed.
Lemma make_bound_p:
Zpos (vNum (make_bound))=(Zpower_nat 2 (Zabs_nat p)).
Zpos (vNum (make_bound))=(Zpower_nat beta (Zabs_nat p)).
Proof.
unfold make_bound, vNum; simpl.
rewrite Z2Pos.id.
apply Zpower_nat_Zpower.
omega.
generalize (Zpower_gt_0 radix2); simpl.
generalize (Zpower_gt_0 beta); simpl.
intros T; apply T.
omega.
Qed.
......@@ -57,14 +58,14 @@ Qed.
End Bounds.
Section b_Bounds.
Definition bsingle := make_bound 24 (-149)%Z.
Definition bsingle := make_bound radix2 24 (-149)%Z.
Lemma psGivesBound: Zpos (vNum bsingle) = Zpower_nat 2 24.
unfold bsingle; apply make_bound_p.
omega.
Qed.
Definition bdouble := make_bound 53 1074.
Definition bdouble := make_bound radix2 53 1074.
Lemma pdGivesBound: Zpos (vNum bdouble) = Zpower_nat 2 53.
unfold bdouble; apply make_bound_p.
......@@ -74,21 +75,22 @@ Qed.
End b_Bounds.
Section Equiv.
Variable beta: radix.
Variable b : Fbound.
Variable p : Z.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat 2%Z (Zabs_nat p).
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta (Zabs_nat p).
Hypothesis precisionNotZero : (1 < p)%Z.
Lemma pff_format_is_format: forall f, Fbounded b f ->
(generic_format radix2 (FLT_exp (-dExp b) p) (FtoR 2 f)).
(generic_format beta (FLT_exp (-dExp b) p) (FtoR beta f)).
intros f Hf.
apply generic_format_FLT; auto with zarith.
exists (Float radix2 (Float.Fnum f) (Float.Fexp f)).
exists (Float beta (Float.Fnum f) (Float.Fexp f)).
simpl; split.
unfold F2R, FtoR; simpl.
rewrite Z2R_IZR.
rewrite <- 2!Z2R_IZR.
rewrite bpow_powerRZ.
reflexivity.
split; destruct Hf.
......@@ -100,8 +102,8 @@ Qed.
Lemma format_is_pff_format: forall r,
(generic_format radix2 (FLT_exp (-dExp b) p) r)
-> exists f, FtoR 2 f = r /\ Fbounded b f.
(generic_format beta (FLT_exp (-dExp b) p) r)
-> exists f, FtoR beta f = r /\ Fbounded b f.
intros r Hr.
apply FLT_format_generic in Hr; auto with zarith.
destruct Hr as (f,(Hf1,(Hf2,Hf3))).
......@@ -110,7 +112,7 @@ rewrite Hf1.
unfold F2R, FtoR; simpl.
rewrite Z2R_IZR.
rewrite bpow_powerRZ.
reflexivity.
rewrite Z2R_IZR; reflexivity.
split.
apply Zlt_le_trans with (1:=Hf2).
rewrite pGivesBound.
......@@ -136,16 +138,16 @@ exists (Zneg p1); auto with zarith.
intros H; contradict H; auto.
Qed.
Lemma pff_canonic_is_canonic: forall f, Fcanonic 2 b f -> FtoR 2 f <> 0 ->
canonic radix2 (FLT_exp (- dExp b) p)
(Float radix2 (Float.Fnum f) (Float.Fexp f)).
Lemma pff_canonic_is_canonic: forall f, Fcanonic beta b f -> FtoR beta f <> 0 ->
canonic beta (FLT_exp (- dExp b) p)
(Float beta (Float.Fnum f) (Float.Fexp f)).
intros f Hf1 Hf2; unfold canonic; simpl.
assert (K:(F2R (Float radix2 (Float.Fnum f) (Float.Fexp f)) = FtoR 2 f)).
assert (K:(F2R (Float beta (Float.Fnum f) (Float.Fexp f)) = FtoR beta f)).
unfold FtoR, F2R; simpl.
rewrite bpow_powerRZ; rewrite Z2R_IZR; reflexivity.
rewrite bpow_powerRZ; rewrite <- 2!Z2R_IZR; reflexivity.
unfold canonic_exp, FLT_exp.
rewrite K.
destruct (ln_beta radix2 (FtoR 2 f)) as (e, He).
destruct (ln_beta beta (FtoR beta f)) as (e, He).
simpl; destruct Hf1.
(* . *)
destruct H as (H1,H2).
......@@ -154,13 +156,13 @@ 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].
apply trans_eq with (ln_beta radix2 (FtoR 2 f)).
apply trans_eq with (ln_beta beta (FtoR beta f)).
apply sym_eq; apply ln_beta_unique.
apply He; assumption.
apply ln_beta_unique.
rewrite <- K; unfold F2R; simpl.
rewrite Rabs_mult.
rewrite (Rabs_right (bpow radix2 (Float.Fexp f))).
rewrite (Rabs_right (bpow beta (Float.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.
......@@ -168,20 +170,21 @@ rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
(* .. *)
apply Rmult_le_reg_l with (Z2R radix2).
auto with real.
apply Rmult_le_reg_l with (Z2R beta).
replace 0%R with (Z2R 0) by reflexivity.
apply Z2R_lt.
apply radix_gt_0.
rewrite <- bpow_plus1.
replace (p-1+1)%Z with (Z_of_nat (Zabs_nat p)).
rewrite <- Z2R_Zpower_nat.
simpl; rewrite <- pGivesBound, 2!Z2R_IZR.
simpl; rewrite <- pGivesBound, 3!Z2R_IZR.
rewrite Rabs_Zabs.
replace 2%R with (IZR 2) by (simpl; ring).
rewrite <- mult_IZR.
apply IZR_le.
replace 2%Z with (Zabs 2).
rewrite <- (Zabs_eq (beta)).
rewrite <- Zabs.Zabs_Zmult.
assumption.
auto with zarith.
apply Zlt_le_weak; apply radix_gt_0.
rewrite inj_abs; try ring.
omega.
(* .. *)
......@@ -199,22 +202,26 @@ destruct H as (H1,(H2,H3)).
rewrite H2.
apply sym_eq; apply Zmax_right.
assert ((e-1) < p-dExp b)%Z;[idtac|omega].
apply lt_bpow with radix2.
apply Rle_lt_trans with (Rabs (FtoR 2 f)).
apply lt_bpow with beta.
apply Rle_lt_trans with (Rabs (FtoR beta f)).
apply He; auto.
apply Rlt_le_trans with (FtoR 2 (firstNormalPos 2 b (Zabs_nat p))).
apply Rlt_le_trans with (FtoR beta (firstNormalPos beta b (Zabs_nat p))).
rewrite <- Fabs_correct.
2: apply radix_gt_0.
apply FsubnormalLtFirstNormalPos; auto with zarith.
apply radix_gt_1.
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
apply FsubnormFabs; auto with zarith.
apply radix_gt_1.
split; [idtac|split]; assumption.
rewrite Fabs_correct; auto with real zarith.
auto with zarith.
apply radix_gt_0.
unfold firstNormalPos, FtoR, nNormMin.
simpl.
replace (IZR (Zpower_nat 2 (Peano.pred (Zabs_nat p)))) with (bpow radix2 (p-1)).
rewrite <- (bpow_powerRZ radix2).
replace (IZR (Zpower_nat beta (Peano.pred (Zabs_nat p)))) with (bpow beta (p-1)).
rewrite <- Z2R_IZR.
rewrite <- (bpow_powerRZ _).
rewrite <- bpow_plus.
apply bpow_le.
omega.
......@@ -229,22 +236,24 @@ Qed.
Lemma pff_round_NE_is_round: forall (r:R),
(FtoR 2 (RND_EvenClosest b 2 (Zabs_nat p) r)
= round radix2 (FLT_exp (-dExp b) p) rndNE r).
(FtoR beta (RND_EvenClosest b beta (Zabs_nat p) r)
= round beta (FLT_exp (-dExp b) p) rndNE r).
Proof.
intros.
assert (Rnd_NE_pt radix2 (FLT_exp (-dExp b) p) r
(round radix2 (FLT_exp (-dExp b) p) rndNE r)).
assert (Rnd_NE_pt beta (FLT_exp (-dExp b) p) r
(round beta (FLT_exp (-dExp b) p) rndNE r)).
apply round_NE_pt; auto with zarith.
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
apply exists_NE_FLT.
right; auto with zarith.
now right.
unfold Rnd_NE_pt, Rnd_NG_pt, Rnd_N_pt, NE_prop in H.
destruct H as ((H1,H2),H3).
destruct (format_is_pff_format _ H1) as (f,(Hf1,Hf2)).
rewrite <- Hf1.
generalize (EvenClosestUniqueP b 2 (Zabs_nat p)); unfold UniqueP; intros T.
generalize (EvenClosestUniqueP b beta (Zabs_nat p)); unfold UniqueP; intros T.
apply sym_eq; apply T with r; auto with zarith; clear T.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
split.
......@@ -254,37 +263,41 @@ rewrite Hf1.
apply H2.
apply pff_format_is_format; auto.
(* *)
case (Req_dec (FtoR 2 (Fnormalize 2 b (Zabs_nat p) f)) 0%R); intros L.
case (Req_dec (FtoR beta (Fnormalize beta b (Zabs_nat p) f)) 0%R); intros L.
left.
unfold FNeven, Feven, Even.
exists 0%Z.
rewrite Zmult_0_r.
apply eq_IZR.
apply Rmult_eq_reg_l with (powerRZ 2 (Float.Fexp (Fnormalize 2 b (Zabs_nat p) f)))%R.
apply Rmult_eq_reg_l with (powerRZ beta (Float.Fexp (Fnormalize beta b (Zabs_nat p) f)))%R.
simpl (IZR 0); rewrite Rmult_0_r.
rewrite <- L; unfold FtoR; simpl; ring.
apply powerRZ_NOR; auto with zarith real.
apply Rgt_not_eq; replace 0%R with (IZR 0) by reflexivity.
apply IZR_lt; apply radix_gt_0.
destruct H3.
(* . *)
destruct H as (g,(Hg1,(Hg2,Hg3))).
left.
unfold FNeven, Feven.
apply equiv_RNDs_aux.
replace (Float.Fnum (Fnormalize 2 b (Zabs_nat p) f)) with (Fnum g); try assumption.
replace g with (Float radix2 (Float.Fnum (Fnormalize 2 b (Zabs_nat p) f)) (Float.Fexp (Fnormalize 2 b (Zabs_nat p) f))).
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))).
easy.
apply canonic_unicity with (FLT_exp (- dExp b) p).
2: assumption.
apply pff_canonic_is_canonic.
apply FnormalizeCanonic; auto with zarith real.
apply radix_gt_1.
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
exact L.
rewrite <- Hg1, <- Hf1.
rewrite <- FnormalizeCorrect with 2%Z b (Zabs_nat p) f; auto with zarith.
rewrite <- FnormalizeCorrect with beta b (Zabs_nat p) f; auto with zarith.
unfold F2R, FtoR; simpl.
rewrite Z2R_IZR, bpow_powerRZ.
reflexivity.
rewrite Z2R_IZR; reflexivity.
apply radix_gt_1.
(* . *)
right; intros q (Hq1,Hq2).
rewrite Hf1.
......@@ -296,22 +309,25 @@ destruct (format_is_pff_format _ Hg) as (v,(Hv1,Hv2)).
rewrite <- Hv1.
apply Hq2; auto.
apply RND_EvenClosest_correct; auto with zarith.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
Qed.
Lemma round_NE_is_pff_round: forall (r:R),
exists f:Float.float, (Fcanonic 2 b f /\ (EvenClosest b 2 (Zabs_nat p) r f) /\
FtoR 2 f = round radix2 (FLT_exp (-dExp b) p) rndNE r).
exists f:Float.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 2 (Zabs_nat p) r).
exists (RND_EvenClosest b beta (Zabs_nat p) r).
split.
apply RND_EvenClosest_canonic; auto with zarith.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
split.
apply RND_EvenClosest_correct; auto with zarith.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply pff_round_NE_is_round.
......@@ -324,7 +340,7 @@ 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) /\
FtoR 2 f = round radix2 (FLT_exp (-149) 24) rndNE r).
apply (round_NE_is_pff_round bsingle 24).
apply (round_NE_is_pff_round radix2 bsingle 24).
apply psGivesBound.
omega.
Qed.
......@@ -333,7 +349,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) /\
FtoR 2 f = round radix2 (FLT_exp (-1074) 53) rndNE r).
apply (round_NE_is_pff_round bdouble 53).
apply (round_NE_is_pff_round radix2 bdouble 53).
apply pdGivesBound.
omega.
Qed.
......
......@@ -3,11 +3,173 @@ Require Import Fprop_plus_error.
Require Import Fprop_mult_error.
Require Import FmaErr.
Require Import Ftranslate_flocq2Pff.
Open Scope R_scope.
Section Veltkamp.
Variable beta : radix.
Variable emin prec : Z.
Variable s:Z.
Hypothesis precisionGe3 : (3 <= prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis emin_neg: (emin <= 0)%Z.
Notation format := (generic_format beta (FLT_exp emin prec)).
Notation round_flt :=(round beta (FLT_exp emin prec) ZnearestE).
Notation round_flt_s :=(round beta (FLT_exp emin (prec-s)) ZnearestE).
Notation ulp_flt :=(ulp beta (FLT_exp emin prec)).
Notation bpow e := (bpow beta e).
(** inputs *)
Hypothesis SLe: (2 <= s)%Z.
Hypothesis SGe: (s <= prec-2)%Z.
Variable x:R.
Hypothesis Fx: format x.
(** algorithm *)
Let p := round_flt (x*(bpow s+1)).
Let q:= round_flt (x-p).
Let hx:=round_flt (q+p).
Let tx:=round_flt (x-hx).
(** Theorems *)
Lemma precisionNotZero : (1 < prec)%Z.
omega.
Qed.
Lemma C_format: format (bpow s +1).
Proof with auto with typeclass_instances.
apply generic_format_FLT.
unfold FLT_format.
exists (Fcore_defs.Float beta (Zpower beta s+1)%Z 0%Z).
split; try split; simpl; try easy.
unfold F2R; simpl.
rewrite Z2R_plus, Z2R_Zpower; try omega.
simpl; ring.
rewrite Zabs_eq.
apply Zle_lt_trans with (beta^s+beta^0)%Z.
simpl; omega.
apply Zle_lt_trans with (beta^s+beta^s)%Z.
apply Zplus_le_compat_l.
apply Zpower_le; omega.
apply Zle_lt_trans with (2*beta^s)%Z.
omega.
apply Zle_lt_trans with (beta^1*beta^s)%Z.
apply Zmult_le_compat_r.
rewrite Z.pow_1_r.
apply Zle_bool_imp_le; apply beta.
apply Zpower_ge_0.
rewrite <- Zpower_plus; try omega.
apply Zpower_lt; omega.
apply Zle_trans with (beta^s)%Z; try omega.
apply Zpower_ge_0.
Qed.
Theorem Veltkamp_Even: hx = round_flt_s x.
Proof with auto with typeclass_instances.
destruct (format_is_pff_format beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x)
as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
(x*(bpow s+1)))
as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
(x-p))
as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
(q+p))
as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
(* *)
destruct VeltkampEven with beta (make_bound beta prec emin) (Zabs_nat s)
(Zabs_nat prec) fx fp fq fhx as (hx', (H1,H2)); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
replace 2%nat with (Zabs_nat 2) by easy.
apply Zabs_nat_le; omega.
apply Nat2Z.inj_le.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite inj_abs; simpl; omega.
rewrite Hfx; rewrite inj_abs; try omega.
rewrite bpow_powerRZ in Hfp'; rewrite Z2R_IZR in Hfp'; exact Hfp'.
rewrite Hfx, Hfp''; assumption.
rewrite Hfp'', Hfq''; assumption.
(* *)
unfold hx; rewrite <- Hfhx'', <- H1.
apply trans_eq with (FtoR beta (RND_EvenClosest
(make_bound beta (prec-s) emin) beta (Zabs_nat (prec-s)) x)).
generalize (EvenClosestUniqueP (make_bound beta (prec-s) emin) beta
(Zabs_nat (prec-s))); unfold UniqueP; intros T.
apply T with x; clear T.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
rewrite <- Hfx.
replace (Zabs_nat (prec-s)) with (Zabs_nat prec - Zabs_nat s)%nat.
replace (make_bound beta (prec - s) emin) with
(Bound (Pos.of_succ_nat
(Peano.pred
(Z.abs_nat
(Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s)))))
(dExp (make_bound beta prec emin))).
exact H2.
generalize (make_bound_Emin beta (prec-s) _ emin_neg).
generalize (make_bound_p beta (prec-s) emin).
destruct (make_bound beta (prec-s) emin) as (l1,l2).
simpl; intros H3 H4; f_equal.
apply Pos2Z.inj.
rewrite H3; try omega.
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 Nat2Z.inj.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite 2!inj_abs; omega.
apply N2Z.inj.
rewrite H4.
rewrite Zabs2N.id_abs.
now apply Z.abs_neq.
apply Nat2Z.inj.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite 2!inj_abs; omega.
apply RND_EvenClosest_correct.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
rewrite pff_round_NE_is_round; try omega.
f_equal; f_equal.
rewrite make_bound_Emin; omega.
apply make_bound_p; omega.
Qed.
Theorem Veltkamp_tail:
x = hx+tx /\ generic_format beta (FLT_exp emin s) tx.
Proof with auto with typeclass_instances.
TODO.
Qed.
End Veltkamp.
Section ErrFMA.
Variable emin prec : Z.
......
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