Commit 9004703e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Simplified proofs.

parent 562147cc
...@@ -92,76 +92,45 @@ rewrite <- Ropp_mult_distr_l_reverse. ...@@ -92,76 +92,45 @@ rewrite <- Ropp_mult_distr_l_reverse.
now rewrite opp_Z2R. now rewrite opp_Z2R.
Qed. Qed.
Theorem F2R_prec_normalize_pos : Theorem F2R_change_exp :
forall e' m e : Z,
(e' <= e)%Z ->
F2R (Float beta m e) = F2R (Float beta (m * Zpower (radix_val beta) (e - e')) e').
Proof.
intros e' m e He.
unfold F2R. simpl.
rewrite mult_Z2R, Z2R_Zpower, Rmult_assoc.
apply f_equal.
pattern e at 1 ; replace e with (e - e' + e')%Z by ring.
apply epow_add.
now apply Zle_minus_le_0.
Qed.
Theorem F2R_prec_normalize :
forall m e e' p : Z, forall m e e' p : Z,
(Zabs m < Zpower (radix_val beta) p)%Z -> (Zabs m < Zpower (radix_val beta) p)%Z ->
(bpow e' <= F2R (Float beta m e))%R -> (bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R ->
exists m' : Z, F2R (Float beta m e) = F2R (Float beta (m * Zpower (radix_val beta) (e - e' + p)) (e' - p)).
F2R (Float beta m e) = F2R (Float beta m' (e' - (p - 1))).
Proof. Proof.
intros m e e' p Hm Hf. intros m e e' p Hm Hf.
exists (m * Zpower (radix_val beta) (e - (e' - (p - 1))))%Z. assert (Hp: (0 <= p)%Z).
unfold F2R. destruct p ; try easy.
simpl. now elim (Zle_not_lt _ _ (Zabs_pos m)).
rewrite mult_Z2R. (* . *)
rewrite Rmult_assoc. replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.
apply Rmult_eq_compat_l. apply F2R_change_exp.
rewrite Z2R_Zpower. cut (e' - 1 < e + p)%Z. omega.
rewrite <- epow_add.
apply f_equal.
ring.
assert (e' <= e + (p - 1))%Z.
2: omega.
apply Zlt_succ_le.
unfold Zsucc.
replace (e + (p - 1) + 1)%Z with (e + p)%Z by ring.
apply <- epow_lt. apply <- epow_lt.
apply Rle_lt_trans with (1 := Hf). apply Rle_lt_trans with (1 := Hf).
unfold F2R. unfold F2R.
rewrite epow_add. rewrite epow_add, Rabs_mult, Rabs_Z2R, Rabs_pos_eq.
rewrite Rmult_comm. rewrite Rmult_comm.
apply Rmult_lt_compat_l. apply Rmult_lt_compat_l.
apply epow_gt_0. apply epow_gt_0.
simpl. rewrite <- Z2R_Zpower.
apply Rle_lt_trans with (1 := RRle_abs _).
rewrite Z2R_IZR.
rewrite Rabs_Zabs.
rewrite <- Z2R_IZR.
replace (bpow p) with (Z2R (Zpower (radix_val beta) p)).
now apply Z2R_lt. now apply Z2R_lt.
rewrite Z2R_Zpower. exact Hp.
apply refl_equal. apply epow_ge_0.
clear -Hm.
destruct p as [_|p|p] ; try discriminate.
simpl in Hm.
elim Zlt_not_le with (1 := Hm).
apply Zabs_pos.
Qed.
Theorem F2R_prec_normalize :
forall m e e' p : Z,
(Zabs m < Zpower (radix_val beta) p)%Z ->
(bpow e' <= Rabs (F2R (Float beta m e)))%R ->
exists m' : Z,
F2R (Float beta m e) = F2R (Float beta m' (e' - (p - 1))).
Proof.
intros [|m|m] e e' p Hm Hf.
exists Z0.
unfold F2R. simpl.
now rewrite 2!Rmult_0_l.
(* . *)
apply F2R_prec_normalize_pos.
exact Hm.
now rewrite abs_F2R in Hf.
(* . *)
destruct (F2R_prec_normalize_pos (Zpos m) e e' p) as (m', Hm').
exact Hm.
now rewrite abs_F2R in Hf.
exists (Zopp m').
rewrite <- opp_F2R.
rewrite <- Hm'.
unfold F2R. simpl.
apply Ropp_mult_distr_l_reverse.
Qed. Qed.
End Float_prop. End Float_prop.
\ No newline at end of file
...@@ -103,24 +103,12 @@ simpl. ...@@ -103,24 +103,12 @@ simpl.
specialize (Hx5 (Rabs_pos_lt _ Hx4)). specialize (Hx5 (Rabs_pos_lt _ Hx4)).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ; destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2. rewrite H2 ; clear H2.
destruct (F2R_prec_normalize beta xm xe (ex - 1) prec Hx2) as (mx, Hx6). rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now rewrite <- Hx1.
rewrite Hx1, Hx6.
replace (ex - 1 - (prec - 1))%Z with (ex - prec)%Z by ring.
now eexists. now eexists.
assert (Hx6 : x = F2R (Float beta (xm * Zpower (radix_val beta) (xe - emin)) emin)). now rewrite <- Hx1.
rewrite Hx1. rewrite Hx1, (F2R_change_exp beta emin).
unfold F2R. simpl.
rewrite mult_Z2R.
rewrite Z2R_Zpower.
rewrite Rmult_assoc.
apply f_equal.
rewrite <- epow_add.
apply f_equal.
ring.
now apply Zle_minus_le_0.
rewrite Hx6.
now eexists. now eexists.
exact Hx3.
Qed. Qed.
Theorem FLT_format_satisfies_any : Theorem FLT_format_satisfies_any :
......
...@@ -76,11 +76,9 @@ unfold generic_format, canonic. ...@@ -76,11 +76,9 @@ unfold generic_format, canonic.
destruct (ln_beta beta (Rabs x)) as (ex, Hx4). destruct (ln_beta beta (Rabs x)) as (ex, Hx4).
simpl. simpl.
specialize (Hx4 (Rabs_pos_lt _ Hx3)). specialize (Hx4 (Rabs_pos_lt _ Hx3)).
destruct (F2R_prec_normalize beta xm xe (ex - 1) prec Hx2) as (mx, Hx5). rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now rewrite <- Hx1.
rewrite Hx1, Hx5.
replace (ex - 1 - (prec - 1))%Z with (ex - prec)%Z by ring.
now eexists. now eexists.
now rewrite <- Hx1.
Qed. Qed.
Theorem FLX_format_satisfies_any : Theorem FLX_format_satisfies_any :
......
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