510 lines
17 KiB
Diff
510 lines
17 KiB
Diff
--- ./lib/coq/WhyFloats.v.orig 2011-10-24 09:21:06.000000000 -0600
|
|
+++ ./lib/coq/WhyFloats.v 2012-01-11 15:41:08.873131034 -0700
|
|
@@ -19,17 +19,13 @@ Let emin := (3 - emax - prec)%Z.
|
|
Let fexp := FLT_exp emin prec.
|
|
Lemma Hprec': (0 < prec)%Z. revert Hprec. now case Zlt_bool_spec. Qed.
|
|
Lemma Hemax': (prec < emax)%Z. revert Hemax. now case Zlt_bool_spec. Qed.
|
|
-Let binary_round_correct := binary_round_sign_shl_correct prec emax Hprec' Hemax'.
|
|
+Lemma fexp': Valid_exp fexp. apply FLT_exp_valid. apply Hprec'. Qed.
|
|
|
|
Definition r_to_sd rnd x : binary_float prec emax :=
|
|
let r := round radix2 fexp (round_mode rnd) x in
|
|
let m := Ztrunc (scaled_mantissa radix2 fexp r) in
|
|
- let e := canonic_exponent radix2 fexp r in
|
|
- match m with
|
|
- | Z0 => B754_zero prec emax false
|
|
- | Zpos m => FF2B _ _ _ (proj1 (binary_round_correct rnd false m e))
|
|
- | Zneg m => FF2B _ _ _ (proj1 (binary_round_correct rnd true m e))
|
|
- end.
|
|
+ let e := canonic_exp radix2 fexp r in
|
|
+ binary_normalize prec emax Hprec' Hemax' rnd m e false.
|
|
|
|
Lemma is_finite_FF2B :
|
|
forall f H,
|
|
@@ -49,59 +45,19 @@ Theorem r_to_sd_correct :
|
|
(Rabs r < bpow radix2 emax)%R ->
|
|
is_finite prec emax (r_to_sd rnd x) = true /\
|
|
r_to_sd rnd x = r :>R.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros rnd x r Bx.
|
|
unfold r_to_sd. fold r.
|
|
-assert (Gx: generic_format radix2 fexp r).
|
|
-apply generic_format_round.
|
|
-apply FLT_exp_correct.
|
|
-exact Hprec'.
|
|
-assert (Hr: Z2R (Ztrunc (scaled_mantissa radix2 fexp r)) = scaled_mantissa radix2 fexp r).
|
|
-apply sym_eq.
|
|
-now apply scaled_mantissa_generic.
|
|
-revert Hr.
|
|
-case_eq (Ztrunc (scaled_mantissa radix2 fexp r)).
|
|
-(* *)
|
|
-intros _ Hx.
|
|
-repeat split.
|
|
-apply Rmult_eq_reg_r with (bpow radix2 (- canonic_exponent radix2 fexp r)).
|
|
-now rewrite Rmult_0_l.
|
|
-apply Rgt_not_eq.
|
|
-apply bpow_gt_0.
|
|
-(* *)
|
|
-intros p Hp Hx.
|
|
-case binary_round_correct ; intros Hv.
|
|
-unfold F2R, Fnum, Fexp, cond_Zopp.
|
|
-rewrite Hx, scaled_mantissa_bpow.
|
|
-rewrite round_generic with (1 := Gx).
|
|
-rewrite Rlt_bool_true with (1 := Bx).
|
|
-intros H.
|
|
-split.
|
|
-rewrite is_finite_FF2B.
|
|
-revert H.
|
|
-assert (0 <> r)%R.
|
|
-intros H.
|
|
-rewrite <- H, scaled_mantissa_0 in Hx.
|
|
-now apply (Z2R_neq 0 (Zpos p)).
|
|
-now case binary_round_sign_shl.
|
|
-now rewrite B2R_FF2B.
|
|
-(* *)
|
|
-intros p Hp Hx.
|
|
-case binary_round_correct ; intros Hv.
|
|
-unfold F2R, Fnum, Fexp, cond_Zopp, Zopp.
|
|
-rewrite Hx, scaled_mantissa_bpow.
|
|
-rewrite round_generic with (1 := Gx).
|
|
+generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
|
|
+unfold r.
|
|
+elim generic_format_round...
|
|
+fold emin r.
|
|
+rewrite round_generic...
|
|
rewrite Rlt_bool_true with (1 := Bx).
|
|
-intros H.
|
|
-split.
|
|
-rewrite is_finite_FF2B.
|
|
-revert H.
|
|
-assert (0 <> r)%R.
|
|
-intros H.
|
|
-rewrite <- H, scaled_mantissa_0 in Hx.
|
|
-now apply (Z2R_neq 0 (Zneg p)).
|
|
-now case binary_round_sign_shl.
|
|
-now rewrite B2R_FF2B.
|
|
+now split.
|
|
+apply generic_format_round...
|
|
+apply fexp'.
|
|
+apply fexp'.
|
|
Qed.
|
|
|
|
Theorem r_to_sd_format :
|
|
@@ -109,15 +65,14 @@ Theorem r_to_sd_format :
|
|
FLT_format radix2 emin prec x ->
|
|
(Rabs x < bpow radix2 emax)%R ->
|
|
r_to_sd rnd x = x :>R.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros rnd x Fx Bx.
|
|
assert (Gx: generic_format radix2 fexp x).
|
|
-apply -> FLT_format_generic.
|
|
+apply generic_format_FLT.
|
|
apply Fx.
|
|
-exact Hprec'.
|
|
-pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (1 := Gx).
|
|
+pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
|
|
refine (proj2 (r_to_sd_correct _ _ _)).
|
|
-now rewrite round_generic with (1 := Gx).
|
|
+rewrite round_generic...
|
|
Qed.
|
|
|
|
End r_to_sd.
|
|
@@ -152,10 +107,10 @@ rewrite <- Zsucc_pred.
|
|
generalize (Zeq_bool_eq _ _ H1). clear.
|
|
rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
|
|
intros H.
|
|
-apply (Fcalc_digits.Zpower_gt_digits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
|
|
+apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
|
|
revert H.
|
|
unfold FLT_exp.
|
|
-generalize (Fcalc_digits.digits Fcalc_digits.radix2 (Zpos m)).
|
|
+generalize (Fcore_digits.Zdigits Fcalc_digits.radix2 (Zpos m)).
|
|
intros ; zify ; omega.
|
|
apply bpow_le.
|
|
now apply Zle_bool_imp_le.
|
|
@@ -172,6 +127,23 @@ Definition rnd_of_mode (m:mode) :=
|
|
|
|
(** Single precision *)
|
|
|
|
+Definition binary32 := binary_float 24 128.
|
|
+
|
|
+Let Hprec32 : (0 < 24)%Z.
|
|
+apply refl_equal.
|
|
+Qed.
|
|
+
|
|
+Let Hprec32_emax : (24 < 128)%Z.
|
|
+apply refl_equal.
|
|
+Qed.
|
|
+
|
|
+Definition b32_opp := Bopp 24 128.
|
|
+Definition b32_plus := Bplus _ _ Hprec32 Hprec32_emax.
|
|
+Definition b32_minus := Bminus _ _ Hprec32 Hprec32_emax.
|
|
+Definition b32_mult := Bmult _ _ Hprec32 Hprec32_emax.
|
|
+Definition b32_div := Bdiv _ _ Hprec32 Hprec32_emax.
|
|
+Definition b32_sqrt := Bsqrt _ _ Hprec32 Hprec32_emax.
|
|
+
|
|
Record single : Set := mk_single {
|
|
single_float : binary32;
|
|
single_value := (single_float : R);
|
|
@@ -229,12 +201,12 @@ Theorem bounded_real_no_overflow_single
|
|
forall m x,
|
|
(Rabs x <= max_single)%R ->
|
|
no_overflow_single m x.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros m x Hx.
|
|
apply Rabs_le.
|
|
assert (generic_format radix2 (FLT_exp (-149) 24) max_single).
|
|
-apply generic_format_canonic_exponent.
|
|
-unfold canonic_exponent.
|
|
+apply generic_format_F2R.
|
|
+unfold canonic_exp.
|
|
rewrite ln_beta_F2R. 2: easy.
|
|
rewrite (ln_beta_unique _ _ 24).
|
|
easy.
|
|
@@ -245,31 +217,40 @@ now apply Z2R_lt.
|
|
generalize (Rabs_le_inv _ _ Hx).
|
|
split.
|
|
erewrite <- round_generic with (x := Ropp max_single).
|
|
-apply round_monotone with (2 := proj1 H0).
|
|
-now apply FLT_exp_correct.
|
|
+unfold round_single.
|
|
+apply round_le...
|
|
+apply FLT_exp_valid. easy.
|
|
+easy.
|
|
+apply valid_rnd_round_mode.
|
|
now apply generic_format_opp.
|
|
-rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
|
|
-apply round_monotone with (2 := proj2 H0).
|
|
-now apply FLT_exp_correct.
|
|
+unfold round_single.
|
|
+apply round_le_generic...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'...
|
|
+easy.
|
|
Qed.
|
|
|
|
Theorem round_single_monotonic :
|
|
forall m x y, (x <= y)%R ->
|
|
(round_single m x <= round_single m y)%R.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros m x y Hxy.
|
|
-apply round_monotone with (2 := Hxy).
|
|
-now apply FLT_exp_correct.
|
|
+unfold round_single.
|
|
+apply round_le...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'...
|
|
Qed.
|
|
|
|
Theorem round_single_idempotent :
|
|
forall m1 m2 x,
|
|
round_single m1 (round_single m2 x) = round_single m2 x.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros m1 m2 x.
|
|
apply round_generic.
|
|
-apply generic_format_round.
|
|
-now apply FLT_exp_correct.
|
|
+apply valid_rnd_round_mode.
|
|
+apply generic_format_round...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'...
|
|
Qed.
|
|
|
|
Theorem round_down_single_neg :
|
|
@@ -295,8 +276,9 @@ Theorem round_single_down_le :
|
|
(round_single down x <= x)%R.
|
|
Proof.
|
|
intros x.
|
|
-eapply round_DN_pt.
|
|
-now apply FLT_exp_correct.
|
|
+eapply round_DN_pt...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'. easy.
|
|
Qed.
|
|
|
|
Theorem round_up_single_ge :
|
|
@@ -305,12 +287,30 @@ Theorem round_up_single_ge :
|
|
Proof.
|
|
intros x.
|
|
apply Rle_ge.
|
|
-eapply round_UP_pt.
|
|
-now apply FLT_exp_correct.
|
|
+eapply round_UP_pt...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'. easy.
|
|
Qed.
|
|
|
|
(** Double precision *)
|
|
|
|
+Definition binary64 := binary_float 53 1024.
|
|
+
|
|
+Let Hprec64 : (0 < 53)%Z.
|
|
+apply refl_equal.
|
|
+Qed.
|
|
+
|
|
+Let Hprec64_emax : (53 < 1024)%Z.
|
|
+apply refl_equal.
|
|
+Qed.
|
|
+
|
|
+Definition b64_opp := Bopp 53 1024.
|
|
+Definition b64_plus := Bplus _ _ Hprec64 Hprec64_emax.
|
|
+Definition b64_minus := Bminus _ _ Hprec64 Hprec64_emax.
|
|
+Definition b64_mult := Bmult _ _ Hprec64 Hprec64_emax.
|
|
+Definition b64_div := Bdiv _ _ Hprec64 Hprec64_emax.
|
|
+Definition b64_sqrt := Bsqrt _ _ Hprec64 Hprec64_emax.
|
|
+
|
|
Record double : Set := mk_double {
|
|
double_float : binary64;
|
|
double_value := (double_float : R);
|
|
@@ -368,12 +368,12 @@ Theorem bounded_real_no_overflow_double
|
|
forall m x,
|
|
(Rabs x <= max_double)%R ->
|
|
no_overflow_double m x.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros m x Hx.
|
|
apply Rabs_le.
|
|
assert (generic_format radix2 (FLT_exp (-1074) 53) max_double).
|
|
-apply generic_format_canonic_exponent.
|
|
-unfold canonic_exponent.
|
|
+apply generic_format_F2R.
|
|
+unfold canonic_exp.
|
|
rewrite ln_beta_F2R. 2: easy.
|
|
rewrite (ln_beta_unique _ _ 53).
|
|
easy.
|
|
@@ -384,31 +384,40 @@ now apply Z2R_lt.
|
|
generalize (Rabs_le_inv _ _ Hx).
|
|
split.
|
|
erewrite <- round_generic with (x := Ropp max_double).
|
|
-apply round_monotone with (2 := proj1 H0).
|
|
-now apply FLT_exp_correct.
|
|
+unfold round_double.
|
|
+apply round_le...
|
|
+apply FLT_exp_valid. easy.
|
|
+easy.
|
|
+apply valid_rnd_round_mode.
|
|
now apply generic_format_opp.
|
|
-rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
|
|
-apply round_monotone with (2 := proj2 H0).
|
|
-now apply FLT_exp_correct.
|
|
+unfold round_double.
|
|
+apply round_le_generic...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'...
|
|
+easy.
|
|
Qed.
|
|
|
|
Theorem round_double_monotonic :
|
|
forall m x y, (x <= y)%R ->
|
|
(round_double m x <= round_double m y)%R.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros m x y Hxy.
|
|
-apply round_monotone with (2 := Hxy).
|
|
-now apply FLT_exp_correct.
|
|
+unfold round_double.
|
|
+apply round_le...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'...
|
|
Qed.
|
|
|
|
Theorem round_double_idempotent :
|
|
forall m1 m2 x,
|
|
round_double m1 (round_double m2 x) = round_double m2 x.
|
|
-Proof.
|
|
+Proof with auto with typeclass_instances.
|
|
intros m1 m2 x.
|
|
apply round_generic.
|
|
-apply generic_format_round.
|
|
-now apply FLT_exp_correct.
|
|
+apply valid_rnd_round_mode.
|
|
+apply generic_format_round...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'...
|
|
Qed.
|
|
|
|
Theorem round_down_double_neg :
|
|
@@ -434,8 +443,9 @@ Theorem round_double_down_le :
|
|
(round_double down x <= x)%R.
|
|
Proof.
|
|
intros x.
|
|
-eapply round_DN_pt.
|
|
-now apply FLT_exp_correct.
|
|
+eapply round_DN_pt...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'. easy.
|
|
Qed.
|
|
|
|
Theorem round_up_double_ge :
|
|
@@ -444,8 +454,9 @@ Theorem round_up_double_ge :
|
|
Proof.
|
|
intros x.
|
|
apply Rle_ge.
|
|
-eapply round_UP_pt.
|
|
-now apply FLT_exp_correct.
|
|
+eapply round_UP_pt...
|
|
+apply FLT_exp_valid.
|
|
+apply Hprec'. easy.
|
|
Qed.
|
|
|
|
(** Quad precision *)
|
|
@@ -566,8 +577,8 @@ unfold F2R. simpl.
|
|
split.
|
|
now rewrite Rmult_1_r.
|
|
now split.
|
|
-apply <- FLT_format_generic.
|
|
-2: easy.
|
|
+apply FLT_format_generic.
|
|
+apply Hprec'. easy.
|
|
change 2%Z with (radix_val radix2) in Bz.
|
|
destruct z as [|z|z] ; unfold Zabs in Bz.
|
|
apply generic_format_0.
|
|
--- ./lib/coq/WhyFloatsStrict.v.orig 2011-10-24 09:21:06.000000000 -0600
|
|
+++ ./lib/coq/WhyFloatsStrict.v 2012-01-11 15:42:11.453663887 -0700
|
|
@@ -155,30 +155,13 @@ repeat split.
|
|
exact H2.
|
|
Qed.
|
|
|
|
-Axiom Bplus_correct : (* the statement from Flocq 1.4 is not strong enough;
|
|
- the axiom can be removed once the library is converted to Flocq 2.0 *)
|
|
- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
|
|
- (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
|
|
- is_finite prec emax x = true ->
|
|
- is_finite prec emax y = true ->
|
|
- if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
|
|
- (B2R prec emax x + B2R prec emax y))) (bpow radix2 emax)
|
|
- then
|
|
- B2R prec emax (Bplus prec emax Hprec Hmax m x y) =
|
|
- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x + B2R prec emax y) /\
|
|
- is_finite prec emax (Bplus prec emax Hprec Hmax m x y) = true
|
|
- else
|
|
- B2FF prec emax (Bplus prec emax Hprec Hmax m x y) =
|
|
- binary_overflow prec emax m (Bsign prec emax x) /\
|
|
- Bsign prec emax x = Bsign prec emax y.
|
|
-
|
|
Lemma add_single_specification :
|
|
forall m (x y : single),
|
|
no_overflow_single m (single_value x + single_value y) ->
|
|
exists z, add_single_post m x y z.
|
|
Proof.
|
|
intros m x y Br.
|
|
-refine (_ (Bplus_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y)
|
|
+refine (_ (Bplus_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y)
|
|
(single_finite x) (single_finite y))).
|
|
rewrite Rlt_bool_true.
|
|
2: now apply no_overflow_single_bounded.
|
|
@@ -189,27 +172,13 @@ repeat split.
|
|
exact H1.
|
|
Qed.
|
|
|
|
-Axiom Bmult_correct : (* the statement from Flocq 1.4 is not strong enough;
|
|
- the axiom can be removed once the library is converted to Flocq 2.0 *)
|
|
- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
|
|
- (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
|
|
- if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
|
|
- (B2R prec emax x * B2R prec emax y))) (bpow radix2 emax)
|
|
- then
|
|
- B2R prec emax (Bmult prec emax Hprec Hmax m x y) =
|
|
- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x * B2R prec emax y) /\
|
|
- is_finite prec emax (Bmult prec emax Hprec Hmax m x y) = andb (is_finite prec emax x) (is_finite prec emax y)
|
|
- else
|
|
- B2FF prec emax (Bmult prec emax Hprec Hmax m x y) =
|
|
- binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
|
|
-
|
|
Lemma mul_single_specification :
|
|
forall m (x y : single),
|
|
no_overflow_single m (single_value x * single_value y) ->
|
|
exists z, mul_single_post m x y z.
|
|
Proof.
|
|
intros m x y Br.
|
|
-refine (_ (Bmult_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y))).
|
|
+refine (_ (Bmult_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y))).
|
|
rewrite Rlt_bool_true.
|
|
2: now apply no_overflow_single_bounded.
|
|
fold b32_mult.
|
|
@@ -220,28 +189,13 @@ repeat split.
|
|
exact H1.
|
|
Qed.
|
|
|
|
-Axiom Bdiv_correct : (* the statement from Flocq 1.4 is not strong enough;
|
|
- the axiom can be removed once the library is converted to Flocq 2.0 *)
|
|
- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
|
|
- (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
|
|
- B2R prec emax y <> 0%R ->
|
|
- if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
|
|
- (B2R prec emax x / B2R prec emax y))) (bpow radix2 emax)
|
|
- then
|
|
- B2R prec emax (Bdiv prec emax Hprec Hmax m x y) =
|
|
- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x / B2R prec emax y) /\
|
|
- is_finite prec emax (Bdiv prec emax Hprec Hmax m x y) = is_finite prec emax x
|
|
- else
|
|
- B2FF prec emax (Bdiv prec emax Hprec Hmax m x y) =
|
|
- binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
|
|
-
|
|
Lemma div_single_specification :
|
|
forall m (x y : single), single_value y <> R0 ->
|
|
no_overflow_single m (single_value x / single_value y) ->
|
|
exists z, div_single_post m x y z.
|
|
Proof.
|
|
intros m x y Zy Br.
|
|
-refine (_ (Bdiv_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y) Zy)).
|
|
+refine (_ (Bdiv_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y) Zy)).
|
|
rewrite Rlt_bool_true.
|
|
2: now apply no_overflow_single_bounded.
|
|
fold b32_div.
|
|
@@ -252,20 +206,12 @@ repeat split.
|
|
exact H1.
|
|
Qed.
|
|
|
|
-Axiom Bsqrt_correct : (* the statement from Flocq 1.4 is not strong enough;
|
|
- the axiom can be removed once the library is converted to Flocq 2.0 *)
|
|
- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
|
|
- (m : Fappli_IEEE.mode) (x : binary_float prec emax),
|
|
- B2R prec emax (Bsqrt prec emax Hprec Hmax m x) =
|
|
- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (sqrt (B2R prec emax x)) /\
|
|
- is_finite prec emax (Bsqrt prec emax Hprec Hmax m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end.
|
|
-
|
|
Lemma sqrt_single_specification :
|
|
forall m (x : single), Rle 0 (single_value x) ->
|
|
exists z, sqrt_single_post m x z.
|
|
Proof.
|
|
intros m x Zx.
|
|
-refine (_ (Bsqrt_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x))).
|
|
+refine (_ (Bsqrt_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x))).
|
|
fold b32_sqrt.
|
|
intros (H1, H2).
|
|
assert (is_finite 24 128 (b32_sqrt (rnd_of_mode m) (single_float x)) = true).
|
|
--- ./lib/coq/JessieGappa.v.orig 2011-10-24 09:21:06.000000000 -0600
|
|
+++ ./lib/coq/JessieGappa.v 2012-01-11 15:41:08.874131235 -0700
|
|
@@ -571,7 +571,7 @@ unfold min_gen_float, min_float2.
|
|
case F ; apply bpow_gt_0.
|
|
rewrite <- round_of_min_gen with F m.
|
|
revert Bx1.
|
|
-case F ; apply round_monotone ; now apply FLT_exp_correct.
|
|
+case F ; apply round_le...
|
|
Save.
|
|
|
|
Lemma negative_constant : forall f m x,
|
|
@@ -592,7 +592,7 @@ case F ; apply bpow_ge_0.
|
|
apply Rle_lt_trans with (- min_gen_float F)%R.
|
|
rewrite <- round_of_opp_min_gen with F m.
|
|
revert Bx2.
|
|
-case F ; apply round_monotone ; now apply FLT_exp_correct.
|
|
+case F ; apply round_le...
|
|
apply Ropp_lt_gt_0_contravar.
|
|
unfold min_gen_float, min_float2.
|
|
case F ; apply bpow_gt_0.
|
|
@@ -602,7 +602,7 @@ Lemma round_increasing: forall f m x y,
|
|
(x <= y)%R -> (round_float f m x <= round_float f m y)%R.
|
|
Proof.
|
|
intros F m x y.
|
|
-case F ; apply round_monotone ; now apply FLT_exp_correct.
|
|
+case F ; apply round_le...
|
|
Save.
|
|
|
|
Lemma round_greater_min: forall f m x,
|