Commit 0e887112 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Simplified theorems about inclusion.

parent 236fb3aa
......@@ -208,29 +208,14 @@ Theorem FLT_generic_format_FIX :
(Rabs x <= bpow (emin + prec))%R ->
generic_format beta (FIX_exp emin) x ->
generic_format beta FLT_exp x.
Proof.
intros x Hx H'.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply generic_format_0.
destruct Hx as [Hx|Hx].
unfold generic_format, scaled_mantissa.
now rewrite (FLT_canonic_FIX x Hx0 Hx).
(* extra case *)
rewrite <- (Rabs_pos_eq (bpow (emin + prec))) in Hx. 2: apply bpow_ge_0.
assert (H1: generic_format beta FLT_exp (bpow (emin + prec))).
apply generic_format_bpow.
unfold FLT_exp.
assert (Hp := prec_gt_0 prec).
apply Zmax_lub ; clear -Hp ; omega.
assert (H2: generic_format beta (FIX_exp emin) (bpow (emin + prec))).
apply generic_format_bpow.
Proof with auto with typeclass_instances.
clear prec_gt_0_.
apply generic_inclusion_le...
intros e He.
unfold FIX_exp.
generalize (prec_gt_0 prec).
clear ; omega.
destruct Rabs_eq_Rabs with (1 := Hx) as [H|H] ;
rewrite H ; clear H ;
try apply generic_format_opp ; easy.
apply Zmax_lub.
omega.
apply Zle_refl.
Qed.
(** FLT is a nice format: it has a monotone exponent... *)
......
......@@ -70,52 +70,6 @@ exact H2.
now rewrite <- H1.
Qed.
Theorem FLX_format_FIX :
forall x e,
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FIX_format beta (e - prec) x ->
FLX_format x.
Proof.
intros x e (Hx1,[Hx2|Hx2]).
(* . *)
intros ((xm, xe), (H1, H2)).
rewrite H1.
eexists ; repeat split.
simpl.
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow (e - prec)).
apply bpow_gt_0.
rewrite Z2R_Zpower, <- bpow_plus.
ring_simplify (prec + (e - prec))%Z.
rewrite <- H2.
simpl.
change (F2R (Float beta (Zabs xm) xe) < bpow e)%R.
now rewrite <- abs_F2R, <- H1.
now apply Zlt_le_weak.
(* . *)
intros ((xm, xe), (H1, H2)).
assert (Ha: forall x, FLX_format (Rabs x) -> FLX_format x).
clear.
intros x Ha.
unfold Rabs in Ha.
destruct (Rcase_abs x) as [Hx|Hx].
destruct Ha as ((m,e),(Ha,Hb)).
exists (Float beta (-m) e).
split.
now rewrite <- opp_F2R, <- Ha, Ropp_involutive.
simpl.
now rewrite Zabs_Zopp.
exact Ha.
(* . . *)
apply Ha.
rewrite Hx2.
exists (Float beta 1 e).
split.
apply sym_eq.
apply Rmult_1_l.
now apply Zpower_gt_1.
Qed.
Theorem FLX_format_generic :
forall x, generic_format beta FLX_exp x -> FLX_format x.
Proof.
......@@ -169,6 +123,20 @@ apply FLX_format_generic.
apply generic_format_FLX.
Qed.
Theorem FLX_format_FIX :
forall x e,
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
FIX_format beta (e - prec) x ->
FLX_format x.
Proof with auto with typeclass_instances.
intros x e Hx Fx.
apply FLX_format_generic.
apply generic_format_FIX in Fx.
revert Fx.
apply generic_inclusion with (e := e)...
apply Zle_refl.
Qed.
(** unbounded floating-point format with normal mantissas *)
Definition FLXN_format (x : R) :=
exists f : float beta,
......
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