Commit de2f0164 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added a typeclass for positive precision.

parent 82d8d10e
......@@ -46,12 +46,12 @@ End AnyRadix.
Section Binary.
Variable prec emax : Z.
Hypothesis Hprec : (0 < prec)%Z.
Context (prec_gt_0_ : Prec_gt_0 prec).
Hypothesis Hmax : (prec < emax)%Z.
Let emin := (3 - emax - prec)%Z.
Let fexp := FLT_exp emin prec.
Instance fexp_correct : Valid_exp fexp := FLT_exp_valid _ _ Hprec.
Instance fexp_correct : Valid_exp fexp := FLT_exp_valid emin prec.
Definition bounded_prec m e :=
Zeq_bool (fexp (Z_of_nat (S (digits2_Pnat m)) + e)) e.
......@@ -335,8 +335,9 @@ rewrite <- abs_F2R.
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
unfold emin. clear -Hprec Hmax.
omega.
unfold emin.
generalize (prec_gt_0 prec).
clear -Hmax ; omega.
Qed.
Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }.
......@@ -678,12 +679,12 @@ rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
replace (digits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
unfold fexp, FLT_exp, emin.
clear -Hprec Hmax.
zify ; omega.
generalize (prec_gt_0 prec).
clear -Hmax ; zify ; omega.
change 2%Z with (radix_val radix2).
case_eq (Zpower radix2 prec - 1)%Z.
simpl digits.
generalize (Zpower_gt_1 radix2 _ Hprec).
generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)).
clear ; omega.
intros p Hp.
apply Zle_antisym.
......@@ -700,7 +701,7 @@ apply digits_le_Zpower.
simpl Zabs. rewrite <- Hp.
apply Zlt_pred.
intros p Hp.
generalize (Zpower_gt_1 radix2 _ Hprec).
generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)).
clear -Hp ; zify ; omega.
apply Rnot_lt_le.
intros Hx.
......@@ -780,7 +781,7 @@ unfold fexp, FLT_exp.
refine (_ (digits_mult_ge radix2 (Zpos mx) (Zpos my) _ _)) ; try discriminate.
refine (_ (digits_gt_0 radix2 (Zpos mx) _) (digits_gt_0 radix2 (Zpos my) _)) ; try discriminate.
generalize (digits radix2 (Zpos mx)) (digits radix2 (Zpos my)) (digits radix2 (Zpos mx * Zpos my)).
clear -Hprec Hmax.
clear -Hmax.
unfold emin.
intros dx dy dxy Hx Hy Hxy.
zify ; intros ; subst.
......@@ -1291,7 +1292,7 @@ rewrite Rlt_bool_true.
easy.
(* .. *)
rewrite Rabs_pos_eq.
refine (_ (relative_error_FLT_ex radix2 emin prec Hprec (round_mode m) (sqrt (F2R (Float radix2 (Zpos mx) ex))) _)).
refine (_ (relative_error_FLT_ex radix2 emin prec (prec_gt_0 prec) (round_mode m) (sqrt (F2R (Float radix2 (Zpos mx) ex))) _)).
fold fexp.
intros (eps, (Heps, Hr)).
rewrite Hr.
......@@ -1299,7 +1300,8 @@ assert (Heps': (Rabs eps < 1)%R).
apply Rlt_le_trans with (1 := Heps).
fold (bpow radix2 0).
apply bpow_le.
clear -Hprec. omega.
generalize (prec_gt_0 prec).
clear ; omega.
apply Rsqr_incrst_0.
3: apply bpow_ge_0.
rewrite Rsqr_mult.
......@@ -1322,8 +1324,8 @@ apply (Rabs_lt_inv _ _ Heps').
now apply (Z2R_le 0 2).
change 4%R with (bpow radix2 2).
apply bpow_le.
clear -Hprec Hmax.
omega.
generalize (prec_gt_0 prec).
clear -Hmax ; omega.
apply Rmult_le_pos.
apply sqrt_ge_0.
rewrite <- (Rplus_opp_r 1).
......@@ -1342,8 +1344,7 @@ unfold Rsqr.
rewrite <- bpow_plus.
apply bpow_le.
unfold emin.
clear -Hprec Hmax.
omega.
clear -Hmax ; omega.
apply generic_format_ge_bpow with fexp.
intros.
apply Zle_max_r.
......
......@@ -27,6 +27,10 @@ Section test.
Variable beta : radix.
Variable prec emin : Z.
Variable Hprec : (1 < prec)%Z.
Instance prec_gt_0_ : Prec_gt_0 prec.
unfold Prec_gt_0.
omega.
Qed.
Definition Fsqrt_FLT_ne (f : float beta) :=
let '(Float m e) := f in
......@@ -38,14 +42,10 @@ Definition Fsqrt_FLT_ne (f : float beta) :=
Theorem Fsqrt_FLT_ne_correct :
forall x,
Rnd_NE_pt beta (FLT_exp emin prec) (sqrt (F2R x)) (F2R (Fsqrt_FLT_ne x)).
Proof.
Proof with auto with typeclass_instances.
intros x.
replace (F2R (Fsqrt_FLT_ne x)) with (round beta (FLT_exp emin prec) rndNE (sqrt (F2R x))).
apply round_NE_pt.
apply FLT_exp_valid.
omega.
apply exists_NE_FLT.
now right.
apply round_NE_pt...
unfold Fsqrt_FLT_ne.
destruct x as (mx, ex).
generalize (Zle_cases mx 0).
......@@ -66,8 +66,7 @@ now rewrite sqrt_0.
generalize (Fsqrt_core_correct beta prec mx ex (Zgt_lt _ _ Hm)).
destruct (Fsqrt_core beta prec mx ex) as ((ms, es), ls).
intros (H1, H2).
assert (Hp : (0 < prec)%Z) by omega.
generalize (@round_trunc_NE_correct beta _ (FLT_exp_valid emin prec Hp) (sqrt (F2R (Float beta mx ex))) ms es ls).
generalize (round_trunc_NE_correct beta (FLT_exp emin prec) (sqrt (F2R (Float beta mx ex))) ms es ls).
destruct (truncate beta (FLT_exp emin prec) (ms, es, ls)) as ((mr, er), lr).
intros Hr. apply Hr. clear Hr.
apply sqrt_ge_0.
......
......@@ -34,7 +34,8 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable emin prec : Z.
Variable Hp : Zlt 0 prec.
Context { prec_gt_0_ : Prec_gt_0 prec }.
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
......@@ -48,23 +49,9 @@ Global Instance FLT_exp_valid : Valid_exp FLT_exp.
Proof.
intros k.
unfold FLT_exp.
destruct (Zmax_spec (k - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2.
split.
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
intros H0.
apply False_ind.
omega.
split.
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
split.
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
intros l H0.
generalize (Zmax_spec (l - prec) emin).
omega.
generalize (prec_gt_0 prec).
repeat split ;
intros ; zify ; omega.
Qed.
Theorem FLT_format_generic :
......@@ -237,12 +224,14 @@ rewrite <- F2R_bpow.
apply generic_format_canonic_exponent.
unfold generic_format, canonic_exponent, FLT_exp.
rewrite F2R_bpow, ln_beta_bpow.
assert (Hp := prec_gt_0 prec).
apply Zmax_lub ; omega.
assert (H2: generic_format beta (FIX_exp emin) (bpow (emin + prec))).
rewrite <- F2R_bpow.
apply generic_format_canonic_exponent.
unfold generic_format, canonic_exponent, FIX_exp.
omega.
generalize (prec_gt_0 prec).
clear ; omega.
destruct Rabs_eq_Rabs with (1 := Hx) as [H|H] ;
rewrite H ; clear H ;
split ; intros _ ;
......@@ -265,10 +254,8 @@ Qed.
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
Proof.
intros ex ey.
clear Hp.
unfold FLT_exp.
generalize (Zmax_spec (ex - prec) emin) (Zmax_spec (ey - prec) emin).
omega.
zify ; omega.
Qed.
(** and it allows a rounding to nearest, ties to even. *)
......
......@@ -33,7 +33,11 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Variable Hp : Zlt 0 prec.
Class Prec_gt_0 :=
prec_gt_0 : (0 < prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 }.
(* unbounded floating-point format *)
Definition FLX_format (x : R) :=
......@@ -48,6 +52,7 @@ Global Instance FLX_exp_valid : Valid_exp FLX_exp.
Proof.
intros k.
unfold FLX_exp.
generalize prec_gt_0.
repeat split ; intros ; omega.
Qed.
......@@ -198,7 +203,8 @@ ring_simplify (prec - d + (d - prec))%Z.
now rewrite Rmult_1_r, Z2R_abs.
apply bpow_ge_0.
exact H5.
omega.
generalize prec_gt_0.
clear ; omega.
apply lt_Z2R.
rewrite Z2R_abs, Z2R_mult, Rabs_mult.
rewrite 2!Z2R_Zpower.
......
......@@ -32,7 +32,8 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable emin prec : Z.
Variable Hp : Zlt 0 prec.
Context { prec_gt_0_ : Prec_gt_0 prec }.
(* floating-point format with abrupt underflow *)
Definition FTZ_format (x : R) :=
......@@ -56,6 +57,7 @@ generalize (Zlt_cases (emin + prec + 1 - prec) emin).
case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3.
omega.
generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin).
generalize (prec_gt_0 prec).
case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega.
intros l H3.
generalize (Zlt_cases (l - prec) emin).
......@@ -63,6 +65,7 @@ case (Zlt_bool (l - prec) emin) ; omega.
split ; intros H2.
generalize (Zlt_cases (k + 1 - prec) emin).
case (Zlt_bool (k + 1 - prec) emin) ; omega.
generalize (prec_gt_0 prec).
split ; intros ; omega.
Qed.
......@@ -183,18 +186,16 @@ Theorem FTZ_format_FLXN :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
( FTZ_format x <-> FLXN_format beta prec x ).
Proof.
Proof with auto with typeclass_instances.
intros x Hx.
split.
(* . *)
destruct (Req_dec x 0) as [H4|H4].
intros _.
rewrite H4.
apply -> FLX_format_FLXN.
apply <- FLX_format_generic.
apply -> FLX_format_FLXN...
apply <- FLX_format_generic...
apply generic_format_0.
exact Hp.
exact Hp.
intros ((xm,xe),(H1,(H2,H3))).
specialize (H2 H4).
rewrite H1.
......@@ -321,7 +322,8 @@ apply bpow_ge_0.
apply Rle_trans with (2 := proj1 He).
apply bpow_le.
unfold FLX_exp.
omega.
generalize (prec_gt_0 prec).
clear -He' ; omega.
apply bpow_ge_0.
unfold FLX_exp, FTZ_exp.
generalize (Zlt_cases (ex - prec) emin).
......
......@@ -28,7 +28,7 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Variable Hp : Zlt 0 prec.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
......@@ -92,7 +92,7 @@ now apply FLX_exp_valid.
unfold Rminus; apply format_add with fx (Fopp beta (Fmult beta fr fy)); trivial.
now rewrite Fopp_F2R,mult_F2R, <- Hr1, <- Hy1.
(* *)
destruct (relative_error_FLX_ex beta prec Hp Zrnd (x / y)%R) as (eps,(Heps1,Heps2)).
destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) Zrnd (x / y)%R) as (eps,(Heps1,Heps2)).
apply Rmult_integral_contrapositive_currified.
exact Zx.
now apply Rinv_neq_0_compat.
......@@ -106,7 +106,8 @@ now apply Rabs_pos_lt.
apply Rlt_le_trans with (1 := Heps1).
change R1 with (bpow 0).
apply bpow_le.
clear -Hp. omega.
generalize (prec_gt_0 prec).
clear ; omega.
rewrite Rmult_1_r.
rewrite Hx2.
unfold canonic_exponent.
......@@ -180,7 +181,7 @@ unfold Rsqr; now rewrite Fopp_F2R,mult_F2R, <- Hr1.
apply Rle_lt_trans with x.
apply Rabs_Rminus_pos.
apply Rle_0_sqr.
destruct (relative_error_N_FLX_ex beta prec Hp choice (sqrt x)) as (eps,(Heps1,Heps2)).
destruct (relative_error_N_FLX_ex beta prec (prec_gt_0 prec) choice (sqrt x)) as (eps,(Heps1,Heps2)).
rewrite Heps2.
rewrite Rsqr_mult, Rsqr_sqrt, Rmult_comm. 2: now apply Rlt_le.
apply Rmult_le_compat_r.
......
......@@ -27,7 +27,7 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Variable Hp : Zlt 0 prec.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
......@@ -86,7 +86,9 @@ unfold canonic_exponent, FLX_exp.
rewrite ln_beta_unique with (1 := Hex).
rewrite ln_beta_unique with (1 := Hey).
rewrite ln_beta_unique with (1 := Hexy).
cut ((ex - 1) + (ey - 1) < exy)%Z. omega.
cut ((ex - 1) + (ey - 1) < exy)%Z.
generalize (prec_gt_0 prec).
clear ; omega.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 Hexy).
rewrite Rabs_mult.
......@@ -160,7 +162,7 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable emin prec : Z.
Variable Hp : Zlt 0 prec.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Variable Hpemin: (emin <= prec)%Z.
Notation format := (generic_format beta (FLT_exp emin prec)).
......@@ -186,17 +188,18 @@ rewrite Hxy.
rewrite round_0.
ring_simplify (0 - 0)%R.
apply generic_format_0.
destruct (mult_error_FLX_aux beta prec Hp rnd x y) as ((m,e),(H1,(H2,H3))).
destruct (mult_error_FLX_aux beta prec rnd x y) as ((m,e),(H1,(H2,H3))).
now apply FLX_generic_format_FLT with emin.
now apply FLX_generic_format_FLT with emin.
rewrite <- (FLT_round_FLX beta emin).
assumption.
apply Rle_trans with (2:=Hxy).
apply bpow_le.
omega.
generalize (prec_gt_0 prec).
clear ; omega.
rewrite <- (FLT_round_FLX beta emin) in H1.
2:apply Rle_trans with (2:=Hxy).
2:apply bpow_le; omega.
2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega.
unfold f; rewrite <- H1.
apply generic_format_canonic_exponent.
simpl in H2, H3.
......
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